Reasoning about Security of Amazon Web Services
summary
Amazon Web Services adopts formal verification across design and operation, proving distributed key protocols and TLS code, and using Zelkova to check IAM policies at millions of calls per day. The team reduces protocol proofs to object‑oriented reasoning, uses bounded model checking (CBMC) to prove bootloader memory safety, and applies SAW/LLVM-style proofs to an s2n TLS implementation including a timing-mitigation. Work scales rapidly — cloud growth is ~45% year‑over‑year — and automated checks are integrated into deployment pipelines.
AI-written summary · about
chapters (9)
- 0:00Introduction to AWS and cloud
- 3:08The scale and business of AWS
- 14:36Formal methods in the cloud
- 18:20Operationalizing formal methods
- 24:03Security protocol verification
- 35:25Customer security and tools
- 42:15Virtual network security
- 45:32Future work and collaboration
- 54:13Q&A session
