The course aims to teach learners how to develop fast, correct, and secure software for deployment by providing high-performance secure communication components with mathematical proofs of correctness and security. The course focuses on programming in F*, proving code memory safe, functionally correct, and side-channel resistant. The teaching method includes showcasing open-source tools like EverCrypt, EverParse, and EverQuic-transport. The intended audience for this course includes software developers, security professionals, and individuals interested in formal verification and secure software development.
Project Everest - Fast, Correct, and Secure Software for Deployment Now
Overview
Syllabus
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
Taught by
0xdade
