CSFV

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.