Verifiable Contracts for Stack Inspection-based Sandboxing

Overview

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.
We propose formal component and method contracts for stack inspectionbased 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.

Code Samples

Prerequisite In order to verify the code samples, Spec# (version 1.0.5424) must be installed on your machine. Furthermore, ssc.exe (which can be found in the bin-directory of your Spec# installation) has to be on your path.

Publications

last update: December 8th 2006
email