![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2019\/03\/Evercrypt_Blog_Site_01_2019_BlogHeader_cropped-002-1024x328.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 high-performance industrial-grade EverCrypt cryptographic provider (opens in new tab)<\/span><\/a>, is the second in a series exploring the groundbreaking work, which is available on GitHub (opens in new tab)<\/span><\/a> now.<\/em><\/p>\n If you\u2019re reading this blog post right now, you\u2019re likely using HTTPS, the most popular application of the Transport Layer Security (TLS) protocol. In fact, if you\u2019ve logged in to a website, checked your email, ordered a product, or banked online today, you\u2019ve used it. Just check out the URL in your address bar. An internet standard, TLS powers most secure communications over the internet, ensuring all clients and servers can interoperate with each other.<\/p>\n Delivering an implementation of TLS that guarantees with mathematical certainty your communications will be confidential and protected is a vast and ambitious effort. Like the building of a pyramid, it requires a strong foundation. Such an implementation needs successive verified software layers, beginning with the raw cryptographic algorithms, followed by a cryptographic provider. A crucially important component, the cryptographic provider orchestrates these standalone algorithms into a unified collection to meet the security needs of the protocol. Today, we\u2019re happy to introduce the first fully verified cryptographic provider.<\/p>\n EverCrypt (opens in new tab)<\/span><\/a>\u2014developed and verified by the Project Everest (opens in new tab)<\/span><\/a> team\u2014offers the same features, convenience, and performance as popular existing cryptographic libraries without the bugs that leave protocols and applications vulnerable. Usable by verified and unverified clients alike, EverCrypt emphasizes both multiplatform support and high performance. We accomplish this by producing both platform-agnostic C code and optimized assembly code for specific hardware targets through the combination of two components of Project Everest: the HACL* (opens in new tab)<\/span><\/a> cryptographic library developed jointly between Inria (opens in new tab)<\/span><\/a> and Microsoft Research and the Vale-Crypto library (opens in new tab)<\/span><\/a> of assembly primitives developed collectively between Microsoft Research and Carnegie Mellon University (opens in new tab)<\/span><\/a>.<\/p>\n Historically, writing a high-quality, trustworthy cryptographic library has been a difficult task, and many of the bugs found in security applications like TLS turn out to be in this underlying layer. These bugs are often a result of extremely complex cryptographic implementations that have been designed to achieve maximum performance. For each algorithm, there are dozens of implementations, each hand-tuned to a specific platform so the implementation can leverage vector or crypto-specific instructions. This practice\u2014known as implementation multiplexing\u2014allows a library to provide high-performance implementations on popular hardware platforms while still providing a fallback implementation that\u2019ll work on any platform. For instance, one may find several versions of the AES block cipher (opens in new tab)<\/span><\/a>, some using SSE, AVX, or NEON, or even the dedicated AES-NI collection of instructions.<\/p>\n In light of this complexity, it\u2019s no surprise existing crypto libraries have bugs. After all, who among us can truly scrutinize half a dozen slightly different assembly implementations and spot a bug\u2014for example, a forgotten carry-bit propagation\u2014that testing has an infinitesimally small chance of finding?<\/p>\n The research community has recognized this as an urgent issue and over the past few years has produced several verified implementations of individual algorithms. While these developments have advanced our understanding of the research area, they do not provide the kind of industrial-grade features developers have come to expect from popular established libraries such as Microsoft Windows Cryptography API: Next Generation (opens in new tab)<\/span><\/a>, OpenSSL\u2019s libcrypto (opens in new tab)<\/span><\/a>, or libsodium (opens in new tab)<\/span><\/a>.<\/p>\n To meet the needs and expectations of programmers today, a cryptographic library should possess three features:<\/p>\n With EverCrypt, we deliver this and more. EverCrypt comprises a comprehensive suite of algorithms that includes block ciphers, elliptic curves, and hash functions (opens in new tab)<\/span><\/a>. To build cryptographically agile applications, developers can use the EverCrypt interface to easily switch from the algorithm SHA2-256 to SHA3-512, for instance. As far as multiplexing, we\u2019ve designed EverCrypt to choose the best implementations based on the features of the processor it\u2019s running on. And we\u2019ve verified the entire provider, which distinguishes it from other libraries available today.<\/p>\n By using the F* programming language (opens in new tab)<\/span><\/a> for all our verification results, we\u2019ve enabled EverCrypt to perform verified implementation multiplexing and algorithmic agility. No matter which implementation or algorithm is called, the same cryptographic guarantees apply. For verified clients of EverCrypt, the details of multiplexing and agility are intentionally hidden, providing a clean interface that serves as a robust foundation for the subsequent layer of the pyramid. Our TLS implementation sits right above EverCrypt, and the careful design of EverCrypt directly benefits and supports the verification efforts taking place in the TLS layer.<\/p>\n Under the EverCrypt hood, we bring together HACL* and Vale-Crypto, both of which are written using domain-specific languages based on F*. HACL* is written in Low* (opens in new tab)<\/span><\/a> for verified low-level C implementations, while Vale-Crypto is written in Vale (opens in new tab)<\/span><\/a> for verified assembly implementations. Both are verified for memory safety, correctness, and side-channel resistance. Crucially, Vale and Low* algorithms are shown to implement the same specifications, meaning that the two can be brought together under the EverCrypt provider interface. The two languages can interoperate\u2014mundane, noncritical parts of an algorithm are written once in Low*, leaving more time to write and verify performance-critical code in Vale.<\/p>\n Thanks to the mixture of C and assembly code, the verification effort doesn\u2019t compromise performance. EverCrypt operates on par with, or better than, many existing offerings.<\/p>\n We built EverCrypt for our TLS implementation, but we designed the provider to be useful for a wide range of software beyond TLS, from disk encryption to instant messaging. As of this writing, several other clients use EverCrypt for their cryptographic needs.<\/p>\n As part of the work we\u2019re doing with Project Everest, we have one verified client written in F*: a Merkle tree library (opens in new tab)<\/span><\/a> usable for blockchains. Outside of Project Everest, clients include Mozilla Firefox; the WireGuard VPN; the upcoming Zinc crypto library for the Linux kernel; the MirageOS unikernel; and the Tezos blockchain. Parts of EverCrypt have been used for over a year within Microsoft in support of implementing the QUIC protocol. These clients are usually written in C and are not themselves verified; however, because they use a verified cryptographic provider, they\u2019re reducing their attack surface and improving their security and reliability.<\/p>\n As tools improve and the scope of verification expands, we hope that EverCrypt will not only show that large-scale verified libraries are attainable but also that there now exist viable alternatives to legacy libraries. With EverCrypt, developers no longer have to compromise performance for security, and it is our aspiration that many more software projects start using EverCrypt for greater assurance.<\/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 high-performance industrial-grade EverCrypt cryptographic provider, is the second in a series exploring the groundbreaking work, which is available on GitHub now. If you\u2019re reading this […]<\/p>\n","protected":false},"author":38022,"featured_media":571920,"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":"","footnotes":""},"categories":[194488],"tags":[],"research-area":[13560],"msr-region":[197900],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-570825","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-program-languages-and-software-engineering","msr-research-area-programming-languages-software-engineering","msr-region-north-america","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,663087],"related-projects":[235367],"related-events":[],"related-researchers":[{"type":"user_nicename","value":"Jonathan Protzenko","user_id":33286,"display_name":"Jonathan Protzenko","author_link":"Jonathan Protzenko<\/a>","is_active":false,"last_first":"Protzenko, Jonathan","people_section":0,"alias":"protz"},{"type":"guest","value":"bryan-parno","user_id":"429675","display_name":"Bryan Parno","author_link":"Bryan Parno<\/a>","is_active":true,"last_first":"Parno, Bryan","people_section":0,"alias":"bryan-parno"}],"msr_type":"Post","featured_image_thumbnail":"The case for verification<\/h3>\n
A high-performance industrial-grade provider\u2014minus the bugs<\/h3>\n
\n
Performance and<\/em> safety<\/h3>\n
EverCrypt\u2014TLS and beyond<\/h3>\n
![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2019\/03\/EverCrypt_Graph_Feature_Image.png\")
","byline":"Jonathan Protzenko<\/a> and Bryan Parno<\/a>","formattedDate":"April 2, 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 high-performance industrial-grade EverCrypt cryptographic provider, is the second in a series exploring the groundbreaking work,…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/570825"}],"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\/38022"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=570825"}],"version-history":[{"count":20,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/570825\/revisions"}],"predecessor-version":[{"id":576894,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/570825\/revisions\/576894"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/571920"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=570825"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=570825"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=570825"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=570825"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=570825"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=570825"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=570825"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=570825"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=570825"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=570825"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=570825"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}