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. Kathleen Fisher
Contact: kathleen.fisher@darpa.mil
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: opencatalog@darpa.mil
Last updated: February 09, 2015
| Team | Project | Category | Code | Description | License |
|---|---|---|---|---|---|
| Rockwell Collins (publications) | FM Workbench | Research Integration | http://github.com/smaccm/smaccm | 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 | https://github.com/agacek/jkind | 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 | https://github.com/GaloisInc/smaccmpilot-build.git | 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 | https://github.com/GaloisInc/cbmc-reporter.git | 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 | https://github.com/GaloisInc/smaccmpilot-build.git | 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 | https://github.com/GaloisInc/smaccmpilot-build.git | 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 | http://ssrg.nicta.com.au/software/TS/camkes/download.pml | 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 | http://www.ssrg.nicta.com.au/software/TS/wcet-tools/wcet-tools-0.2.tar.gz | 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 | http://vst.cs.princeton.edu/download/ | 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 | http://plv.csail.mit.edu/bedrock/ | 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 | https://github.com/draperlaboratory/fracture | 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 | https://github.com/tomgr/libcspm.git | 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 | Specware System | Operating Systems | http://www.specware.org/news.html | 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. | Open Source License TBD |
| 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 |
| Team | Title | Link |
|---|---|---|
| Carnegie Mellon University | Motion Interference Detection in Mobile Robots | http://www.cs.cmu.edu/~mmv/papers/12iros-MendozaVelosoSimmons.pdf |
| Carnegie Mellon University | Mobile Robot Fault Detection based on Redundant Information Statistics | http://www.cs.cmu.edu/~mmv/papers/12irosw-MendozaVelosoSimmons.pdf |
| Carnegie Mellon University | A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems | http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/submissions/stage2/99990008.pdf |
| Carnegie Mellon University | On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles | http://symbolaris.com/pub/robix.pdf |
| MIT | Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier | http://adam.chlipala.net/papers/BedrockICFP13/BedrockICFP13.pdf |
| NICTA | seL4: from General Purpose to a Proof of Information Flow Enforcement | http://www.ieee-security.org/TC/SP2013/papers/4977a415.pdf |
| NICTA | Binary Verification of an OS Microkernel | http://www.cl.cam.ac.uk/~mom22/pldi13.pdf |
| NICTA | File Systems Deserve Verification Too! | http://plosworkshop.org/2013/preprint/keller.pdf |
| NICTA | Towards a Verified Component Platform | http://plosworkshop.org/2013/preprint/fernandez.pdf |
| Princeton University | Mostly sound type system improves a foundational program verifier | http://www.cs.princeton.edu/~appel/papers/typecheck.pdf |
| Princeton University | Computational Verification of Network Programs in Coq | http://www.cs.princeton.edu/~jsseven/papers/netcorewp/ |
| Princeton University | Program Logics for Certified Compilers | http://vst.cs.princeton.edu/PLCC-sample.pdf |
| Rockwell Collins, University of Minnesota | Your What Is My How: Iteration and Hierarchy in System Design | http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=6359702 |
| SRI | Automated Reasoning, Fast and Slow? | http://link.springer.com/chapter/10.1007%2F978-3-642-38574-2_10 |
| SRI | Logic and Epistemology in Safety Classes | Not Yet Published |
| SRI | ARSENAL: Automatic Requirements Specification Extraction from Natural Language | http://arxiv.org/pdf/1403.3142.pdf |
| SRI | Reasoning about the Reliability Of Diverse Two-Channel Systems In which One Channel is 'Possibly Perfect' | http://openaccess.city.ac.uk/1069/ |
| SRI | Tool Integration with the Evidential Tool Bus | http://cedeela.fr/~simon/files/etb.pdf |
| SRI | Time-Aware Relational Abstractions for Hybrid Systems | https://es-static.fbk.eu/people/mover/paper/relabs/time-aware.pdf |
| SRI, University of Illinois - Urbana-Champaign | Safety Verification for Linear Systems | http://www.csl.sri.com/~tiwari/papers/emsoft2013_hsalcegar.pdf |
| UCLA | Security for control systems under sensor and actuator attacks | http://www.mit.edu/~hfawzi/security_cdc2012.pdf |
| UCLA | Non-invasive Active Sensor Signal Spoofing Attacks on ABS Operation | http://www.chesworkshop.org/ches2013/presentations/CHES2013_Session1_4.pdf |
| UCLA | Minimax Control For Cyber-Physical Systems under Network Packet Scheduling Attacks | http://people.kth.se/~araujo/publications/hicons14-shoukry.pdf |
| University of Minnesota | Compositional Verification of a Medical Device System | http://www.umsec.umn.edu/publications/compositional-verification-medical-device-system |
| University of Minnesota | Your what is my how: Why requirements and architectural design should be iterative | http://www.umsec.umn.edu/publications/Your-what-my-how-Why-requirements-and |
| University of Pennsylvania | Stochastic Game Approach for Replay Attack Detection | http://rtg.cis.upenn.edu/HACMS/docs/ReplayGame_cdc13.pdf |
| University of Pennsylvania | Resilient Adaptive Control with Application to Vehicle Cruise Control | http://link.springer.com/chapter/10.1007%2F978-3-319-01159-2_11 |
| University of Pennsylvania, UCLA, Carnegie Mellon University | Towards Synthesis of Platform-aware Attack-Resilient Control Systems | http://www.georgejpappas.org/papers/p75-pajic.pdf |
| Yale University | A Case for Behavior-Preserving Actions in Separation Logic | http://flint.cs.yale.edu/flint/publications/bpsltr.pdf |
| Yale University | Modular Verification of Concurrent Thread Management | http://flint.cs.yale.edu/flint/publications/ctm.pdf |
| Yale University | Characterizing Progress Properties of Concurrent Objects via Contextual Refinements | http://flint.cs.yale.edu/flint/publications/eqconcur.pdf |
| Yale University | Compositional Verification of a Baby Virtual Memory Manager | http://flint.cs.yale.edu/flint/publications/babyvmm_tr.pdf |
| Yale University | Quantitative Reasoning for Proving Lock-Freedom | http://cs-www.cs.yale.edu/homes/hoffmann/papers/lockfree2012full.pdf |
| SRI | The Semantics of Datalog for the Evidential Tool Bus | http://stijnheymans.net/pubs/sas2014.pdf |
| Yale University | A Separation Logic for Enforcing Declarative Information Flow Control Policies | http://flint.cs.yale.edu/certikos/slides/IFC.pdf |
| University of Pennsylvania | Attack-Resilient Sensor Fusion | http://repository.upenn.edu/cgi/viewcontent.cgi?article=1815&context=cis_papers |
| University of Pennsylvania | Resilient Multidimensional Sensor Fusion using Measurement History | http://repository.upenn.edu/cgi/viewcontent.cgi?article=1816&context=cis_papers |
| SRI | Safety Envelope for Security | http://www.csl.sri.com/users/tiwari/papers/hicons14.pdf |