Komodo is a formally-verified reference monitor for an attested, secure isolated execution environment (“enclave”) on ARM TrustZone. It illustrates an alternative approach to Intel’s SGX, achieving similar security guarantees through formal verification, and allowing enclave features to evolve independently of the underlying hardware.<\/p>\n
Komodo is described by our paper in SOSP’17 (opens in new tab)<\/span><\/a>. The formal specification, prototype, and proofs are available at GitHub (opens in new tab)<\/span><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":" Komodo is a formally-verified reference monitor for an attested, secure isolated execution environment (“enclave”) on ARM TrustZone. It illustrates an alternative approach to Intel’s SGX, achieving similar security guarantees through formal verification, and allowing enclave features to evolve independently of the underlying hardware. Komodo is described by our paper in SOSP’17. The formal specification, prototype, […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13547],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-429627","msr-project","type-msr-project","status-publish","hentry","msr-research-area-systems-and-networking","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2016-03-01","related-publications":[429705,606981,386810],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"guest","display_name":"Andrew Ferraiuolo","user_id":429651,"people_section":"Section name 1","alias":""},{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Section name 1","alias":"chrishaw"},{"type":"guest","display_name":"Bryan Parno","user_id":429675,"people_section":"Section name 1","alias":""}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/429627"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":6,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/429627\/revisions"}],"predecessor-version":[{"id":431319,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/429627\/revisions\/431319"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=429627"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=429627"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=429627"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=429627"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=429627"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}