Static Verification of Code Access Security Policy Compliance of .NET Applications

By: Jan Smans, Bart Jacobs, Frank Piessens

Abstract

In this paper, we propose formal component and method contracts for stack inspection-based sandboxing, and we show that formal verification of these contracts is feasible with state-of-the-art program verification tools. Our contracts are significantly more expressive than existing type systems for stack inspection-based sandboxing. We describe our solution in the context of the sandboxing mechanism in the .NET Framework, called Code Access Security. Our system relies on the Spec# programming language and its accompanying static verification tool.

Cite as:

Jan Smans, Bart Jacobs, Frank Piessens, “Static Verification of Code Access Security Policy Compliance of .NET Applications”, Journal of Object Technology, Volume 5, no. 3 (April 2006), pp. 35-58, doi:10.5381/jot.2006.5.3.a2.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access   |    Contact