HACMS: High-Assurance Cyber Military Systems

The High-Assurance Cyber Military Systems (HACMS) program proved that it's possible to deliver high-assurance software capable of withstanding cyber threats and operate effectively in military applications.

Traditionally, air gaps and obscurity provided security for embedded systems. A lack of network connectivity made these embedded systems an unattractive target for cyber threat actors. However, the proliferation of commoditized software in embedded systems coupled with advances in re-engineering and vulnerability exploitation tools have made embedded systems an attractive target for cyber-attacks.

HACMS employed formal methods to construct high-assurance software – i.e., functionally correct software that satisfies appropriate safety and security properties – and generate machine-checkable proofs that the code was safe and secure. These high-assurance software tools are publicly available today and have transitioned to parts of the U.S. government, and defense and commercial industries.

The test

DARPA tested the software developed under HACMS on real military hardware and systems to verify its performance and compatibility in operational environments. First using a small quadcopter as a testbed, then graduating to a much larger helicopter, Boeing’s Unmanned Little Bird, DARPA demonstrated the benefits of software written with formal methods. HACMS conducted simulated cyber-attacks (often called red team exercises) to test the resilience of its software against real-world threats. These exercises identified weaknesses and vulnerabilities that could be addressed before deployment. Throughout the development process, HACMS continuously monitored and evaluated the software to ensure that it met the desired security and reliability standards. This iterative approach enabled ongoing improvements and corrections.

When the project started, the Red Team was able to remotely take over the systems. At the end of the HACMS program, they repeated that experiment while Little Bird was in flight with two test pilots on board. DARPA’s HACMS team had become so confident in the formally verified software that they were willing to risk the lives of those two pilots as the Red Team attempted to hack the helicopter – the Red Team failed, and the pilots remarked they couldn’t even tell the difference in flying the high assurance version. To this day, the system has yet to be successfully hacked. The following provides the abbreviated story of how.

Back to top

Proving what's possible

The HACMS program achieved these results by first charging a "Blue Team" of formal methods researchers to improve the security of a hobbyist quadcopter. The team rewrote ~80,000 out of the 100,000 lines of code with formal methods and divided the code on the system's mission-control computer into partitions. This approach was required because the system contained off-the-shelf, monolithic software. This attribute, which is shared by many legacy code bases, meant that if an attacker broke into one piece of it, they had unfettered access to the entire system. Unlike most computer code, which is written informally and evaluated based mainly on whether it works, formal methods-based software can be analyzed like a mathematical proof: Each statement follows logically from the preceding one. An entire program can be assessed with the same certainty that mathematicians prove theorems.

With the formal method upgrades in place, Blue handed the quadcopter over to Red to see if they could hack into the system. The tools and methods worked as intended and the hackers were unsuccessful. This methodology has stood the test of time and subsequent hacking events, including a 'hack the drone' challenge at DEF CON, have proved unsuccessful.

Following the success with the quadcopter, the DARPA team applied the formal methods approach to the Boeing Little Bird. This platform provided a proxy for the version used for U.S. special operations missions. The Boeing engineers were confident the system was immune to cyber-attacks. They were wrong. Without formal methods integrated into the system, a Red Team of ethical hackers quickly gained access to the helicopter's computer system. From there, they easily gained access to Little Bird's onboard flight-control computer. The Red Team owned the entire system.

To secure the helicopter, the Blue Team applied the same approach developed on the quadcopter into the Little Bird. Following this system modification, the Red Team was granted six weeks to hack the system. The formal method-generated code foiled all Red Team attempts to crack the Little Bird's defenses.

After a first round of failed attempts, the Red Team was granted access to a partition on the helicopter that provided a non-critical function (i.e. the helicopter's camera system). Because of the formal methods design approach, the hackers were mathematically guaranteed to remain stuck in that partition…and that's exactly what happened. Even with this initial foothold, the Red Team could not expand access to additional Little Bird systems, nor disrupt operations beyond their initial partition. Once again, the formal methods approach demonstrated that the high assurance code was acting as intended.

The Blue Team repeated this test while the helicopter was in flight with two test pilots at the controls. Again, the Red Team was not able to break out of their partition. In addition to reporting no operational impacts due to the Red Team's access, the test pilots noted no performance consequences to the software functionality. The cyber-hardened Little Bird operated the same as the legacy system. This test confirmed that it is possible to significantly enhance security using formal methods without compromising system performance.

Since the Little Bird test, DARPA successfully applied the HACMS tools to other military systems, including satellites and self-driving convoy trucks. Each successful project has validated the advantages of applying a formal methods approach to software security.

Back to top

The role of secure, verified parsers in HACMS

The HACMS program highlighted the critical role parsers play in ensuring the security and reliability of software systems. (Parsers are software routines that convert external input to in-memory representations; buggy parsers are responsible for a significant fraction of successful hacker attacks). 

Key aspects of the role parsers play include the following:

• Input validation and sanitization: Parsers are essential for validating and sanitizing input data received by software systems. They ingest incoming data, which could come from various sources such as user inputs, sensors, or communication channels. Proper parsing ensures that the data is correctly formatted and free from malicious content or potential exploits like buffer overflows or injection attacks.
• Defense against cyber attacks: One of the primary concerns addressed by parsers in HACMS was their role in defending against cyber-attacks. By carefully ingesting and validating input data, parsers help prevent common attack vectors such as SQL injection, cross-site scripting (XSS), and command injection. High assurance parsers are the first-line of defense for maintaining the integrity and security of military systems that may be targeted by adversaries seeking to exploit vulnerabilities.
• Interoperability and compatibility: Parsers also facilitate interoperability and compatibility by correctly interpreting data formats and protocols used in military systems. They ensure that data exchanged between different components or systems is properly understood and processed, thereby supporting seamless communication and integration within complex military environments.
• Formal verification and assurance: In the context of HACMS, parsers were subjected to formal verification techniques, which involved using mathematical methods to rigorously analyze and prove the correctness of parser implementations. Formal verification ensured that parsers behaved as intended under all possible inputs, reducing the risk of errors or vulnerabilities.
• Integration into secure software architecture: Parsers were integrated into the broader secure software architecture developed under HACMS. This architecture emphasized principles such as least privilege, defense-in-depth, and compartmentalization to enhance overall system security. Parsers played a role in enforcing these principles by securely handling input data and contributing to the overall resilience of the software systems.

Back to top