DEF CON 30 - Adam Zabrocki, Alex Tereshkin - Exploitation in the era of Formal Verification

For decades, software vulnerabilities have remained an unsolvable security problem regardless of years of investment in various mitigations, hardening and fuzzing strategies. In the last years there have been moves to formal methods as a path toward better security. Verification and formal methods can produce rigorous arguments about the absence of the entire classes of security bugs, and are a powerful tool to build highly secure software. AdaCore/SPARK is a formally defined programming language intended for the development of high integrity software used in systems where predictable and highly reliable operation is crucial. The formal, unambiguous, definition of SPARK allows a variety of static analysis techniques to be applied, including information flow analysis, proof of absence of run-time exceptions, proof of termination, proof of functional correctness, and proof of safety and security properties. In this talk we will dive-into AdaCore/SPARK, cover the blind spots and limitations, and show real-world vulnerabilities which we met during my work and which are still possible in the formally proven software. We will also show an exploit targeting one of the previously described vulnerabilities.