« BACK TO PROGRAM

Proving memory safety of C programs

Henny Sipma, Kestrel Technology, LLC

Heartbleed demonstrated that lack of memory safety is still a problem. Bug finders have made large strides in recent years, but they are not exhaustive and memory corruptionn vulnerabilities continue to be exploited today at large scale. In this talk we present a mathematical approach for analyzing C source code that has the ability to provide full assurance for memory safety. The methodology takes the C standard as its specification and creates proof obligations that assert the necessary preconditions for safe execution for all language constructs that can lead to undefined behavior. Proofs of these proof obligations provide explicit and auditable evidence of full memory safety.

The methodology has been implemented in the KT Advance Analyzer and has been applied to more than a million lines of open-source C code. We discuss the challenges of the last mile in reaching 100% proof obligation discharge for legacy code, the opportunities for improving analyzability of new projects and the side benefits of enhanced maintainability and automatic generation of API documentation that the methodology offers.

Download this presentation

About Henny Sipma

Henny Sipma is CTO of Kestrel Technology, a small company that specializes in sound static analysis of source and binary code based on the theory of abstract interpretation. Henny has been working in the area of formal methods and program analysis for 25 years, both in academia, where she co-authored more than 50 conference and journal papers on program analysis, and in industry. She is the lead designer and developer of KT Advance. She holds a PhD in computer science from Stanford University.