SMACCM

New generations of military vehicles, including unmanned air vehicles (UAVs), are almost universally being equipped with network interfaces. In addition to the baseline control and monitoring capabilities, network connectivity can provide advanced features such as the ability to adapt to new missions through field upgrades and remote access for maintenance. These network connections typically rely on standard protocols for compatibility with other networked systems and reduction of cost through the use of COTS equipment.

However, network-enabled vehicles bring with them new risks. As UAV systems continue this rapid evolution toward network access, there is great danger that insufficient attention is being paid to security concerns. Unless a new approach is taken, they will likely end up with same vulnerabilities that plague personal computers and web servers, and that we are now seeing in industrial SCADA systems and even automobiles. Recently documented security vulnerabilities in cyber-physical systems include the “car-hacking” work of University of Washington and UCSD, the Stuxnet virus, and the Landsat 7 and Terra AM1 satellite incidents.

These examples demonstrate that security vulnerabilities can be exploited to cause safety hazards such as the loss of the vehicle or compromise of its mission, in addition to the loss of classified data. A new approach based on comprehensive use of formal methods throughout the development process is needed to ensure that such vulnerabilities are eliminated from critical military assets.

With our unmatched expertise in application of formal methods to commercial and military aerospace systems, Rockwell Collins is uniquely positioned to provide the needed clean-slate approach to building high-assurance systems. Our proposed Secure Mathematically-Assured Composition of Control Models (SMACCM) project will:

Develop a complete, formally proven architecture for UAVs (and other embedded systems) that provides robustness against cyber attack

Develop compositional verification tools for combining formal evidence from multiple sources, components, and subsystems

Prototype these technologies on an open research platform and transfer them to a military platform to demonstrate their practicality and effectiveness

This is a challenging project with far-reaching goals. Our integrated team brings together key technologies and leading researchers with the experience needed to create a revolutionary approach to the development of high-assurance systems. We are prepared to work together to accomplish the goals of HACMS Technology Areas 1 through 4, as follows:

Boeing (TA1) will develop challenge problems derived from the Unmanned Little Bird military UAV to define research needs and integrate research results for demonstration on the military platform.

NICTA (TA2) will provide formal verification of operating system components, including seL4, the world’s only microkernel formally verified to the code-level.

Galois (TA3) will synthesize high-assurance control components through the development of new Embedded Domain Specific Languages and will develop an open source research platform based on the ArduCopter design.

Rockwell Collins and University of Minnesota (TA4) will develop an integrated tool environment for composition of formal verification evidence and design of the high-assurance vehicle architecture.

Tools

Click here to download the SMACCM Tools.