{"id":235367,"date":"2020-02-27T07:12:30","date_gmt":"2016-05-31T09:09:04","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=235367"},"modified":"2023-02-15T01:49:37","modified_gmt":"2023-02-15T09:49:37","slug":"project-everest-verified-secure-implementations-https-ecosystem","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/","title":{"rendered":"Project Everest"},"content":{"rendered":"<section class=\"mb-3 moray-highlight\">\n\t<div class=\"card-img-overlay mx-lg-0\">\n\t\t<div class=\"card-background  has-background- card-background--full-bleed\">\n\t\t\t<img loading=\"lazy\" decoding=\"async\" width=\"1920\" height=\"720\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest.jpg\" class=\"attachment-full size-full\" alt=\"\" style=\"\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest.jpg 1920w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest-300x113.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest-1024x384.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest-768x288.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest-1536x576.jpg 1536w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/Everest-1600x600.jpg 1600w\" sizes=\"(max-width: 1920px) 100vw, 1920px\" \/>\t\t<\/div>\n\t\t<!-- Foreground -->\n\t\t<div class=\"card-foreground d-flex mt-md-n5 my-lg-5 px-g px-lg-0\">\n\t\t\t<!-- Container -->\n\t\t\t<div class=\"container d-flex mt-md-n5 my-lg-5 align-self-center\">\n\t\t\t\t<!-- Card wrapper -->\n\t\t\t\t<div class=\"w-100 w-lg-col-5\">\n\t\t\t\t\t<!-- Card -->\n\t\t\t\t\t<div class=\"card material-md-card py-5 px-md-5\">\n\t\t\t\t\t\t<div class=\"card-body \">\n\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\n\n<h1 id=\"project-everest\" class=\"h2\">Project Everest<\/h1>\n\n\n\n<p>Building and deploying provably secure communication software<\/p>\n\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/div>\n<\/section>\n\n\n\n\n\n<h2 id=\"summary\">Summary<\/h2>\n\n\n\n<p>The <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/project-everest.github.io\" target=\"_blank\" rel=\"noopener\">main Project Everest web page<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> is hosted on GitHub.&nbsp;This site serves only to aggregate all content on the Microsoft site related to Everest.<\/p>\n\n\n\n<h3 id=\"related-work\">Related work<\/h3>\n\n\n\n<p>The project brings together the following Microsoft Research projects and tools:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/mitls.org\/\" target=\"_blank\" rel=\"noopener\">miTLS<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a verified implementation of TLS 1.2 and 1.3<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/project-everest\/hacl-star\" target=\"_blank\" rel=\"noopener\">HACL*<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a verified library of cryptographic primitives<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/hacl-star.github.io\/HaclValeEverCrypt.html\" target=\"_blank\" rel=\"noopener\">EverCrypt<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a verified cryptographic library<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/project-everest.github.io\/everparse\/\" target=\"_blank\" rel=\"noopener\">EverParse<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; an automatic generator for verified parsers and serializers for binary data formats<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/project-everest.github.io\/vale\/\" target=\"_blank\" rel=\"noopener\">Vale<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a verified assembly language<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/fstarlang.github.io\/lowstar\/html\/\" target=\"_blank\" rel=\"noopener\">Low* and KReMLin<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, a language subset of F* and a C code generator to model and verify C programs<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/www.fstar-lang.org\/\" target=\"_blank\" rel=\"noopener\">F*<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; an ML-like functional programming language aimed at program verification<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/dafny\" target=\"_blank\" rel=\"noopener\">Dafny<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a verification-aware programming language<\/li>\n\n\n\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Z3Prover\/z3\" target=\"_blank\" rel=\"noopener\">Z3<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> &#8211; a SMT theorem prover<\/li>\n<\/ul>\n\n\n\n<figure class=\"wp-block-image alignnone\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/collaboration\/inria-joint-centre\/\"><img loading=\"lazy\" decoding=\"async\" width=\"300\" height=\"197\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-300x197.jpg\" alt=\"INRIA graphic\" class=\"wp-image-739756\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-300x197.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-1024x672.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-768x504.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-1536x1008.jpg 1536w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-2048x1343.jpg 2048w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/02\/INRIA-graphic-16x10.jpg 16w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><figcaption class=\"wp-element-caption\">In collaboration with Inria Joint Center<\/figcaption><\/figure>\n\n\n\n\n\n<p><iframe loading=\"lazy\" title=\"Verified Low-Level Programming Embedded in F*\" width=\"500\" height=\"281\" src=\"https:\/\/www.youtube-nocookie.com\/embed\/3F8PU7Y-lTw?start=2&feature=oembed\" frameborder=\"0\" allow=\"accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share\" referrerpolicy=\"strict-origin-when-cross-origin\" allowfullscreen><\/iframe><\/p>\n\n\n","protected":false},"excerpt":{"rendered":"<p>Project Everest aims to build and deploy a verified HTTPS stack, constructing a high-performance, standards-compliant, and\u00a0veri\ufb01ed implementation of the full HTTPS ecosystem.<\/p>\n","protected":false},"featured_media":649929,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560,13558],"msr-locale":[268875],"msr-impact-theme":[261676],"msr-pillar":[],"class_list":["post-235367","msr-project","type-msr-project","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-locale-en_us","msr-archive-status-complete"],"msr_project_start":"","related-publications":[380516,590623,380549,619023,420279,662418,420288,662424,422070,669240,445551,695655,481464,701437,503894,741925,557169,845653,564012,900717,564099],"related-downloads":[345386,489092,736225,736231,736240,736246,736252,736291,828283],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[{"id":0,"name":"Talks & workshops","content":"[embed]https:\/\/www.youtube.com\/watch?time_continue=2&amp;v=3F8PU7Y-lTw&amp;feature=emb_logo[\/embed]"}],"slides":[],"related-researchers":[{"type":"guest","display_name":"Benjamin  Beurdouche","user_id":741892,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Karthikeyan  Bhargavan","user_id":571929,"people_section":"Section name 0","alias":""},{"type":"user_nicename","display_name":"Antoine Delignat-Lavaud","user_id":31056,"people_section":"Section name 0","alias":"antdl"},{"type":"user_nicename","display_name":"C\u00e9dric Fournet","user_id":31819,"people_section":"Section name 0","alias":"fournet"},{"type":"guest","display_name":"Aymeric  Fromherz","user_id":741898,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Sydney Gibson","user_id":741901,"people_section":"Section name 0","alias":""},{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Section name 0","alias":"chrishaw"},{"type":"guest","display_name":"C\u0103t\u0103lin Hri\u021bcu","user_id":741904,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Markulf  Kohlweiss","user_id":741907,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Natalia Kulatova","user_id":741910,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Guido Mart\u00ednez","user_id":741913,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Denis Merigoux","user_id":741916,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Bryan Parno","user_id":741919,"people_section":"Section name 0","alias":""},{"type":"guest","display_name":"Marina Polubelova","user_id":741922,"people_section":"Section name 0","alias":""},{"type":"user_nicename","display_name":"Jonathan Protzenko","user_id":33286,"people_section":"Section name 0","alias":"protz"},{"type":"user_nicename","display_name":"Tahina Ramananandro","user_id":36293,"people_section":"Section name 0","alias":"taramana"},{"type":"user_nicename","display_name":"Aseem Rastogi","user_id":36021,"people_section":"Section name 0","alias":"aseemr"},{"type":"user_nicename","display_name":"Nikhil Swamy","user_id":33138,"people_section":"Section name 0","alias":"nswamy"},{"type":"user_nicename","display_name":"Santiago Zanella-B\u00e9guelin","user_id":33518,"people_section":"Section name 0","alias":"santiago"}],"msr_research_lab":[199562,199565,199561],"msr_impact_theme":["Trust"],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/235367"}],"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":21,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/235367\/revisions"}],"predecessor-version":[{"id":919476,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/235367\/revisions\/919476"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/649929"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=235367"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=235367"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=235367"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=235367"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=235367"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}