Basic example

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

Introduction

This example illustrates the basic idea behind our solution. To keep it as clear as possible, we make two simplifying assumptions.
  1. We assume that only a single permission exists, namely WebPermission.
  2. We assume that permission objects take no parameters.
Under these assumptions, a permission set is either the empty set or the singleton containing just WebPermission. Therefore, we can represent or encode permission sets by means of boolean variables, where false corresponds to the empty set and true to the singleton. Note that our solution supports programs using multiple, parametrized permissions; the simplifying assumptions are only made to simplify the basic example.

In this example, we consider two components: a library component and a client component. The next two sections explain how to verify both these components.

The library component

The source code of the library component is stored in Library.ssc.

Verification of this component consists of two steps:

  1. We first apply a Security-passing style transformation. The result of applying this transformation to Library.ssc is LibrarySPS.ssc.
  2. To actually verify the component, input the compiled component to Boogie (Spec#'s program verifier). Run verifylibrary.bat in order to verify.

For the library component verification will succeed, meaning that the implementation of this component complies wit its specification.

The client component

The source code of the library component is stored in Client.ssc.

Again, verification of this component consists of two steps:

  1. We first "generate" specifications based on the component-level attribute and apply a Security-passing style transformation. The result of applying this transformation to Client.ssc is ClientSPS.ssc.
  2. To verify the component, input the compiled component to Boogie. Run verifyclient.bat in order to verify.

For the client component verification will fail. Boogie will indicate that the precondition of Connect can possibly be violated within the body of the method Spy.

last update: October 18th 2005
email