A development environment and static analyses for GUARDOL - a language for the specification of high assurance guards

Abstract

There are a number of network situations where different networks have different security policies and still need to share information. While it is important to allow some data to flow between the two networks, it is just as important that they don't share any data that violates the respective security policies of the networks. Constraints on data sharing are often phrased in terms of classification levels of data (e.g. top secret, secret, public). They might also be stated in terms of the contents of the data (e.g. are there military base names, is the location correct). The software and hardware that works to solve these problems is called Cross Domain Solutions (CDS). There are a variety of hardware platforms capable of implementing CDS. These platforms are all configured in different ways and they are often proprietary. Not only are there a number of platforms on the market, many are difficult to understand, verify, or even specify. The Guardol project provides an open, non-proprietary, and domain-specific language for specifying CDS security policies and implementing CDS. Guardol is designed to be easy to understand and verify. This thesis describes the design and implementation of primary Guardol components. It includes a description of the Eclipse GUI plug-ins that have been developed for the project as well as a description of new formal analyses and translations that have been developed for the language. The translation is used to plug into external tools for model checking and the analyses help to make the translation clean and efficient. The analyses are also useful tools to help make the use of Guardol easier for developers.