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

Stack inspection-based sandboxing originated as a security mechanism for safely executing partially trusted code. Today, it is widely used for the more general purpose of supporting the principle of least privilege in component-based software development. In this more general setting, the permissions required by a component to run properly, or the permissions needed by other components to successfully call methods in a given component are conceptually part of the interface specification of the component. Hence, correct documentation of this part of the interface is essential. 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 theNET Framework, called Code Access Security. Our system relies on the Spec# programming language and its accompanying static verification tool.Special issue: .NET Technologies 2005 Conferencestatus: publishe