Safer unsafe code for .NET

Abstract

The.NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typi-cally 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 sin-gle piece of unsafe code may corrupt memory and destabi-lize the entire runtime or allow attackers to compromise the security of the platform. We present a new static analysis based on abstract in-terpretation to check memory safety for unsafe code in the.NET framework. The core of the analysis is a new numeri-cal abstract domain, Strp, which is used to efficiently com-pute memory invariants. Strp is combined with lightweight abstract domains to raise the precision, yet achieving scala-bility. We implemented this analysis in Clousot, a generic static analyzer for.NET. In combination with contracts ex-pressed 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 as-semblies of the.NET framework. We compare our results with those obtained using existing domains, showing how they are either too imprecise (e.g., Intervals or Octagons) or too expensive (Polyhedra) to be used in practice.