High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)

The Nuclear Regulatory Commission (NRC) ensures the safety of commercial nuclear power plants and other nuclear projects. These are some of the most important safety-critical systems in existence today. It would be disastrous if any adversary – whether they’re anonymous individuals or nation-states – gained control of a control system for a nuclear power plant. So it is vital that the technology powering the software and hardware for these systems is safe, correct, and secure.

Galois’s High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) is designed for this purpose. 

HARDENS uses our Models-Based Systems Engineering (MBSE) methodology – known as Rigorous Digital Engineering (RDE) – to create the world’s most advanced, high-assurance protection system demonstrator.  HARDENS demonstrates MBSE-based capabilities for safety-critical nationally critical infrastructure like nuclear power plant (NPP) control and protection systems. 

Why MBSE and RDE? 

Model-Based Systems Engineering is currently used in aerospace, defense, and automotive applications. High-level models of systems are written in standardized languages like SysML or UML. The benefits of MBSE are comparable to real-world (e.g. non-digital) engineering practices, because MBSE provides a holistic design-to-development-lifecycle. Unfortunately, while models and code are deeply connected in our modern world, they are disconnected in most MBSE systems. Few code-generation frameworks provide assurance about generated code – most do not even create test cases for implementations.

Galois uses RDE to authentically and rigorously describe different levels of abstraction. RDE holistically addresses all levels of a system’s lifecycle, including process, methodology, design, development, assurance, and maintenance. 

As a Galois RDE project, HARDENS involves the development of high-assurance firmware (software that runs directly on the hardware) and an assurance that the hardware and firmware fit perfectly together. HARDENS takes RDE one step further as it focuses on a fault-tolerant system – the project is developing a hardware demonstrator, known as the HARDENS Reactor Trip System (RTS).

Demonstrating Assurance for Nuclear Systems

The HARDENS RTS includes formally assured hardware – a three-core RISC-V System-on-Chip, automatically generated and hand-written formally verified hardware components. It also includes automatically synthesized and hand-written formally verified software.

The HARDENS demonstrator’s most informal specification starts with precise English from the NRC RFP and relevant IEEE standards. These specifications refine to formally verified properties of the hardware and software, and this refinement is completely traceable. 

The HARDENS RTS also includes several digital twins, demonstrates co-design and co-verification using formal methods, and it uses refinement for traceability and digital threads. 

Product Line of Assurance

HARDENS, like our fellow RDE project HIPERSPACE, is designed to be a product line. This means that it is an integrated set of hardware, firmware, and software systems engineering artifacts – including documentation, specifications, and source code – that can derive multiple different products from a build/synthesis/fabrication process. 

The HARDENS product line family can be used to efficiently create many product variants (such as cryptographic algorithm choices), while supporting many different build processes (like clock speed) and Q/A (such a rigorous runtime verification versus formal static verification) features. 

The Outcome

HARDENS’s final description and assurance case (e.g., the evidence of its correctness) is digital and physical. The entire system is exported as a single rich, hyperlinked, and auditable document.

Galois presented the final slide deck and the demonstrator to the NRC in an all-day review, incorporated their input, and delivered the final technical snapshot of all artifacts.  

You can also read about HARDENS on its github page.