Dr. Greg Morrisett
Much of our computing infrastructure is still built using C and C++, in spite of overwhelming language-level errors 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 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) that have low overhead, and guarantee to enforce a particular security policy. However, the SFI policy is 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.
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