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

Avoid needless TLB flushes in SVC handler #5

Open 0xabu opened 6 years ago

0xabu commented 6 years ago

Prove that SHA code (and the SVC handlers that wrap it) preserve TLB consistency, and thus avoid needless TLB flushes in those SVC handlers.