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

There was a problem when running make in the top-level directory #19

Closed hz1490919302 closed 4 years ago

hz1490919302 commented 4 years ago

QQ截图20191204214953

0xabu commented 4 years ago

What environment are you building on? Native Linux, Cygwin or WSL? Based on this build output, it appears to be one of the latter, but the native vale.exe executable has a problem. Can you run tools/vale/bin/vale.exe on its own? Can you run it from a CMD prompt?

hz1490919302 commented 4 years ago

I have solved the problem.I am building on the WSL.So I use mono bin / vale.exe instead of vale.exe. Thank you very much.

hz1490919302 commented 4 years ago

Sorry, I encountered another problem. The modules _lemmaARML2PTE_helper and lemmanonexecmapping in the file verified / ptebits.i.dfy timed out during validation,which causes running make to fail. According to the description, these modules should complete verification in 90 seconds, but they exceed 90 seconds. QQ截图20191205192421 QQ截图20191205192434 QQ截图20191205192513 QQ截图20191205192853

0xabu commented 4 years ago

I have solved the problem.I am building on the WSL. So I use mono bin / vale.exe instead of vale.exe. Thank you very much.

Interesting. Mono shouldn't be required to run .NET binaries on WSL. I'm guessing that you're using the new VM-based WSL2, and something has changed in this respect.

Sorry, I encountered another problem. The modules _lemmaARML2PTE_helper and lemmanonexecmapping in the file verified / ptebits.i.dfy timed out during validation,which causes running make to fail. According to the description, these modules should complete verification in 90 seconds, but they exceed 90 seconds.

Timeouts are a known issue. See #1, and #7 for a possible workaround.