University of Virginia
|
|
Department of Computer
Science University of Virginia
Expressing Safety Policies |
This page is based on:
David Evans and Andrew Twyman. Policy-Directed Code Safety. 1999 IEEE Symposium on Security and Privacy, Oakland, California, May 9-12, 1999. The class of safety policies that can be expressed using Naccio is limited by the resource operations defined in the resource descriptions. We can express safety policies that constrain how these resources may be manipulated, but only in terms of information available through resources. For example, we cannot express a policy that enforces precise constraints on information flow. Further, Naccio cannot express any liveness properties (i.e., properties that constrain what must happen at some time in the future). Once an execution has reached an invalid state, it is terminated. A safety policy is described by listing safety properties and their parameters. Safety policies can be combined to define a new policy. The simplest way to combine safety policies is to create a policy that includes all safety properties of both policies. Other combination mechanisms designed to support easily modifying existing policies by strengthening or weakening particular constraints are currently under investigation. LimitWrite is a sample safety policy. It instantiates two safety properties - NoOverwrite disallows replacing or altering the contents of any existing file, and LimitBytesWritten (1000000) places a million-byte limit on the amount of data that may be written to files. These safety properties are defined as part of a standard properties library. By itself, this would not be a wise policy to use on an untrusted application since it does not constrain what files the application may read or how the application may use the network. In practice, this policy would be combined with policies that place constraints on other resources. A safety property consists of one or more check clauses that identify resource operations and provide action code for enforcing the property. For example, the check clause of the NoOverwrite property identifies the two RFileSystem resource operations associated with opening an existing file for writing (openWrite and openAppend) and the operations associated with deleting a file (preDelete). The action code simply invokes the violation command, which will produce a dialog box that alerts the user to the safety violation and provides an option to terminate the program. The LimitBytesWritten property illustrates how a more complex safety property is defined. It takes an integer limit parameter, and constrains the total number of bytes that may be written by the application to the value of that parameter. When LimitBytesWritten is instantiated in a safety policy, limit is given a value. To implement the write limit, we need to keep track of how many bytes are written. This is done by the TrackTotalBytesWritten state maintainer that is included by the requires clause. It adds a state variable to the RFileSystem resource, and provides a precode action to the RFileSystem.write operation. The body of the precode action will happen before any checking code associated with the resource operation. Hence, when the LimitBytesWritten property check action compares the value of bytes_written to the limit, the value of bytes_written has already been incremented before the comparison. We keep the state maintenance and property checking code separate, since many safety properties may require the same state.
Next - Platform Interfaces
Naccio Home Page |