Pietro Ferrara, Francesco Logozzo, and Manuel Fähndrich
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.
|Published in||Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08)|
|Publisher||Association for Computing Machinery, Inc.|
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or firstname.lastname@example.org. The definitive version of this paper can be found at ACM’s Digital Library --http://www.acm.org/dl/.
Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.