Guardol
A guard is a device that mediates information sharing over a network between security domains according to a specified policy. Typical guard operations include reading field values in a packet, changing fields in a packet, transforming a packet by adding new fields, dropping fields from a packet, constructing audit messages, and removing a packet from a stream. Guards are becoming prevalent, for example, in coalition forces networks, where selective sharing of data among coalition partners in real time is essential. One such guard, the Rockwell Collins Turnstile high-assurance, cross-domain guard, provides directional, bi-directional, and all-way guarding for up to three Ethernet connected networks.
The proliferation of guards in critical applications, each with its own specialized language for specifying guarding functions, has led to the need for a portable, high-assurance guard language.
Guardol is a new, domain-specific programming language aimed at improving the creation, verification, and deployment of network guards. Guardol supports a wide variety of guard platforms, and features the ability to glue together existing or mandated functionality; the generation of both implementations and formal analysis artifacts; and sound, highly automated formal analysis. Messages to be guarded, such as XML, may have recursive structure; thus a major aspect of Guardol is datatype declaration facilities similar to those available in functional languages such as SML or Haskell. Recursive programs over such datatypes are supported by ML-style pattern matching. However, Guardol is not simply an adaptation of a functional language to guards. In fact, much of the syntax and semantics of Guardol is similar to that of Ada: Guardol is a sequential imperative language with non-sidee ecting expressions, assignment, sequencing, conditional commands, and procedures with in/out variables. To a first approximation Guardol = Ada + ML. This hybrid language supports writing complex programs over complex data structures, while also providing standard programming constructs from Ada.
Tools
RADA is an open source and highly portable tool to reason about algebraic data types. The reasoning is based on creating an abstraction of the data type via a catamorphism (fold) function. The syntax for reasoning problems is presented as an extension of the SMT-Lib 2.0 format, supporting integration with tools that use this format. RADA uses a catamorphism unrolling algorithm and currently supports CVC4 and Z3 as underlying reasoning engines. Our project presents a new version of RADA, which was completely rewritten from scratch using Java and ANTLR 4.