Safer unsafe code for .NET

The .NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typically called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of code as unsafe. Writing unsafe code can be useful where the rules of managed code are too strict. The obvious drawback of unsafe code is that it opens the door to programming errors typical of C and C++, namely memory access errors such as buffer overruns. Worse, a single piece of unsafe code may corrupt memory and destabilize the entire runtime or allow attackers to compromise the security of the platform.

We present a new static analysis based on abstract interpretation to check memory safety for unsafe code in the .NET framework. The core of the analysis is a new numerical abstract domain, Stripes, which is used to efficiently compute memory invariants. Stripes is combined with lightweight abstract domains to raise the precision, yet achieving scalability.

We implemented this analysis in Clousot, a generic static analyzer for .NET. In combination with contracts expressed in Foxtrot, an MSIL based annotation language for .NET, our analysis provides static safety guarantees on memory accesses in unsafe code. We tested it on all the assemblies of the .NET framework. We compare our results with those obtained using existing domains, showing how they are either too imprecise (eg, Intervals or Octagons) or too expensive (Polyhedra) to be used in practice.