Pietro Ferrara
Francesco Logozzo
Manuel Fähndrich
ABSTRACT
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, Strp, which is used to efficiently compute memory invariants. Strp 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 (e.g., Intervals or Octagons) or too expensive (Polyhedra) to be used in practice.
- R. Bagnara, P.M. Hill, and E. Zaffanella. The Parma Polyhedra Library. http://www.cs.unipr.it/ppl/.Google Scholar
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for Object-Oriented programs. In FMCO'05. Springer-Verlag, November 2005. Google ScholarDigital Library
- M. Barnett, M. Fähndrich, and F. Logozzo. Foxtrot and Clousot: Language Agnostic Dynamic and Static Contract Checking for .Net. Technical Report MSR-TR-2008-105, Microsoft Research, Redmond, WA, August 2008.Google Scholar
- M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004, 2004. Google ScholarDigital Library
- G. P. Brat and A. Venet. Precise and scalable static program analysis at NASA. In IEEE Aerospace Conference. IEEE, 2005.Google Scholar
- D. R. Cok and J. Kiniry. ESC/Java 2: Uniting ESC/Java and JML. In CASSIS 2004, 2004. Google ScholarDigital Library
- P. Cousot. The calculational design of a generic abstract interpreter. In Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77. ACM Press, January 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL '79, pages 269--282. ACM Press, January 1979. Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL '78. ACM Press, January 1978. Google ScholarDigital Library
- Manuvir Das. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI-00), pages 35--46. ACM, 2000. Google ScholarDigital Library
- N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In SAS'01, LNCS. Springer-Verlag, June 2001. Google ScholarDigital Library
- N. Dor, M. Rodeh, and M. Sagiv. CSSV: towards a realistic tool for statically detecting all buffer overflows in c. In PLDI'03. ACM Press, 2003. Google ScholarDigital Library
- M. Furr and J. S. Foster. Polymorphic type inference for the JNI. In ESOP'06. Springer-Verlag, April 2006. Google ScholarDigital Library
- B. Hackett, M. Das, D. Wang, and Z. Yang. Modular checking for buffer overflows in the large. In ACM ICSE'06. ACM Press, 2006. Google ScholarDigital Library
- M. Hirzel and R. Grimm. Jeannie: granting Java native interface developers their wishes. In OOPSLA'07. ACM, October 2007. Google ScholarDigital Library
- R. N. Horspool and J. Vitek. Static analysis of postscript code. In ICCL'92. IEEE, 1992.Google ScholarCross Ref
- M. Karr. On affine relationships among variables of a program. Acta Informatica, 6(2):133--151, July 1976.Google ScholarDigital Library
- L. Khachiyan, E. Boros, K. Borys, K. M. Elbassioni, and M. Gurvich. Generating all vertices of a polyhedron is hard. In ACM SODA'06. ACM Press, 2006. Google ScholarDigital Library
- S. Liang. Java Native Interface: Programmer's Guide and Specification. Sun Microsystems, 2001. Google ScholarDigital Library
- F. Logozzo. Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes. In VMCAI'07. Springer-Verlag, January 2007. Google ScholarDigital Library
- F. Logozzo and M. A. Fähndrich. On the relative completeness of bytecode analysis versus source code analysis. In CC'08, LNCS. Springer-Verlag, March 2008. Google ScholarDigital Library
- F. Logozzo and M. A. Fähndrich. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In ACM SAC'08 - OOPS. ACM Press, March 2008. Google ScholarDigital Library
- J. Matthews and R. B. Findler. Operational semantics for multi-language programs. In POPL'07. ACM, January 2007. Google ScholarDigital Library
- B. Meyer. Object-Oriented Software Construction (2nd Edition). Professional Technical Reference. Prentice Hall, 1997. Google ScholarDigital Library
- A. Miné. The octagon abstract domain. In WCRE 2001. IEEE Computer Society, October 2001.Google ScholarCross Ref
- M. Müller-Olm and H. Seidl. A note on karr's algorithm. In Springer-Verlag, editor, ICALP'04, LNCS, 2004.Google Scholar
- R. Rugina and C. R. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI-00), volume 35.5 of ACM Sigplan Notices, pages 182--195, N.Y., June 18-21 2000. ACM Press. Google ScholarDigital Library
- R. Rugina and M. C. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. ACM Transactions on Programming Languages and Systems, 27(2):185--235, 2005. Google ScholarDigital Library
- D. A. Schmidt. The internal and external logic of abstract interpretations. In VMCAI'08. Springer-Verlag, January 2008. Google ScholarDigital Library
- A. Simon and A. King. Analyzing string buffers in c. In AMAST'02, LNCS. Springer-Verlag, September 2002. Google ScholarDigital Library
- A. Simon, A. King, and J. Howe. Two variables per linear inequality as an abstract domain. In LOPSTR'02, LNCS. Springer-Verlag, September 2002. Google ScholarDigital Library
- G. Tan and G. Morrisett. Ilea: inter-language analysis across java and c. In OOPSLA'07. ACM, October 2007. Google ScholarDigital Library
- D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In NDSS'00, 2000.Google Scholar
Index Terms
- Safer unsafe code for .NET
Recommendations
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 ...
Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
SAC '08: Proceedings of the 2008 ACM symposium on Applied computingWe introduce Pentagons (Pntg), a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages (IL). This abstract domain captures properties of the form of x ε [a, b]∧x < y. It is more ...
Static program analysis of embedded executable assembly code
CASES '04: Proceedings of the 2004 international conference on Compilers, architecture, and synthesis for embedded systemsWe consider the problem of automatically checking if coding standards have been followed in the development of embedded applications. The problem arises from practical considerations because DSP chip manufacturers (in our case Texas Instruments) want ...
Comments