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
102 stars 28 forks source link

Use resource limits rather than time limits for verification #1

Open 0xabu opened 6 years ago

0xabu commented 6 years ago

Dafny now supports Z3 resource limits (https://github.com/Microsoft/dafny/issues/106). We should convert to them to avoid unstable / unpredictable timeouts when verifying. This will require determining appropriate limits and updating the lemmas for which we have hardcoded time limit multipliers.