{"id":2603,"date":"2020-07-06T07:00:01","date_gmt":"2020-07-06T14:00:01","guid":{"rendered":"https:\/\/blog.mozilla.org\/security\/?p=2603"},"modified":"2020-07-06T08:37:03","modified_gmt":"2020-07-06T15:37:03","slug":"performance-improvements-via-formally-verified-cryptography-in-firefox","status":"publish","type":"post","link":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/","title":{"rendered":"Performance Improvements via Formally-Verified Cryptography in Firefox"},"content":{"rendered":"<div style=\"display:none\"><\/div>\n<p style=\"text-align: left;\">\nCryptographic primitives, while extremely complex and difficult to implement, audit, and validate, are critical for security on the web. To ensure that NSS (Network Security Services, the cryptography library behind Firefox) abides by Mozilla\u2019s <a href=\"https:\/\/www.mozilla.org\/en-US\/about\/manifesto\/\">principle<\/a> of user security being fundamental, we\u2019ve been working with <a href=\"https:\/\/project-everest.github.io\/\">Project Everest<\/a> and the <a href=\"https:\/\/github.com\/project-everest\/hacl-star\">HACL*<\/a> team to bring formally-verified cryptography into Firefox.<\/p>\n<p>In Firefox 57, we introduced <a href=\"https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/verified-cryptography-firefox-57\/\">formally-verified Curve25519<\/a>, which is a mechanism used for key establishment in TLS and other protocols. In Firefox 60, we added ChaCha20 and Poly1305, providing high-assurance authenticated encryption. Firefox 69, 77, and 79 improve and expand these implementations, providing increased performance while retaining the assurance granted by formal verification.<\/p>\n<h3>Performance &amp; Specifics<\/h3>\n<p>For key establishment, we recently replaced the 32-bit implementation of Curve25519 with one from the <a href=\"http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/FiatCryptoSP19.pdf\">Fiat-Crypto<\/a> project. The arbitrary-precision arithmetic functions of this implementation are proven to be functionally correct, and it improves performance by nearly 10x over the previous code. Firefox 77 updates the 64-bit implementation with new HACL* code, benefitting from a ~27% speedup. Most recently, Firefox 79 also brings this update to Windows. These improvements are significant: <a href=\"https:\/\/telemetry.mozilla.org\/new-pipeline\/dist.html#!cumulative=0&amp;end_date=2020-06-15&amp;include_spill=0&amp;keys=__none__!__none__!__none__&amp;max_channel_version=nightly%252F79&amp;measure=SSL_KEA_ECDHE_CURVE_FULL&amp;min_channel_version=null&amp;processType=*&amp;product=Firefox&amp;sanitize=1&amp;sort_by_value=0&amp;sort_keys=submissions&amp;start_date=2020-06-01&amp;table=0&amp;trim=1&amp;use_submission_date=0\">Telemetry<\/a> shows Curve25519 to be the most widely used elliptic curve for ECDH(E) key establishment in Firefox, and increased throughput reduces energy consumption, which is particularly important for mobile devices.<\/p>\n<table style=\"margin: 0 auto;\" border=\"0\">\n<tbody>\n<tr>\n<td>\n<p><div id=\"attachment_2615\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png\"><img aria-describedby=\"caption-attachment-2615\" decoding=\"async\" loading=\"lazy\" class=\"size-medium wp-image-2615\" src=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1-300x258.png\" alt=\"\" width=\"300\" height=\"258\" srcset=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1-300x258.png 300w, https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png 336w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-2615\" class=\"wp-caption-text\">64-bit Curve25519 with HACL*<\/p><\/div><\/td>\n<td>\n<p><div id=\"attachment_2617\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_32-1.png\"><img aria-describedby=\"caption-attachment-2617\" decoding=\"async\" loading=\"lazy\" class=\"size-medium wp-image-2617\" src=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_32-1-300x257.png\" alt=\"\" width=\"300\" height=\"257\" srcset=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_32-1-300x257.png 300w, https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_32-1.png 336w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-2617\" class=\"wp-caption-text\">32-bit Curve25519 with Fiat-Crypto<\/p><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<p>For encryption and decryption, we improved the performance of ChaCha20-Poly1305 in Firefox 77. Throughput is doubled by taking advantage of vectorization with 128-bit and 256-bit integer arithmetic (via the AVX2 instruction set on x86-64 CPUs). When these features are unavailable, NSS will fall back to an AVX or scalar implementation, both of which have been further optimized.<\/p>\n<div id=\"attachment_2616\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/chacha20poly1305-1.png\"><img aria-describedby=\"caption-attachment-2616\" decoding=\"async\" loading=\"lazy\" class=\"size-medium wp-image-2616\" src=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/chacha20poly1305-1-300x257.png\" alt=\"\" width=\"300\" height=\"257\" srcset=\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/chacha20poly1305-1-300x257.png 300w, https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/chacha20poly1305-1.png 337w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-2616\" class=\"wp-caption-text\">ChaCha20-Poly1305 with HACL* and AVX2<\/p><\/div>\n<p>The HACL* project has introduced <a href=\"https:\/\/eprint.iacr.org\/2020\/572\">new techniques<\/a> and <a href=\"https:\/\/eprint.iacr.org\/2017\/536\">libraries<\/a> to improve efficiency in writing verified primitives for both scalar and vectorized variants. This allows aggressive code sharing and reduces the verification effort across many different platforms.<\/p>\n<h3>What\u2019s Next?<\/h3>\n<p>For Firefox 81, we intend to incorporate a formally-verified implementation of the P256 elliptic curve for ECDSA and ECDH. Middle-term targets for verified implementations include GCM, the P384 and P521 elliptic curves, and the ECDSA signature scheme itself. While there remains work to be done, these updates provide an improved user experience and ease the implementation burden for future inclusion of platform-optimized primitives.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Cryptographic primitives, while extremely complex and difficult to implement, audit, and validate, are critical for security on the web. To ensure that NSS (Network Security Services, the cryptography library behind &hellip; <a class=\"go\" href=\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/\">Read more<\/a><\/p>\n","protected":false},"author":1725,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[69],"tags":[320796,301292,311,45514,45499],"coauthors":[327147,301291],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v22.5 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>Performance Improvements via Formally-Verified Cryptography in Firefox - Mozilla Security Blog<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Kevin Jacobs, Benjamin Beurdouche\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/\",\"url\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/\",\"name\":\"Performance Improvements via Formally-Verified Cryptography in Firefox - Mozilla Security Blog\",\"isPartOf\":{\"@id\":\"https:\/\/blog.mozilla.org\/security\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1-300x258.png\",\"datePublished\":\"2020-07-06T14:00:01+00:00\",\"dateModified\":\"2020-07-06T15:37:03+00:00\",\"author\":{\"@id\":\"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/70f5c1fa80b570beb3471f1bd0ab52d1\"},\"breadcrumb\":{\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage\",\"url\":\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png\",\"contentUrl\":\"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png\",\"width\":336,\"height\":289,\"caption\":\"64-bit Curve25519 with HACL*\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/blog.mozilla.org\/security\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Performance Improvements via Formally-Verified Cryptography in Firefox\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/#website\",\"url\":\"https:\/\/blog.mozilla.org\/security\/\",\"name\":\"Mozilla Security Blog\",\"description\":\"\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/blog.mozilla.org\/security\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"},{\"@type\":\"Person\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/70f5c1fa80b570beb3471f1bd0ab52d1\",\"name\":\"Kevin Jacobs\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/image\/8cfc33caf633741f18861dfce24d10d3\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/728c05cda6abbaa330d7045b9ecd123f?s=96&d=identicon&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/728c05cda6abbaa330d7045b9ecd123f?s=96&d=identicon&r=g\",\"caption\":\"Kevin Jacobs\"},\"description\":\"Cryptography Engineer at Mozilla\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Performance Improvements via Formally-Verified Cryptography in Firefox - Mozilla Security Blog","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/","twitter_misc":{"Written by":"Kevin Jacobs, Benjamin Beurdouche","Est. reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/","url":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/","name":"Performance Improvements via Formally-Verified Cryptography in Firefox - Mozilla Security Blog","isPartOf":{"@id":"https:\/\/blog.mozilla.org\/security\/#website"},"primaryImageOfPage":{"@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage"},"image":{"@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage"},"thumbnailUrl":"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1-300x258.png","datePublished":"2020-07-06T14:00:01+00:00","dateModified":"2020-07-06T15:37:03+00:00","author":{"@id":"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/70f5c1fa80b570beb3471f1bd0ab52d1"},"breadcrumb":{"@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#primaryimage","url":"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png","contentUrl":"https:\/\/blog.mozilla.org\/security\/files\/2020\/07\/curve25519_64-1.png","width":336,"height":289,"caption":"64-bit Curve25519 with HACL*"},{"@type":"BreadcrumbList","@id":"https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-via-formally-verified-cryptography-in-firefox\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/blog.mozilla.org\/security\/"},{"@type":"ListItem","position":2,"name":"Performance Improvements via Formally-Verified Cryptography in Firefox"}]},{"@type":"WebSite","@id":"https:\/\/blog.mozilla.org\/security\/#website","url":"https:\/\/blog.mozilla.org\/security\/","name":"Mozilla Security Blog","description":"","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/blog.mozilla.org\/security\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"},{"@type":"Person","@id":"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/70f5c1fa80b570beb3471f1bd0ab52d1","name":"Kevin Jacobs","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/blog.mozilla.org\/security\/#\/schema\/person\/image\/8cfc33caf633741f18861dfce24d10d3","url":"https:\/\/secure.gravatar.com\/avatar\/728c05cda6abbaa330d7045b9ecd123f?s=96&d=identicon&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/728c05cda6abbaa330d7045b9ecd123f?s=96&d=identicon&r=g","caption":"Kevin Jacobs"},"description":"Cryptography Engineer at Mozilla"}]}},"_links":{"self":[{"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/posts\/2603"}],"collection":[{"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/users\/1725"}],"replies":[{"embeddable":true,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/comments?post=2603"}],"version-history":[{"count":0,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/posts\/2603\/revisions"}],"wp:attachment":[{"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/media?parent=2603"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/categories?post=2603"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/tags?post=2603"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blog.mozilla.org\/security\/wp-json\/wp\/v2\/coauthors?post=2603"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}