Item Details

A Semantic Base for Verifying the Security of a Computer System

Himmick, S
Format
Report
Author
Himmick, S
Abstract
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
Language
English
Date Received
20121029
Published
University of Virginia, Department of Computer Science, 1992
Published Date
1992
Collection
Libra Open Repository
Logo for In CopyrightIn Copyright

Availability

Access Online