LaSCO


Introduction

LaSCO, the Language for Security Constraints on Objects, is a formal mechanism based on graphs for specifying security policies. In particular, LaSCO policies specifies constraints on what is allowed on systems that can be modeled as object-oriented.

We consider the system to consist of objects with attribute values and method invocations (events) with paramater values. We look at the system as a graph with the objects as node and the events as edges, where the originator of the invocation is the source of the node and the recipient is the destination.

LaSCO policies are annotated graphs that are matched to the system graph and which is then checked for adherence to the policy. Nodes in the policy graph match system nodes and edges in the policy graph match system edges, and the sources and destinations of the edges must match up. Predicate annotations are placed on nodes and edges to restrict the system items they match to a subset. The predicates are logical expressions which may refer to object attributes, event paramaters, constants, and policy-wide variables. Domain predicates help find the places in which the policy applies and Requirement predicates check to see if the policy requirements are upheld.

Our goal is to provide a formal mechanism able to specify policies for a wide variety of systems that is clearly defined and whose semantics are fully defined. It is hoped that the visual nature of the language will serve as an aid to human specifier of the policy and that the language's formal nature will aid users which wish to formally reason about specified policies and software implementing the policy. We have defined a formal operational semantics for the language, have a prototype policy enforecment mechanism implemented for Java, and have a design for an implementation to GrIDS.

Additional information


Jim Hoagland 2000-03-15