Software Trust Assurance
Keep data secret (confidentiality), keep data safe (integrity), and keep software working (availability) by using our software assurance tools.
Hidden defects and security gaps in mission-critical or enterprise-critical software may result in injury, loss of life, financial loss, and exposure or corruption of data. When risk profile or system complexity is high, traditional test-based validation and inspection-based evaluation are not good enough. Instead, developers must offer and evaluators must verify rigorous assurances of software trustworthiness. The Galois technology portfolio incorporates program understanding, code analysis, and software provenance to assess trustworthiness of critical software systems. In order to bring these technologies to bear on complex software systems, our portfolio also includes frameworks for modeling and assessing trust relationships between system components.
Secure your C codebase:
Automated Security Analysis (ASA)
Galois’ Automated Security Analysis (ASA) technology uses advanced static program analysis to automatically prove claims regarding confidentiality and integrity in C-based systems.
Ensure correct ASN.1 data translation among computers:
High Assurance ASN.1 Workbench (HAAW)
The Internet, telecomm backbones, large-scale government networks, and home and small business networks depend on the assumption that data received by one computer are the same as data originally transmitted to it by another. ASN.1 is an abstract data description language used to describe data in a machine-independent manner and allow generation of translation code used at network interfaces. Elements of Galois’ High Assurance ASN Workbench (HAAW) automatically generate data test suites for verifying ASN.1 translation engines.
Capture cryptographic specifications, verify cryptographic implementations:
Designing cryptographic hardware correctly, while trading off time, space, and power, is expensive and time-consuming. Verifying that a hardware implementation implements a cryptographic algorithm specification correctly is equally challenging. The Cryptol domain-specific language (DSL) tool suite offers compelling assurance of hardware correctness by providing direct compilation of abstract cryptographic algorithms into the industry-standard VHDL and Verilog hardware description languages. Cryptol tools can also verify equivalence of crypto algorithm specifications, and equivalence of HDL and Cryptol descriptions.
Verify software equivalence:
Software Analysis Workbench (SAW)
The Software Analysis Workbench (SAW) provides analysts with the ability to extract formal models from programs, and analyze them using a variety of automated reasoning tools.
Identify network configuration problems:
Improperly configured networks can suffer reduced performance, increased outages, and be at extra risk of debilitating attacks. Unfortunately, network configuration remains at best a task for highly skilled experts. Nettle includes a family of domain-specific languages that allow for expression of high-level network routing and configuration policies.