Abstract
We describe a system called Miro 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 article is a case study of the Miro languages and tools. We show how to represent various UNIX security constraints-including those described in a well-known paper on UNIX security 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.