Main navigation | Main content
The goal of DARPA's High-Assurance Cyber Military Systems (HACMS) program 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. HACMS adopts a clean-slate, formal methods-based approach to the development of network-enabled military vehicles to produce systems that provide the highest levels of dependability and are resistant to emerging cyber threats. Rockwell Collins is leading a team on the HACMS program, including Boeing, Data 61, Galois, and University of Minnesota, focusing on cyber threats to unmanned air vehicles. In this presentation, we will provide an overview of our approach and describe results to date on the tools developed to support modeling and verification of system-level security properties.
Our approach is based on compositional reasoning driven by the design of the vehicle system architecture. We are developing verification tools for combining formal evidence from multiple sources, including control components and operating system software synthesized from formal specifications. We are prototyping these technologies on an open research platform (quadcopter) and transferring them to a military platform (Boeing's Unmanned Little Bird helicopter) to demonstrate their practicality and effectiveness.
Directions can be found on the map of the Electrical Engineering/Computer Science Building.
Check out the detailed map by clicking the “close up” button.
Keller (EE/CS) 3-111 (Look for signs)
5:30 - 8:00 p.m. at The University of Minnesota
5:30 start for networking, 6:15 start of meeting
Please note the free parking process at the U has changed.
Free parking tickets will be handed out in the meeting.
Andrew earned his PhD in Computer Science from the University of Minnesota in 2009 and continued his studies as a post-doc INRIA Saclay as part of Parsifal group. In 2010, Andrew joined Rockwell Collins. He is currently working as part of the air vehicle team in DARPA's High Assurance Cyber Military Systems project (HACMS), focusing high-level structural and behavioral properties for unmanned air vehicles.
Andrew has a strong interest in developing tools for the application of formal methods. As part of his PhD thesis, Andrew created the Abella theorem prover, an interactive theorem prover based on lambda-tree syntax. At Rockwell Collins, Andrew developed JKind, an infinite-state model checker for safety properties. JKind is used for both various internal and external projects at Rockwell Collins. Most recently, Andrew developed the Resolute language and tool for architecturally-structured assurance cases.
His interests include theorem proving, model checking, language translation, and software design.