A Semantic Base for Verifying the Security of a Computer SystemReport
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
All rights reserved (no additional license for public reuse)
Himmick, S. "A Semantic Base for Verifying the Security of a Computer System." University of Virginia Dept. of Computer Science Tech Report (1992).
University of Virginia, Department of Computer Science