Item Details

Print View

A Semantic Base for Verifying the Security of a Computer System

Himmick, S
Himmick, S
Nearly all the projects to design secure computer systems for processing classified information have had a formal mathematical model for security as part of the top - level definition of the system. Such a model functions as a concise and precise definition of the desired behavior of the security-relevant portions of the system. This thesis proposes one such model based on the take - grant protection model which describes the access control facilities for shared resources in computer systems. The current state of the system is given by a finite, directed labelled protection graph G(V, E). V is the set of vertices and E the set of edges, where labels include a finite set of rights. First, we show how the extensions made to the takegrant model permit revocation and confinement. Second, a number of results are derived in the form of theorems to be applied to a protection graph. They show how access rights may be transmitted in that graph, It is possible to determine in linear-time in the size of the graph if a given node can obtain rights to another one. An algorithm to do so is presented. Finally, a definition of a "trusted component" in a system is proposed and it is shown how it is possible to characterize that "trust" in our model. iii Note: Abstract extracted from PDF file via OCR
Date Received
University of Virginia, Department of Computer Science, 1992
Published Date
Libra Open Repository
In CopyrightIn Copyright
▾See more
▴See less


Access Online