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

Avoid needless register save/restore in entry path #3

Open 0xabu opened 6 years ago

0xabu commented 6 years ago

Prove that user execution cannot alter any of:

Then, use that lemma where needed in the enclave entry/return path, rather than needlessly saving and restoring the register values.