Finding the right security solution is often a difficult task, with many complex trade-offs to consider. Building a secure system is even more challenging as history has shown. Designing and building systems that are “tolerant of adversarial cyber actions,” as expressed by our interviewee below, seems a herculean task. So I was quite interested to learn while attending the MILCOM 2018 conference in October that such a task is being undertaken by DARPA with the goal of protecting embedded systems. Embedded systems provide the foundational capabilities for many military systems as well as our critical infrastructure and emerging IoT technologies. They are also highly sought after cyber targets by cyber adversaries. Creating resilient cyber systems is a relatively new area of research but one that has its roots in the high assurance and safety critical systems research efforts conducted by DoD, NASA, and the Intelligence Community starting in the 1970’s, through many stops and starts to today.  So read the Active Cyber interview below with Dr. Ray Richards – Program Manager at DARPA for some highlights of the latest research in this space and how recent breakthroughs in engineering methods, tools, and operating systems offer new possibilities in constructing and delivering the highly secure and attack-resistant technologies we need to progress in the fight against cyber threats. 

Spotlight on Dr. Ray Richards

» Title: Dr. Raymond Richards, Program Manager, DARPA Information Innovation Office (I2O)
» Website:
» LinkedIn:

Read his bio below.

December 5, 2018

Chris Daly, Active Cyber™: One of the projects in your portfolio is known as Cyber Assured Systems Engineering (CASE). What are the objectives of CASE and what real world challenges are you trying to address with your research?

Dr. Raymond Richards, Program Manager, DARPA Information Innovation Office (I2O): The goal of the Cyber Assured Systems Engineering (CASE) program is to create technology for the design of cyber resilient military systems. The current state of practice for systems requiring cyber resiliency is to apply best practices during software development, and then perform penetration testing once the system development is complete. This approach does not produce systems that continue to operate after a cyber-incursion, and generates costly rework cycles when penetration testing demonstrates vulnerabilities. CASE seeks to provide the ability to design systems that continue to operate in the face of cyber-attacks.

Active Cyber™: How or why is systems engineering for securing embedded systems different from securing basic IT systems?

Dr. Richards: Embedded computing systems are ubiquitous in critical infrastructure, vehicles, smart devices, and military systems. Conventional wisdom once held that cyber attacks against embedded systems were not a concern since they seldom had traditional networking connections on which an attack could occur. However, attackers have learned to bridge air gaps that surround the most sensitive embedded systems, and network connectivity is now being extended to even the most remote of embedded systems. In short, embedded systems are now subject to cyber attacks, either as the end goal of the cyber assailant or as a means to a greater end, and there is a critical need to protect and defend embedded systems in a cyber context. The mechanisms currently employed to secure embedded systems include development of software using cyber best practices, adapting mechanisms from information technology (IT) systems, and penetration testing followed by patching; however, these methods have proven to be generally ineffective.

Systems engineers are responsible for producing designs with a required set of functional and non-functional properties. Non-functional properties include properties such as safety, performance, durability, survivability, availability, manufacturability, maintainability, etc. The system designer is responsible for managing conflicts and making trade-offs between the desired non-functional properties. Critical systems are built by requirements-based engineering and it is an accepted axiom of systems engineering that requirements are positive, testable statements about the system. Statements on the systems’ functional behaviors and non-functional properties often captured as ‘shall’ statements. This style of engineering has proven to be ineffective in engineering cyber resilient systems because cyber requirements are often statements on what the system should not do, i.e., “shall not …” statements.

Active Cyber™: What types of research breakthroughs are needed to ensure your objectives are met? Have any of these breakthroughs been reached to date?

Dr. Richards: Achieving this goal requires research breakthroughs in:
• the elicitation of cyber resiliency requirements before the system is built;
• the design and verification of systems when requirements are not testable;
• tools to automatically adapt software to new non-functional requirements; and
• techniques to scale and provide meaningful feedback from analysis tools that reside low in the development tool chain.

