Specifying and checking UNIX security constraints
Allan Heydon, J. D. Tygar · 1994
We describe a system called Mir'o for specifying and checking security constraints. Our system is general because it is not tied to any particular operating system. It is flexible because users express security policies in a formal specification language, so it is easy to extend or modify a policy simply by augmenting or changing the specification for the current policy. Finally, our system is expressive enough to describe many relations on file system configurations; however, it is not expressive enough to describe more subtle security holes like Trojan horses or weaknesses in the passwords chosen by the system's users. This paper is a case study of the Mir'o languages and tools. We show how to represent various Unix security constraints --- including those described in a well-known paper on Unix security [5] --- using our graphical specification language. We then describe the results we obtained from running our tools to check an actual Unix file system against these constraints. 1 ...