Exploitation in the Era of Formal Verification
Adam Zabrocki and Alex Tereshkin examine software exploitation in formally verified systems, identifying design flaws and specification gaps that bypass proofs.
Summary
The Promise and Reality of Formal Software Verification
Formal verification mathematically proves that a software implementation adheres strictly to a specified formal model, aiming to eliminate entire classes of implementation bugs.
Analyzing Specification Gaps and Unverified Assumptions
Adam Zabrocki and Alex Tereshkin explore how subtle discrepancies between formal specifications and real-world hardware execution create exploitable attack vectors.
Developing Exploits Against Formally Verified Codebases
The authors demonstrate weaponizing memory corruption, timing side channels, and hardware fault injection against verified cryptographic routines and hypervisors.
Refining Formal Models for Real-World Security
The presentation offers recommendations for aligning mathematical security models with actual physical hardware execution constraints.
Related talks
Main Stage·57 min
Atlas
Atlas details atlas: Remedial Heap Overflows: dlmalloc style Sometimes even the top dudes need a refresher course.
Main Stage·46 min
Dr. Cyrus Peikari · Seth Fogie
Dr. Cyrus Peikari and Seth Fogie explores hacking .net server at DEF CON 10, examining dotnet-security and practical defenses.
CSIT Village·40 min
Kenneth Huang Shaoqi
Kenneth Huang Shaoqi examines compilers generate all our code, but they don’t get it right all the time.