The Everest project is a joint effort between Microsoft Research, INRIA, and CMU to build a formally verified replacement for core HTTPS components, including the TLS protocol, cryptographic primitives, and certificate processing. The goal is to build an efficient implementation of these components, and the cryptographic primitives are especially critical to performance. Therefore, the project has developed verified hand-written assembly language implementations of common cryptographic primitives such as AES, SHA, and Polyl305. This talk will present an overview of Everest, its verified assembly language cryptography, and the tools used to verify the code, including Vale, Dafny, F~*, and Z3. It will discuss challenges in using such tools to verify low-level cryptographic code, including the need to reason about bit-level operations, large integers, and polynomials. A key challenge is the speed of the verification, and the talk will discuss ongoing efforts to combine tactics with SMT solving to make verification fast without sacrificing automation.
展开▼
