Project Everest - Fast, Correct, and Secure Software for Deployment Now

Explore a comprehensive conference talk on Project Everest, a collaborative research initiative aimed at developing high-performance, standards-based secure communication components with mathematical proofs of correctness and security. Learn about the project's goals, including the creation of verified TLS and QUIC implementations, and discover how F* programming language is used to co-develop programs and proofs. Gain insights into the various security guarantees provided, such as memory safety, functional correctness, and side-channel resistance. Examine the open-source tools and verified components, including EverCrypt, EverParse, and EverQuic-transport, and their adoption by major projects like Firefox and Windows. Delve into the speakers' backgrounds and expertise in type systems, language design, and software verification. Understand the complexities of the HTTPS ecosystem, high-profile TLS attacks, and various defense mechanisms. Explore topics such as static analysis, state-machine verification, and program proofs for correctness and security. Discover the project's approach to cryptographic implementations, parser research, and the development of verified components for Azure Confidential Computing.

Intro
Microsoft Research
The HTTPS Ecosystem is critical
The HTTPS Ecosystem is complex
High-Profile TLS Attacks
Defenses against specific coding errors • Compiler warnings
Static analysis - Find bugs by code analysis
State-machine verification • Compact implementation of TLS in C • Formal specification of the state machine
Program Proof for Correctness and Security What we do • Mathematical specification of security and correctness properties
Everest Verified Components in C and asm - Vale Crypto
Is our code perfectly secure? Depends on various modeling assumptions
Verified open source components in C and assembly
Parser research? So 1980s?
Verified components: the crypto library
EverCrypt: a cryptographic provider
Multiplexing: many implementations, one API
Application components for Azure Confidential Computing Open Enclave
TLS 1.3 & QUIC Standardization