Hoag, Jonathan2011-01-182011-01-182011-01-18http://hdl.handle.net/2097/7077Guardol, a domain-specific language (DSL) developed by Rockwell Collins, was designed to streamline the process of specifying, implementing, and verifying Cross Domain Solution (CDS) security policies. Guardol’s syntax and intended computational behavior tightly resembles the core of many functional programming languages, but a number of features have been added to ease the development of high assurance cross domain solutions. A significant portion of the formalization and implementation of Guardol’s grammar and type system was performed by the SAnToS group at Kansas State University. This report summarizes the key conceptual components of Guardol’s grammar and tool- chain architecture. The focus of the report is a detailed description of Guardol’s type system implementation and formalization. A great deal of effort was put into a formalization which provided a high level of assurance that the specification of types and data structures were maintained in the intended implementation.en-US© the author. This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).http://rightsstatements.org/vocab/InC/1.0/GuardolDomain Specific LanguageCompilerType SystemGrammarCross Domain SolutionsReportComputer Science (0984)