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

Wrap core of SHA in a function call #2

Open 0xabu opened 7 years ago

0xabu commented 7 years ago

This would substantially reduce the code size of the monitor. Since vale doesn't support calls, we'd need to specify/verify a function call/return sequence, and manually print the code for it.