search

microsoft / Komodo

Formally-verified reference monitor for a secure isolated execution ("enclave") environment on ARM TrustZone
https://www.microsoft.com/en-us/research/project/komodo/
Other
103 stars 28 forks source link

./verified/remove.vad(76,56): Error: assertion violation #12

Open xiexiewww opened 6 years ago

xiexiewww commented 6 years ago

when I make verified,there is a error in remove.vad,line 76 line76: assert extractPageDbEntry(this.m, as_page) == extractPageDbEntry(old(this.m), as_page); I do not kown why? who can help me? Thank you very much!

xiexiewww commented 6 years ago

Anyone here? Emm.............

0xabu commented 6 years ago

This definitely worked for us, but unfortunately the verification tools can be unstable on different machines/environments. Are you using the same versions of the dafny, Z3 and boogie binaries included in the repository? Can you copy and paste the exact error message and the steps you used to recreate it?

xiexiewww commented 6 years ago

We used boogie binaries and dafny in the repository.But,we can not make verified (because it can only find z3.exe,but it can not work, and it suggested us to install z3) until we installed Z3(linux distribution for ubuntu 16.04), it may cause this problem,we run this project on ubuntu17.so,which z3 should I Iinstall? Thanks very much！

0xabu commented 6 years ago

The Windows x64 Z3 binary in our repo is built from commit 169295c9ba74802e4e17b908982ba8a9f1c9f491, so if you wanted to be sure you could build Z3 for Linux at that specific commit. For a near guess, try the next Z3 release which would be 4.6.0, but I can't guarantee it will work.

xiexiewww commented 6 years ago

It can not work,because we used z3(4.6.0)....haha😂😂

xiexiewww commented 6 years ago

I will try it next day,thanks very much!Good night!

Davidleeh commented 6 years ago

Encountered the same issue here...

Same as @xiexiewww , cannot use z3.exe in the repo since:

Under Ubuntu 18.04, the SConscript (line 171-184) in tools/vale/tools/Vale cannot locate z3.exe since the path "/proc/sys/fs/binfmt_misc/WSLInterop" is not existed. Therefore it has to find "z3", instead of "z3.exe". Hacked the script to search for "z3.exe", then there was "FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.IO.IOException: Write fault on path" error.

Natively building z3 4.7.1 solved the above issue, but encountered the same error: " Verifying Impl$$_module.default.valemmakomsmcremovenonaddrsuccess ... [16.844 s, 456 proof obligations] error ./verified/remove.vad(76,56): Error: assertion violation "

Seems related to pagedb.*... Any hints? Thanks!

Davidleeh commented 6 years ago

Update:

As @0xabu mentioned, natively built z3 with the specific commit solved the issue.

Z3 version 4.5.1 - 64 bit

Might be able to close this issue. :)