Crowd Sourced Formal Verification
Memory errors such as buffer overruns are notorious security vulnerabilities. There is considerable interest in ensuring safety of compiled code, either through static verification or through instrumented runtime checks. Since static verification has so far proved impractical, this project focuses on improving runtime code instrumentation.
Runtime memory sanitization is available in several compilers, which employ the strategy of inserting additional code to ensure various classes of safety, such as checking if an array is accessed beyond its declared bounds, or checking if a memory access might be corrupted due to integer overlow following an arithmetic operation on an index. While these strategies are effective in eliminating the vulnerability, they are can be very expensive in terms of performance, resulting in performance overhead of factors of two to fifty, unacceptable in production code.
These runtime checks incur severe performance penalties because they are applied indiscriminately for every access. Significant overhead savings are achieved by eliminating checks that can be proved to be unnecessary, under sound static analysis using research tools outside the compiler.
We have developed plugins for external analysis frameworks (Frama-C and CodeSurfer) to create annotations describing proven code constraints, and to insert the annotations into C source code. We then provide straightforward compiler plugins to omit check insertion, based on the proven sound annotations. The result is vulnerability defenses that are efficient and scalable.
Applying this protocol to a dozen benchmarks, both large and small, demonstrates improvements in runtime performance that make incorporation of runtime checks a viable option for defenses.
Participating Institutions: Heading link
Sponsor: Heading link
Publications: Heading link
- Kedar S Namjoshi and Lenore D Zuck. Witnessing program transformations. In Francesco Logozzo and Manuel Fahndrich editors, Static Analysis. Lecture Notes in Computer Science 7935, 304–323. Springer Berlin Heidelberg, 2013.
- Rigel Gjomemo, Kedar S. Namjoshi, Phu H. Phung, V.N. Venkatakrishnan, and Lenore D. Zuck. From verification to optimizations. In the 16th international conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, January 12–14, 2015
- Kedar S. Namjoshi, Giacomo Tagliabue, and Lenore D. Zuck, A witnessing compiler: A proof of concept.Legay and Bensalem editors. Programming and Software Engineering: Runtime Verification 8174, 340-345, 2013.
Student Reports: Heading link
- Edmund W. Ballou, Static Analysis To Improve Compiler Sanitization, Master’s Project, UIC, September 2015
- Ankh Kishore, Compiler Optimization for LLVM, Master’s Project, UIC, December 2014
- Giacomo Tagliabue, An Annotation Framework for LLVM Compiler Infrastructure, Master’s Thesis, UIC, December 2014
- Niko Zarzani, Improving Compiler Optimizations using Program Annotations, Master’s Thesis, UIC, May 2014