| This dissertation pushes the boundary between textual and visual expression in a new way. We focus on the issue of writing specifications using a visual notation, and we describe two visual languages for this purpose. These languages provide users with the ability to formally specify security properties of a file system. Relative to previous text-based approaches to security specification, our use of a visual notation yields specifications that are more clear and concise. Moreover, since we formally define the semantics of our languages, every well-formed picture also has a precise meaning, and each can be processed by a computer. Our thesis is that visual languages can be practical and useful, even on a large scale, if they are targeted to sufficiently restricted domains of interest.; We focus on two different aspects of the security domain. First, we use the instance language to specify security configurations, that is, fixed access relationships between users and files on a file system. Since these specifications can be both read and written, they give users the ability to determine the access rights granted on their files and to modify those rights. Second, we use the constraint language to specify security policies, each of which determines a (possibly infinite) set of legal configurations. Systems administrators can use the constraint language to experiment with different policies. In fact, one important application of the constraint language is that it provides systems administrators with a vocabulary for specifying and automatically detecting potential security holes.; The semantics of both the instance language and the constraint language suggest natural computational problems, each of which raises interesting algorithmic questions. Central to our work is the design and implementation of efficient algorithms for processing pictures drawn in these languages. We describe a set of software tools we have developed, including a visual language compiler. In conjunction with the visual languages themselves, these tools give users an easy way to specify and process security configurations and policies. |
