Verifying code using automated reasoning
summary
AWS describes how Kani, an open-source Rust verification engine, translates Rust code (including unsafe blocks) into symbolic logic and uses bounded model checking plus SMT solving to prove absence of panics, overflows, and out-of-bounds accesses. Examples show Kani finding a multiplication-overflow bug in a power-of-two resize routine, checking optimized vs reference implementations, and catching a Firecracker bandwidth bug and issues in S2N-QUIC; proofs return counterexamples or full verification in seconds. Kani S2N-QUIC Firecracker
AI-written summary · about
chapters (14)
- 0:00Introduction to the session
- 1:00What is automated reasoning?
- 2:38Historical context
- 6:11Testing vs. reasoning
- 8:21Amazon's approach
- 10:00Rust and unsafe code
- 14:02Introducing Kani
- 17:49Kani deep dive
- 20:09The logic behind proofs
- 24:39Practical tool usage
- 28:12Proof-guided development
- 37:26Model building mechanics
- 40:45Takeaways and limitations
- 43:57Conclusion and resources
related talks
01h 02mReasoning about Security of Amazon Web Services
30mLightweight Runtime Security Policy Verification Using an Embeddable C++ miniKanren
15mAutomated Verification of Network Function Binaries
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
10m"Verifying Memory Safety for the Rust Standard Library"
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
24mKubernetes Operators: Safety First Through Model Checkers