High Integrity Language Technology
ACM SIGAda’s Annual International Conference
Much of our computing infrastructure (e.g., your operating system, database, networking stack, web browser) is still built using C and C++, in spite of the overwhelming language-level errors (e.g., buffer overruns, integer overflows, double-frees, etc.) that easily lead to security exploits. For both technical and economic reasons, we can't afford to rewrite this code in a type-safe language like Java, though doing so would stop a broad class of attacks.
I will discuss a range of compiler-oriented techniques that researchers have explored to try and harden C/C++ code. In one corner of the space, we have ad hoc techniques such as stack cookies and address space layout randomization that are already deployed, and have essentially no overhead, but leave gaping holes. In another corner, we have techniques such as Software Fault Isolation (SFI) and Control Flow Isolation (CFI) that have low overhead, and guarantee to enforce a particular security policy.
However, the SFI and CFI policies are relatively coarse-grained compared to type-safety, and as such forfeit some security. In yet another corner of the space is the Secure Virtual Architecture (SVA) which enforces a fine-grained, object-level integrity policy comparable to type safety.
However, SVA and related techniques can have high overhead for some code, and will generally break more programs than SFI or CFI.
All of these techniques depend upon compiler transformations, optimizations, and/or analyses, that could lead to a large trusted computing base (TCB). So I will also discuss recent research that helps to minimize the TCB via machine-checked proofs of correctness.