You are now leaving the website that is under the control and management of DARPA. The appearance of hyperlinks does not constitute endorsement by DARPA of non-U.S. Government sites or the information, products, or services contained therein. Although DARPA may or may not use these sites as additional distribution channels for Department of Defense information, it does not exercise editorial control over all of the information that you may find at these locations. Such links are provided consistent with the stated purpose of this website.

After reading this message, click to continue immediately.

Go Back

/ Information Innovation Office (I2O)

High-Assurance Cyber Military Systems (HACMS)

The High-Assurance Cyber Military Systems (HACMS) program goal is to create technology for the construction of high-assurance cyber-physical systems, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties. Key technologies include interactive software synthesis systems, verification tools, and specification languages.

Program Manager: Dr. Raymond Richards

Contact: Contact Dr. Raymond Richards

The content below has been generated by organizations that are partially funded by DARPA; the views and conclusions contained therein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.

Report a problem:

Last updated: November 13, 2015

Rockwell Collins (publications) FM Workbench Research Integration This repository contains 1) the AADL models with verification properties for the research air vehicle (quadcopter), 2) the AGREE analysis tool for compositional verification of behavioral properties, and 3) the Resolute tool for constructing and checking assurance cases on AADL models. BSDv3
Rockwell Collins (publications) JKind model checker Research Integration JKind is a Java implementation of the KIND model checker. KIND is a parallel multi-property k-induction based model checker for Lustre programs. (Java) BSDv3
Galois, Inc. SMACCMPilot Control Systems SMACCMPilot is an open source autopilot software for small, unmanned aerial vehicles (UAVs) using new high-assurance software methods. (C) BSDv3
Galois, Inc. cbmc-reporter Control Systems cbmc-reporter is a driver for the CBMC model-checker for use in verifying C library code. cbmc-reporter helps (1) utilize multi-threading when verifying a large number of claims, (2) generate summary tables of resulting proofs, and (3) aid in build-system integration for library code (e.g., parsing function definitions from sources). (Haskell) BSDv3
Galois, Inc. Ivory Control Systems Ivory is an embedded domain-specific language for safer systems programming. Ivory is implemented as a library of the Haskell programming language. Ivory programs are written using Haskell syntax and types.Ivory is not a general purpose programming language. It aims to be a good language for writing a restricted subset of programs. Ivory gives strong guarantees of type and memory safety, and has features which allow the programmer to specify other safety properties. Ivory is well suited for writing programs which interact directly with hardware and do not require dynamic memory allocation. Ivory can be considered to be a lot like a restricted version of the C programming language, embedded in Haskell. (Haskell) BSDv3
Galois, Inc. Tower Control Systems Tower is a language for composing Ivory programs into real-time tasks. Tower is both a specification language and a code generator. A Tower program describes communication channels and tasks, and provides an Ivory implementation of each task. Tower compiles the specification for the program and delegates code generation to an operating-system specific back end. (C) BSDv3
NICTA (publications) CAmkES: Component Architectures for microkernel-based Embedded System Operating Systems The CAmkES project provides a solution for quickly and reliably building complex microkernel-based embedded systems software. BSD
NICTA (publications) WCET: Worst-case execution time computations tools Operating Systems The WCET computation is based on Chronos 4.2 and is augmented with additional code to perform control flow graph extraction, loop bound computation, and infeasible path detection. The default modelled hardware is the ARM1136 i.MX31 processor on the KZM evaluation board. This software was developed as part of research into mixed-criticality real-time systems, and has been used to compute execution time bounds for seL4. GPL
NICTA (publications) Trustworthy File Systems Operating Systems Not Ready for Release The aim of Trustworthy File Systems is to develop a methodology for the creation of correct-by-construction file systems. Open Source License TBD
Princeton University (publications) Verified Software Toolchain Operating Systems The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context. BSD, GPL
Princeton University (publications) Message-authentication enhancements to the ROS operating system Operating Systems Not Ready for Release Message-authentication enhancements to the ROS operating system. Open source license TBD
Yale University (publications) CertiKOS kernel Operating Systems Not Ready for Release CertiKOS is a new hypervisor kernel that leverages formal certification to ensure correctness and isolate critical services from noncritical components. Open source license TBD
MIT (publications) Bedrock Coq library Operating Systems Bedrock is a library that turns Coq into a tool much like classical verification systems (e.g., ESC, Boogie), but niftier. In particular, Bedrock is: (1) Low-level: You can verify programs that, for performance reasons or otherwise, can't tolerate any abstraction beyond that associated with assembly language. (2) Foundational: The output of a Bedrock verification is a theorem whose statement depends only on the predicates you choose to use in the key specifications and on the operational semantics of a simple cross-platform machine language. That is, you don't need to trust that the verification framework is bug-free; rather, you need to trust the usual Coq proof-checker and the formalization of the machine language semantics. Higher-order: Bedrock facilitates quite pleasant reasoning about code pointers as data. (3) Computational: Many useful functions are specified most effectively by comparing with "reference implementations" in a pure functional language. Bedrock supports that model, backed by the full expressive power of Coq's usual programming language. (4) Structured: Bedrock is an extensible programming language: any client program may add new control flow constructs by providing their proof rules. For example, adding high-level syntax for your own calling convention or exception handling construct is relatively straightforward and does not require tweaking the core library code. (5) Mostly automated: Tactics automate verification condition generation (in a form inspired by separation logic) and most of the process of discharging those conditions. Many interesting programs can be verified with zero manual proof effort, in stark contrast to most Coq developments. BSD
Draper Laboratory Fracture Tool / LLVM decompiler Red Team Draper's HACMS Decompiler is a software tool based on the LLVM open source compiler project. The HACMS Decompiler is a set of modifications to the LLVM compiler that make it run backwards. The HACMS Decompiler converts computer program instructions for a specific machine (binary software program) into generic machine instructions (machine-independent assembly program) called LLVM intermediate representation (IR). The HACMS Decompiler enables a user to directly analyze and modify the resulting LLVM IR. Near term additions to the HAMCS Decompiler include the ability to emit a C program representation from the IR. The HACMS Decompiler currently supports ARM architectures, however it will be extended to include X86, PowerPC, MIPS, and other ISAs as required by the program. Open Source License TBD
Draper Laboratory CSPM parser/type-checker/evaluator included in FDR3 Red Team This library provides a FDR-compliant parser, type checker and (experimental) evaluator for machine CSP files. There is also a program, cspmchecker, that makes use of this library to provide command line type checking. Open Source License TBD
SRI (publications) Evidential Tool Bus Research Integration Not Ready for Release The evidential tool bus (ETB) allows for low-cost integration of diverse tools and components into customized tool chains, and the combination of evidence from different sources into a credible assurance case. GPL
SRI (publications) High-assurance ROS modules Research Integration Not Ready for Release New high-assurance ROS modules that will provide security services, such as authentication and integrity. BSD license TBD
Kestrel Institute
UPD May 18th
Operating Systems Specware is a software engineering tool that automatically generates high-assurance software. Specware is a leading-edge automated software development system that allows users to precisely specify the desired functionality of their applications and to generate provably correct code based on these requirements. At the core of the design process in Specware lies stepwise refinement, in which users begin with a simple, abstract model of their problem and iteratively refine this model until it uniquely and concretely describes their application. BSD
University of Pennsylvania (publications) ROS based cruise controller simulator Control Systems Not Ready for Release ROS-based cruise controller simulator. GPL
University of Pennsylvania (publications) Attack-resilient implementation of cruise controllers Control Systems Not Ready for Release A constant-speed cruise control for LandShark that ensures the vehicle maintains speed when some sensors are attacked (e.g., attack on encoders & GPS spoofing). Also includes adaptive cruise control for an American Built Car based on the CarSim simulator. GPL
University of Pennsylvania (publications) Attack-resilient sensor fusion module Control Systems Not Ready for Release Ubiquitous/redundant sensors can provide additional information about system state. Low-precision sensors can be used to improve attack detection and identification. GPL
Carnegie Mellon University (publications) HACMS Spiral package Control Systems Not Ready for Release Open source Spiral package running on the core Spiral engine. Provides sensor fusion and consistency algorithms, optimized interval arithmetic, and code generation capabilities for advanced Intel instruction sets (SSE, AVX). Includes example specifications in the 'Hybrid control operator language (HCOL)' and an Eclipse-based GUI. Open Source License TBD
Carnegie Mellon University Motion Interference Detection in Mobile Robots
Carnegie Mellon University Mobile Robot Fault Detection based on Redundant Information Statistics
Carnegie Mellon University A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems
Carnegie Mellon University On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles
MIT Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier
NICTA seL4: from General Purpose to a Proof of Information Flow Enforcement
NICTA Binary Verification of an OS Microkernel
NICTA File Systems Deserve Verification Too!
NICTA Towards a Verified Component Platform
Princeton University Mostly sound type system improves a foundational program verifier
Princeton University Computational Verification of Network Programs in Coq
Princeton University Program Logics for Certified Compilers
Rockwell Collins, University of Minnesota Your What Is My How: Iteration and Hierarchy in System Design
SRI Automated Reasoning, Fast and Slow?
SRI Logic and Epistemology in Safety Classes
SRI ARSENAL: Automatic Requirements Specification Extraction from Natural Language
SRI Reasoning about the Reliability Of Diverse Two-Channel Systems In which One Channel is 'Possibly Perfect'
SRI Tool Integration with the Evidential Tool Bus
SRI Time-Aware Relational Abstractions for Hybrid Systems
SRI, University of Illinois - Urbana-Champaign Safety Verification for Linear Systems
UCLA Security for control systems under sensor and actuator attacks
UCLA Non-invasive Active Sensor Signal Spoofing Attacks on ABS Operation
UCLA Minimax Control For Cyber-Physical Systems under Network Packet Scheduling Attacks
University of Minnesota Compositional Verification of a Medical Device System
University of Minnesota Your what is my how: Why requirements and architectural design should be iterative
University of Pennsylvania Stochastic Game Approach for Replay Attack Detection
University of Pennsylvania Resilient Adaptive Control with Application to Vehicle Cruise Control
University of Pennsylvania, UCLA, Carnegie Mellon University Towards Synthesis of Platform-aware Attack-Resilient Control Systems
Yale University A Case for Behavior-Preserving Actions in Separation Logic
Yale University Modular Verification of Concurrent Thread Management
Yale University Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
Yale University Compositional Verification of a Baby Virtual Memory Manager
Yale University Quantitative Reasoning for Proving Lock-Freedom
SRI The Semantics of Datalog for the Evidential Tool Bus
Yale University A Separation Logic for Enforcing Declarative Information Flow Control Policies
University of Pennsylvania Attack-Resilient Sensor Fusion
University of Pennsylvania Resilient Multidimensional Sensor Fusion using Measurement History
SRI Safety Envelope for Security