SAFECode: A Platform for Developing Reliable Software in Unsafe Languages

Опубликовано 6 сентября 2016, 6:24

A vast majority of current software is written in weakly typed languages such as C and C++. These unsafe languages provide very weak semantic guarantees due to the possibility of undetected memory errors such as dangling pointer references, array bounds overflow and arbitrary casting between types. This failing has two major implications. The first, which has been studied previously, is that systems written in these languages are vulnerable to security attacks. The second, which is perhaps more important in the context of developing reliable software, is that most software analysis and verification tools assume the absence of memory errors and so cannot provide any guarantees on software written in these languages. In this talk, I'll describe a compiler and runtime system called SAFECode, which enables development of reliable software in unsafe languages. SAFECode operates in two different modes with varying levels of guarantees and run-time overheads. In the first mode, SAFECode detects (nearly) all memory errors including dangling pointer dereferences at run-time. In this talk, I'll present two novel techniques that SAFECode uses to detect array bounds violations and dangling pointer dereferences. Both techniques are backwards-compatible, fully automatic and require no source changes. Experiments show that the bounds checking technique has low overhead than previous techniques and is applicable to most C programs. The dangling pointer detection technique, however, has low overheads only when the frequency of heap allocation/deallocation is not high (regardless of the memory access frequency). In the second mode, SAFECode can guarantee memory safety and sound alias analysis for nearly arbitrary C programs without actually detecting dangling pointer dereferences (while retaining explicit memory deallocation). Experiments show that this approach has even lesser overhead than previous techniques. We formalize this approach using a type system, define operational semantics, and prove that the approach is sound for a subset of C. I'll present the main insights behind this approach and briefly discuss our formalism. I'll then show that our semantics provide a foundation for other software verification tools to be applied to C programs with a guarantee of soundness.