An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app’s behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times.<\/p>\n
Our specifications, code, proofs, and tools for our projects Ironclad Apps<\/a>\u00a0(verifying the security an a complete software stack)\u00a0and IronFleet<\/a>\u00a0(verifying\u00a0the safety and liveness of\u00a0distributed systems) are now available on GitHub<\/a>.\u00a0\u00a0Comments, suggestions, and pull requests\u00a0are welcome!<\/p>\n One of the key verification tools we use is Dafny<\/a>.\u00a0 Try it out on Rise4Fun<\/a>!\u00a0 Learn more from the official Dafny site<\/a>.\u00a0 Dafny, in turn, relies on Boogie<\/a>, which relies on the Z3 SMT solver<\/a>.\u00a0 We also employ SymDiff<\/a> to verify relational properties.<\/p>\n","protected":false},"excerpt":{"rendered":" An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app’s behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13546,13560,13558,13547],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-171410","msr-project","type-msr-project","status-publish","hentry","msr-research-area-computational-sciences-mathematics","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-research-area-systems-and-networking","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2014-10-02","related-publications":[159433,167532,168694,395171,663702],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Group 1","alias":"chrishaw"},{"type":"user_nicename","display_name":"Jay Lorch","user_id":32732,"people_section":"Group 1","alias":"lorch"},{"type":"user_nicename","display_name":"Srinath Setty","user_id":33709,"people_section":"Group 1","alias":"srinath"}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171410"}],"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":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171410\/revisions"}],"predecessor-version":[{"id":604257,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171410\/revisions\/604257"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=171410"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=171410"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=171410"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=171410"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=171410"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}