At the time of this writing, the program performers have delivered initial prototypes of their technologies, five months after the program start. Future tool integration will depend on these prototypes advancing throughout the balance of this program.

Active Cyber™: What types of tools and techniques are you developing as part of your research efforts and why? How have they performed to date and what changes are you currently working on?

Dr. Richards: CASE is producing a set of tools to derive resiliency requirements from functional system designs, adapt and verify the functional designs to be cyber resilient, while proving for the reuse of legacy software. CASE has partitioned this problem into four sub-problems. First, derive cyber resiliency requirements early in the system design. Second, support the design and verification of the resiliency requirements into the system with the use of run-time assurance and recovery to provide resiliency. Third, adapt legacy software to provide resiliency-supporting requirements, with either design-time or run-time assurance. Fourth, enhance state-of-the-art analysis tools to provide rich feedback to the designer to facilitate design decisions. Recognizing that the technologies developed in the CASE program will need to integrate into complex engineering workflows that employ hundreds of tools, development engineers will demonstrate the integration and use of these technologies.

Active Cyber™: Cyber resiliency is also a keystone of the draft NIST SP 800-160 v2 [Systems Security Engineering: Cyber Resiliency Considerations for the Engineering of Trustworthy Secure Systems]. How does your research align with the guidance contained in that document?

Dr. Richards: CASE is a systems design program. It deals with cyber-resiliency as a system property, much the same way as safety-critical systems, such as airplanes, deals with safety as a system property. That is to say, we wish to design systems that are tolerant of adversarial cyber actions, the essence of resiliency. We are assuming that software can and will be compromised. We would prefer to prove cyber properties conclusively at design time. However, recognizing that this will not be always achievable, run-time assurance of cyber properties, and the restoration of those properties if they are violated at run-time provides resiliency. Of note, developing technologies to support software implementations is out of scope for CASE.

Active Cyber™: A separate but related project in your portfolio is High-Assurance Cyber Military Systems (HACMS). What is meant by “high assurance” and what are the challenges to achieving high assurance? Does this research involve a resurgence of the Trusted Computer System Evaluation Criteria [Orange Book] A level requirements? How are you looking to achieve high assurance?

Dr. Richards: The research thrust of HACMS completed in 2017. There are ongoing efforts to apply the HACMS technologies to cyber retrofit candidate systems.

HACMS demonstrated the use of mathematically rigorous software development and verification techniques to provably remove large classes of cyber vulnerabilities. At the beginning of the program, baseline platforms were provided to a penetration testing team. The research teams were fed the uncovered vulnerabilities. The researchers were able to define a small set of cyber properties that mitigated this class of vulnerabilities. These properties were expressed as non-testable ‘shall not’ requirements. The best option for verification of untestable properties is through analysis. The most rigorous forms of analysis are those that are mathematically sound. These platforms were re-engineered with software that was mathematically verified. The modified platforms were again given to the penetration testers, who were unable to compromise them. We do not claim that these systems are free from vulnerabilities; we have demonstrated the removal of a significant class of vulnerabilities. A video of one of the modified platforms can be found at

Active Cyber™: Why is composability such a difficult challenge when it comes to high assurance systems? What types of conditions or properties must be present and verified for a module to be composable?

Dr. Richards: Composability implies the ability to take separately developed components to integrate them into a system without unwanted emergent properties. To achieve this one needs to have syntactic and semantic alignment of the interfaces and being able to understand all of the interactions and interdependencies among the components. Standardized interfaces address the syntactic alignment, but sometimes fall short on semantic alignment. The interactions and interdependencies are more insidious. Software developers make all sorts of implicit assumptions. These can and do include the programming model of the source language they are using and the behavior of hardware. Capturing interdependencies that are invisible to the developer is very difficult.

Active Cyber™: What types of research advances are you building on and looking to create as part of the HACMS efforts? What tools are you looking to develop as part of the HACMS effort and why?

Dr. Richards: All of the developed HACMS technologies are non-proprietary and available as open source.

