Technology Catalog

Galois has developed the following technologies and capabilities for various government and commercial clients.

For more information on the technologies and how to access them, please contact us.

Trusted Services Engine (TSE)

The Trusted Services Engine (TSE) is network-enabled software appliance based on web standards that enables secure file sharing across multiple security levels. The TSE allows users at higher security levels to gain an integrated view with read-only access to un-replicated files at lower levels and read/write access to files at their own level. It is designed for high assurance (EAL 6 and PL5), including a formal proof that the secure read-down policy will be enforced by the system. The TSE is designed to be hosted on a high assurance separation kernel, and is currently hosted on Security-Enhanced Linux (SELinux).

Availability: GOTS. Contact us for access to the technology.

Related Technologies: Block Access Controller, Tearline Wiki, Cross-domain RSS

Block Access Controller (BAC)

The Block Access Controller (BAC) is a high assurance cross-domain software component that mediates access between security levels, allowing read/write access to the current security level and read access to lower security levels. The BAC includes a formal proof of key security and safety properties, in particular that only the intended information flows are possible and that error states are unreachable. The BAC comprises less than 800 lines of C code, which is generated directly from the formal model used to demonstrate these properties. This design simplicity enables cost-effective EAL 6 and PL5 level assurance claims.

Related Technologies: Trusted Services Engine, Tearline Wiki, Cross-domain RSS

Wait-Free File System (WFFS)

The Trusted Services Engine’s requirement that "read-downs" from HIGH security levels to LOW do not introduce a covert channel is a novel one for file system design. To provide high assurance separation, the TSE uses separate file systems, one per security level, without any direct communication between file systems. This complicates maintaining consistent caches between file systems, yet HIGH must access the LOW disk at any point without reading inconsistent data. The Wait-Free File System (WFFS) provides these consistency properties, which are built using a synchronization mechanism similar to "wait-free" techniques used in multiprocessor systems to synchronize access to shared memory.

Automated Security Analysis

The Automated Security Analysis (ASA) tool applies advanced program analysis techniques to find security bugs in large C codebases. The analysis focuses on calculating conditional information flow for each program function and the whole program, which helps identify bugs that compromise confidentiality, integrity, and separation. For example, the tool can find instances where data entered by the user flows to the format field of an output (printf) statement. Current ASA development work is focused on improving performance, scaling to larger code bases, and adding visualization capabilities.

Tearline Wiki

The Tearline Wiki is a cross-boundary wiki system based on the popular MediaWiki software which powers Wikipedia and Intellipedia. The Tearline Wiki can be used to collaborate across information boundaries, including those spanning multiple clearance levels. Separate knowledge repositories do not contain redundant or divergent information---data stays at its level of origin, but more privileged users can get a combined view of all of the data. The Tearline Wiki can also be used for aggregating multiple wikis. The Tearline Wiki is itself a single level component, designed for integration with a cross-domain component such as the Trusted Services Engine or Multi-Domain Dissemination System.

Advanced Wiki Technologies

Galois has developed technologies for cross-wiki cross-boundary collaboration that go beyond the Tearline concept outlined above. In particular, we have OAuth-based technology to allow wiki systems to share discretionary access control data on a per-page basis, as well as advanced merge capabilities that allow complex branching and other kinds of interaction between wiki instances. These technologies are designed to allow groups in different security domains to engage in rich collaboration without sacrificing the necessary security.

Related Technologies: Tearline Wiki, Cross-domain RSS

Cross-Domain RSS

Really Simple Syndication (RSS) is an open standard publish-subscribe protocol for change notification of events or data, commonly used to allow users to maintain a kind of situational awareness across many web sites. The Cross-Domain RSS (CD-RSS) system provides a secure multi-level and cross-domain RSS routing, filtering, search and subscription service, ensuring timely access to news and events online. It is designed for groups collaborating on secure data, giving users the ability to aggregate across protected resources without relaying private security credentials to those endpoints. The CD-RSS is itself a single level component, designed for integration with a cross-domain component such as the Trusted Services Engine or Multi-Domain Dissemination System.

