![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/01\/Project_Everest_Blog_Site_1400x788-1024x576.png\")
<\/p>\n<\/p>\n
Project Everest (opens in new tab)<\/span><\/a> is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and developing, is the first in a series exploring the groundbreaking work, which is available on GitHub (opens in new tab)<\/span><\/a> now.<\/em><\/p>\n Wouldn\u2019t it be great if a message you sent to your bank over the internet was guaranteed to be safe from tampering and readable only by your financial institution? Project Everest is building software that provides such a guarantee as a theorem<\/em> about the code<\/em> that implements a secure communication protocol deployed in web browsers and servers everywhere.<\/p>\n \u201cProving theorems about programs has been a dream of computer science for the last 60 years or more, and we\u2019re finally able to do this at the scale required for an important, widely deployed security-critical piece of software,\u201d says Microsoft Senior Researcher Nik Swamy<\/a>, a member of the Project Everest team.<\/p>\n The security of internet communications crucially depends on a variety of cryptographic algorithms and protocols. The most widely used among these falls under the umbrella of the Transport Layer Security (TLS) protocol (opens in new tab)<\/span><\/a>. TLS is used for secure web browsing via HTTPS, email, Voice over IP, instant messaging, and many other kinds of communication. Unfortunately, TLS and its many implementations have been attacked repeatedly (opens in new tab)<\/span><\/a> over its 25-year history.<\/p>\n Project Everest (opens in new tab)<\/span><\/a> is an ongoing collaboration started in 2016 with researchers from Microsoft Research Redmond<\/a>, Microsoft Research Cambridge<\/a>, Microsoft Research India<\/a>, the Microsoft Research-Inria Joint Centre (opens in new tab)<\/span><\/a> in Paris, Inria (opens in new tab)<\/span><\/a>, Carnegie Mellon University (opens in new tab)<\/span><\/a>, and The University of Edinburgh (opens in new tab)<\/span><\/a>. Growing out of several prior Microsoft Research projects, including Ironclad<\/a>, miTLS (opens in new tab)<\/span><\/a>, and F* (opens in new tab)<\/span><\/a>, Everest aims to develop and deploy efficient, verified, open-source implementations of the entire TLS stack and related protocols, formally reducing the security of the code to the assumptions about the hardness of certain cryptographic problems (opens in new tab)<\/span><\/a>.<\/p>\n For Jonathan Protzenko<\/a>, a Microsoft researcher on the Everest team, the project\u2019s open collaboration is special.<\/p>\n \u201cEverest makes for a tight interaction between industrial and academic research,\u201d he says. \u201cOur members frequently visit each other, co-author papers together, and send students from one institution to the other over the summer. Several of our members studied at or later moved to these institutions. In that sense, for me, Project Everest truly represents the ideal of open, collaborative research.\u201d<\/p>\n Project Everest is halfway through its projected five-year arc, and its verified components are beginning to replace the current infrastructure with proven, secure software. For instance, Everest\u2019s HACL* (opens in new tab)<\/span><\/a> library provides verified cryptographic primitives for Mozilla Firefox (opens in new tab)<\/span><\/a>, for the WireGuard VPN (opens in new tab)<\/span><\/a>, and for the Tezos blockchain (opens in new tab)<\/span><\/a>. And within Microsoft, Everest\u2019s miTLS protocol stack (opens in new tab)<\/span><\/a> powers the primary implementation of the QUIC transport protocol. The Everest team expects to announce further deployments in the coming weeks. Meanwhile, Everest code is already open source and is developed publicly on GitHub (opens in new tab)<\/span><\/a>.<\/p>\n Formal verification involves using software tools, including various kinds of theorem provers and proof assistants, to analyze all<\/em> possible behaviors of a program and prove mathematically they comply with the code\u2019s specification, a machine-readable description of the developer\u2019s intentions. Once the code has been verified against its specification mechanically, based on trust in the software used to check proofs, a skeptical auditor need only study the specifications<\/em> and the theorem statements<\/em> proven without needing to consult the much larger programs and proofs.<\/p>\n \u201cMost software built today gets tested before it is released\u2014at least one hopes it does!\u201d says Swamy. \u201cBut even the most rigorous testing can only find bugs; it cannot rule out the existence of errors. For certain kinds of software, say security-critical code like TLS, one may actually want to prove that no vulnerabilities exist. Software verification is time-consuming and requires expertise, but, unlike testing, it can actually guarantee mathematically the absence of entire classes of errors.\u201d<\/p>\n For Everest programs, the team\u2019s specifications cover a range of properties, including:<\/p>\n Formal verification can play a role throughout the software development process, from design to implementations and deployments. The value of verification is increasingly widely perceived, especially for security-critical code.<\/p>\n \u201cCryptographic protocols are notoriously hard to implement correctly, with errors in both the algorithms and the protocol implementation itself being common,\u201d says Eric Rescorla, chief technology officer of Mozilla Firefox, security area director at the Internet Engineering Task Force, and the editor of the TLS standard. \u201cFormal verification tools like those developed by the Project Everest team have transformed the way we design these protocols, allowing us to move faster while having much higher confidence in protocol correctness.\u201d<\/p>\n Indeed, assisted in part by their verification efforts, Benjamin Beurdouche (opens in new tab)<\/span><\/a>, Karthik Bhargavan (opens in new tab)<\/span><\/a>, Antoine Delignat-Lavaud (opens in new tab)<\/span><\/a>, and C\u00e9dric Fournet<\/a>, all members of Project Everest, have contributed features and fixes to the TLS standard. Beyond assisting with designs and specifications, verified implementations are also increasingly attractive for mainstream deployment.<\/p>\n \u201cVerified implementations of cryptographic primitives are gradually making their way into major implementations,\u201d Rescorla adds. \u201cThe Curve25519 and ChaCha\/Poly1305 algorithms from HACL* are already running in Firefox, and I look forward to the day when we can adopt completely verified implementations.\u201d<\/p>\n All Everest code is programmed and verified using F* (opens in new tab)<\/span><\/a>, a framework that brings together three strands of research in programming languages.<\/p>\n \u201cStarting from a language in my dissertation called Fable and a language developed at Microsoft Research Cambridge called F7<\/a>, F* has evolved repeatedly over the course of almost a decade and is now developed by a large but closely knit team of people and has become a full-fledged proof assistant,\u201d Swamy says.<\/p>\n \u201cF* is unique in its use of both automated and interactive proofs, and its primitive support for effects makes it well-suited for verifying real-world software that is inherently effectful,\u201d adds Aseem Rastogi<\/a>, a researcher at Microsoft Research India and member of the Project Everest team.<\/p>\n The following simple F* program, a functionally correct implementation of Quicksort on lists, is an example of how it operates. Given a list and total order on its elements, the type of quicksort <\/span>on the first line asserts that the function always returns a sorted permutation of the original list.<\/p>\n While proving purely functional code, such as quicksort <\/span>above, is relatively straightforward, to achieve high performance, Everest code is also programmed in two domain-specific languages embedded in F*: Low* and Vale.<\/p>\n Low* (opens in new tab)<\/span><\/a> is a subset of F* geared toward low-level programming with explicit memory management. Low* programs are extracted to idiomatic C code by a tool called KReMLin (opens in new tab)<\/span><\/a> and run without garbage collection, reference counting, or any other automated memory management strategy. The HACL* library and Everest\u2019s verified implementation of the TLS-1.3 record layer (opens in new tab)<\/span><\/a> are programmed and verified in Low*.<\/p>\n For various cryptographic primitives, peak performance can only be obtained by going still lower level and programming in assembly language, often taking advantage of specialized hardware instructions, such as Intel AES-NI (opens in new tab)<\/span><\/a>. Vale (opens in new tab)<\/span><\/a> stands for \u201cVerified Assembly Language for Everest\u201d and provides a domain-specific language for writing and verifying assembly programs targeting different platforms, like Windows, MacOS, and Linux, and architectures, like x86, x64, and ARM. It also supports multiple verification systems for carrying out proofs, including F* and Dafny.<\/p>\n The 2019 Symposium on Principles of Programming Languages (POPL) (opens in new tab)<\/span><\/a> features a paper on Vale<\/a>. \u201cA Verified, Efficient Embedding of a Verifiable Assembly Language\u201d describes how the Everest team embedded Vale in F*, making use of F*\u2019s dependent type system and its computational capabilities to implement an efficient verification condition generator for embedded assembly programs. Using Vale in F*, the Everest team reports on the first provably correct implementation of AES-GCM (opens in new tab)<\/span><\/a>, a cryptographic routine used by 90 percent of secure internet traffic.<\/p>\n In addition to the availability of Everest components on GitHub (opens in new tab)<\/span><\/a>, the team is planning the first integrated release of Everest\u2019s verified stack, its libraries, and its verification tools for early summer 2019.<\/p>\n \u201cWorking at the intersection of systems, networking, cryptography, programming languages, and program verification, Everest is unique in that it co-develops verified software with the tools and techniques needed to build it,\u201d says Swamy. \u201cBut we\u2019re also looking beyond our specific goals for TLS to apply our verification technology to other areas.\u201d<\/p>\n For instance, the Everest team is also working on verifying implementations of post-quantum cryptography<\/a> and proving the security of key components used in high-assurance enterprise blockchains (opens in new tab)<\/span><\/a>.<\/p>\n Spanning four continents and 12 time zones, the Everest team works around the clock trying to build a more secure internet. There\u2019s still a long way to go to the summit, but halfway through the project, the team has learned a lot and has put down footholds to make it easier to build provably secure software at scale.<\/p>\n","protected":false},"excerpt":{"rendered":" Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and developing, is the first in a series exploring the groundbreaking work, which is available on […]<\/p>\n","protected":false},"author":37074,"featured_media":560244,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194487,194489],"tags":[],"research-area":[13560],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-559317","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-privacy","category-security","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[144812,144927,663087],"related-projects":[235367],"related-events":[558255],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/01\/5c33d2746ef61-5c33d2746ef62Everest-All-Hands-Cambridge-Sep-19-21-2018-1.jpg-1024x585.jpg\")
Members of the Project Everest team are working hard for greater internet security, and their progress is tangible: Two and a half years in, their verified components are already beginning to replace the current infrastructure with proven, secure software.<\/p><\/div>\nFormal Verification of Software<\/h3>\n
\n
F*, Low*, and Vale<\/h3>\n
\n
![\"let](\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/01\/Quicksort-1024x227.png\")
[] | pivot::tl -> let hi, lo = partition (f pivot) tl in quicksort lo f @ pivot :: quicksort hi f\" width=\"1024\" height=\"227\" \/><\/p>\nVerifying efficient low-level code in F*<\/h3>\n
What\u2019s next?<\/h3>\n
![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/01\/Project_Everest_Blog_Site_1400x788-5c3cc1477b0f5.png\")
","byline":"","formattedDate":"January 14, 2019","formattedExcerpt":"Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and developing, is the first in…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/559317","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/37074"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=559317"}],"version-history":[{"count":10,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/559317\/revisions"}],"predecessor-version":[{"id":576771,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/559317\/revisions\/576771"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/560244"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=559317"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=559317"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=559317"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=559317"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=559317"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=559317"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=559317"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=559317"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=559317"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=559317"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=559317"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}