Toaster example

Download the toaster example here. The following files are included in this zip-file:

IPermission.ssc: source code of IPermission
ToasterPermission.ssc: source code of ToasterPermission
PermissionSet.ssc: source code of PermissionSet
Toaster.ssc: source code of a toaster library component
ToasterSPS.ssc: source code of a toaster library component after applying an SPS-transformation
ToasterSPS.bpl: BoogiePL code of the transformed toaster library component
ToasterSPS_mod.bpl: fixed BoogiePL code of the transformed toaster library component
A number of .bat-files for compiling and verifying the permissions and the library component

Introduction

We define and implement a toaster library component which offers toasting services to clients. The library component shields its (sensitive) operations from being used by untrusted code by means of calls to ToasterPermissions.

This example is based on an example described in .NET Framework Security.

IPermission

New permission types can be defined by creating a new class that implements the interface IPermission. More specifically, the subclass should implement (and specify) three methods: IsSubsetOf, Intersect and Union.
Run compileipermission.bat to compile this interface to a dll.

ToasterPermission

We define a new permission type: ToasterPermission. ToasterPermissions have three parameters:

Information: the right to acquire information about the state of the toaster
Eject: the right to eject bread from the toaster
Level: the maximum toastedness (level) at which bread may be ejected

All these parameters can be set when constructing a ToasterPermission and are immutable from then on.

Note that all ToasterPermission methods are marked as Pure, meaning that these methods are side-effect free and can hence be used in specifications. Our definition of side-effect free differs slightly from the one used in Spec#, as we allow object creation in a pure context.

Run compiletoasterpermission.bat to compile this class to a dll.

PermissionSet

A PermissionSet object is a set of permissions, that can contain at most one object of each permission type. PermissionSet provides a number of (pure) methods:

ContainsPermissionOf(Type t): check whether the set contains an element with type t
GetPermission(Type t): returns a copy of the element in the set with type t
AddPermission(IPermission p): returns a copy of the original permission set that also contains p
Intersect(PermissionSet other): returns the intersection of this permission set and another given permission set
Union(PermissionSet other): returns the union of this permission set and another given permission set
...

Run compilepermissionset.bat to compile this class to a dll. Notice that both IPermission and PermissionSet are part of a built-in library and must not be provided or compiled by developers. In the .NET framework they are part of the Base Class Library.

Due to some limitations in the current version of Spec#, we introduced some pecularities in our code:

Instead of using constructors, we use static methods. Spec# does not allow the use of constructors in specifications.
The specifications of some methods have been commented out because they cannot be parsed by the Spec# compiler and/or verifier. We insert them in BoogiePL-code where neccessary.

Library Component: Toaster

We define a library component whose source-code can be found in Toaster.ssc. This library offers toasting services to clients, but guards these sensitive services by access control checks (Demands). For example, the body of ContainsBread is guarded by the invocation of Demand on a ToasterPermission. Callers who lack the required permissions are not able to access the sensitive services.

The library component has a component-level contract and a number of method level-contracts. The component-level contracts declares that the component must receive at least ToasterPermission (with the right to get information and the right to eject bread with level less than or equal to 5) in order to run properly. The method level contracts specify what permissions are required by callers of the toaster component.

To verify the correctness of the library component versus its specification, we must apply the following steps:

We first apply a Security-passing style transformation. The result of applying this transformation to Toaster.ssc is ToasterSPS.ssc.
We then generate the BoogiePl-code for the transformed component using generatetoasterbpl.bat. A new file ToasterSPS.bpl should have been created.
We introduce a number of axioms and functions in ToasterSPS.bpl:
- Missing Functions: Spec# generates a Boogie-PL function for every pure method that is used in specification. Our solution needs a function for every pure method, not just for functions used in specifications. Therefore, we inserted a number of "missing" function declarations.
- GetType Axioms: We introduced two extra axioms for reasoning about the method System.Object.GetType.
- Typing Axioms: In the translation from Spec# source code to Boogie-PL, some information about types is lost. We reintroduced some of this information by inserting additional axioms. For example, for the method CreateToasterPermission, the added axiom states that the result is an object with type ToasterPermission.
- Postcondition Axioms: For Spec# to be able to reason about method-calls in specifications, we introduce axioms describing the result of these method-calls. One axiom is introduced for each postcondition of every pure method. To ensure adding these axioms will not result in unsoundness, permission are immutable (the heap does not change when calling methods on permissions) and we make sure that permission references are never directly compared (only using Equals).
- Inheritance Axioms: Finally, we insert a number of axioms that help Spec# reason about inheritance. Each of these axioms states that if Spec# knows that an object o has type T, then it may rely on the method specifications of T (instead of relying on the method specifications of supertypes of T, which are weaker) when reasoning about o.
The result is ToasterSPS_mod.bpl.
We can now perform the actual verification by calling verifytoaster.bat. Verification of the library component will succeed.

last update: November 1th 2005
email