Secure Federated Search Mashup

Industry and government users need to aggregate and search data that is sensitive and secured as well as data that is freely available and open. Data with different levels of access are kept isolated, either with password protection, VPNs, firewalls, or even by "air-gaps" (where each security level has its own, isolated network). Thus, searching over diverse data sets poses a problem: users cannot perform a single search that will return results from all the systems to which they have access. Indeed, virtually every user of the Internet experiences this problem to some degree. Galois is building a standards-based Secure Federated Search Mashup (S-FSM) system that elegantly satisfies these dual requirements, enabling collaboration without compromising security. This solution is compatible with standard web mashup APIs as well as "discovery" systems like RSS and other Web 2.0 tools. A standards-based approach allows our system to aggregate content from search providers who are completely unanticipated by the S-FSM system, which store data in a variety of formats, and which utilize any kind of identity, authentication, and authorization system.

Security Policy Configuration Language

Security-Enhanced Linux (SELinux) provides a very fine-grained, flexible base on which to create secure systems. But the fine grained control comes at a price: you have to specify every access right for every user, file, process, and kernel call, using a very detailed low-level configuration language. Galois’s Security Policy Configuration Language is a high-level language for defining and validating SELinux policies, and translating them to the low-level configuration language directly used by SELinux. Also included are analysis tools that detect errors in SELinux policies and perform other high-level analyses of SELinux policy modules. Current work includes extending the high-level language beyond just SELinux configuration, to specify policies for (e.g.) networked systems of SELinux boxes.

Related Technologies: Trusted Services Engine

Cryptol Language and Compiler

The Cryptol specification language was designed by Galois for the NSA as a public standard for specifying cryptographic algorithms. A Cryptol reference specification can serve as the formal documentation for a cryptographic module, eliminating the need for separate and voluminous English descriptions. Cryptol is fully executable, allowing designers to experiment with their programs incrementally as their designs evolve. Cryptol compilers can generate C, C††, and Haskell software implementations, and VHDL or Verilog HDL hardware implementations. These tools significantly reduce overall life-cycle costs by addressing the key cost drivers in the deployment of cryptographic solutions. For example, Cryptol allows engineers and mathematicians to program cryptographic algorithms on FPGAs as if they were writing software.

Related Technologies: Cryptol Verifier

Visit Cryptol for more information, including white papers, case studies, software downloads.

Cryptol Verifier

In addition to generating implementations of cryptographic algorithms, Cryptol tools can verify the faithfulness of an implementation to a reference specification, at each stage of the toolchain. Equivalence can be demonstrated between a reference Cryptol specification and a refinement of that specification, and between a Cryptol specification and a VHDL implementation, even if that VHDL was not produced by the Cryptol tools. This enables the designer to incrementally refine an implementation to trade off space, time, and other performance metrics, while ensuring correctness of each refinement.

Related Technologies: Cryptol Language and Compiler

Visit Cryptol for more information, including white papers, case studies, software downloads.

Nettle

Improperly configured computer networks can exhibit poor performance, are subject to attack by malicious agents, and are vulnerable to outages. Indeed, it has been estimated that nearly half of network outages are due to misconfiguration. Errors in configuring networks are common, as standard protocols have become increasingly complex over the years and the effect of altering various parameters is not completely understood. The Nettle technology addresses this by simplifying the expression of routing policies and automating the process of translating policies into a set of device-specific configurations. Key to Nettle is a family of domain-specific languages (DSLs) for expressing high-level network routing policies. A complete local configuration is defined in a Nettle DSL, then compiled into vendor-specific scripts and distributed to the individual routers in the network. A single source file reduces implementation errors between different routers, provides a centralized place to define and modify policy, and facilitates checking for local and global anomalies.