HACMS focused on three software layers, each layer matched with a different style for formal (i.e. mathematical) verification. These layers are the 1) low-level software, 2) application software, and 3) software architectures. The style of formal (i.e. mathematical) analysis for each layer was chosen to prove the necessary properties and maximize the automation of the analysis.

Low-level software means operating systems kernels. Two kernels with rigorous verification were develop. CertiKOS is available from Yale University, and seL4 is available at At this level, the verification was extremely detailed and laborious, and the resulting software kernels were delivered, not the tools to develop and verify them. Frankly, the special skills necessary to perform such work is rare. Taking seL4 as an example, there is a mathematical expression describing its behavior; proofs that this behavior provides Confidentiality, Integrity, and Availability; and proofs that the implementation faithful executes its specification. Several processor architectures are supported by seL4. For most architectures, the implementation proofs prove the C code implementation. On the ARM processor, the proofs go down to the binary. The bits executing on an ARM processor are proven to be correct and provide necessary security properties.

HACMS produced a variety of tools to implement secure application software, all of which is accessible from the DARPA Open Catalog on the DARPA webpage ( These tools include advanced C verification tools (VST from Princeton University), Domain Specific Language tools that do not allow you to implement certain vulnerabilities (Ivory form Galois), and the generation of implementations from specifications that have been analyzed for correctness (SpiralGen from CMU) as examples.

At the architecture level, we developed tools to analyze architectural models (expressed in AADL) to show that the required non-testable properties are met. The architectural models are annotated with contracts that represent the proven properties of the verified components. The annotated models are then analyzed to verify these properties. These tools are available in the Open Source AADL Tool Environment (OSATE) maintained by the Software Engineering Institute (SEI).

Several of the HACMS performers work with military programs to attempt to replicate the success of HACMS on an ever-growing list of platforms. The Society of Automotive Engineers (SAE) is preparing training sessions around the tools developed in HACMS (and related formal verification tools). The initial run of training session is slated to occur in the spring of 2019.

The goal for transitioning HACMS is to demonstrate enough successful developments within the DoD that the DoD begins to write requirements for formally verified software.

Active Cyber™: How are CASE and HACMS research efforts related? Do they share any common goals, research targets, hard problems, or research approaches?

Dr. Richards: CASE is focused on system design and stops at software implementation. In the traditional systems engineering ‘V’ model, CASE includes the activities on the left arm of the ‘V’. HACMS looked at software implementation, staying completely on the bottom of the ‘V’. One could imagine a design workflow where CASE tools perform system design, developing the requirements for the software components. HACMS tools translate those requirements to implementations.

Thank you Dr. Richards for sharing some background on your extensive research in developing highly secure and resilient cyber systems for our military and critical infrastructure. I sincerely hope that practitioners in constructing embedded systems, such as the automotive industry as you highlight in the interview, take advantage of the tools, low level kernels, and techniques your research efforts have developed to make our every day systems, as well as our national defense systems, more secure and resistant to cyber attack effects. I look forward to the day when most of our cyber environments are trustworthy, or minimally “cyber-safe”  to use.

And thanks for checking out! Please give us your feedback because we’d love to know some topics you’d like to hear about in the area of active cyber defenses, PQ cryptography, risk assessment and modeling, autonomous security, securing the Internet of Things, or other security topics. Also, email if you’re interested in interviewing or advertising with us at Active Cyber™.

About Dr. Raymond Richards

Dr. Raymond “Ray” Richards joined DARPA in January 2016. His research interests focus on high assurance software and systems. Dr. Richards joined DARPA from Rockwell Collins Advanced Technology Center (ATC) where he led a research group focused on automated analysis, cyber, and information assurance. In this role he helped foster the industrial use of formal methods verification to support security accreditations.

Dr. Richards holds Master of Business Administration, Doctor of Philosophy and Master of Science degrees in electrical and computer engineering, as well as a Bachelor of Science degree in electrical engineering, all from the University of Iowa. He has nine publications in the area of formal methods/software security analysis and one patent.