Master of Science / Department of Computing and Information Sciences / John M. Hatcliff / Guardol, 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.