{"id":429627,"date":"2017-10-06T16:17:11","date_gmt":"2017-10-06T23:17:11","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=429627"},"modified":"2025-02-06T11:07:49","modified_gmt":"2025-02-06T19:07:49","slug":"komodo","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/komodo\/","title":{"rendered":"Komodo: Using verification to disentangle secure-enclave hardware from software"},"content":{"rendered":"<p>Komodo is a formally-verified reference monitor for an attested, secure isolated execution environment (&#8220;enclave&#8221;) on ARM TrustZone. It illustrates an alternative approach to Intel&#8217;s SGX, achieving similar security guarantees through formal verification, and allowing enclave features to evolve independently of the underlying hardware.<\/p>\n<p>Komodo is described by <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/komodo-using-verification-disentangle-secure-enclave-hardware-software\/\">our paper in SOSP&#8217;17<\/a>. The formal specification, prototype, and proofs are available at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/Microsoft\/Komodo\">GitHub<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Komodo is a formally-verified reference monitor for an attested, secure isolated execution environment (&#8220;enclave&#8221;) on ARM TrustZone. It illustrates an alternative approach to Intel&#8217;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&#8217;17. The formal specification, prototype, [&hellip;]<\/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-complete"],"msr_project_start":"2016-03-01","related-publications":[386810,429705,606981],"related-downloads":[],"related-videos":[],"related-groups":[144927],"related-events":[],"related-opportunities":[],"related-posts":[451146],"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","targetHints":{"allow":["GET"]}}],"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":7,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/429627\/revisions"}],"predecessor-version":[{"id":1126980,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/429627\/revisions\/1126980"}],"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}]}}