Completed
Is our code perfectly secure? Depends on various modeling assumptions
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Project Everest - Fast, Correct, and Secure Software for Deployment Now
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Microsoft Research
- 3 The HTTPS Ecosystem is critical
- 4 The HTTPS Ecosystem is complex
- 5 High-Profile TLS Attacks
- 6 Defenses against specific coding errors • Compiler warnings
- 7 Static analysis - Find bugs by code analysis
- 8 State-machine verification • Compact implementation of TLS in C • Formal specification of the state machine
- 9 Program Proof for Correctness and Security What we do • Mathematical specification of security and correctness properties
- 10 Everest Verified Components in C and asm - Vale Crypto
- 11 Is our code perfectly secure? Depends on various modeling assumptions
- 12 Verified open source components in C and assembly
- 13 Parser research? So 1980s?
- 14 Verified components: the crypto library
- 15 EverCrypt: a cryptographic provider
- 16 Multiplexing: many implementations, one API
- 17 Application components for Azure Confidential Computing Open Enclave
- 18 TLS 1.3 & QUIC Standardization
