AdaCore, a leader in high-assurance, safe, and secure software toolchains, is set to stand out at CYBERUK by showcasing its unique approach to Secure Avionics by Design (SAbD).
AdaCore's SAbD technology has emerged from phase 1 of the collaborative and ongoing Edge Avionics programme. Edge Avionics aims to research state-of-the-art systems security by building a real-world demonstrator avionics defense platform (hardware and software) that showcases cyber and battlefield resilience. The Edge Avionics programme is funded by the Rapid Capabilities Office (RCO) of the UK Royal Air Force (UK RAF). Edge Avionics is a consortium led on behalf of the RCO by the Defence Science and Technology Laboratory (Dstl, an executive agency of the UK Ministry of Defence (MOD)) and delivered by GE Aerospace (the prime), Wind River, and AdaCore.
The primary mission of Edge Avionics is to evaluate security claims made by the Digital Security by Design (DSbD) initiative within a large-scale defense application. DSbD is a programme supported by the UK government to transform digital technology and create a more resilient and secure foundation for a safer future. DSbD involves a significant collaboration between academia, industry, and government with an essential emphasis on evaluating the security benefits of Capability Hardware Enhanced RISC Instructions (CHERI). In partnership with The University of Cambridge and Arm, the initial CHERI initiative has also received large amounts of funding from the US government through SRI International via the Defense Advanced Research Projects Agency (DARPA, the central research and development organization of the Department of Defense (DOD)). CHERI promises to revolutionize the design of CPU architectures by providing dedicated registers and instructions for enforcing the safe usage of memory allocation, reads, and writes. CHERI aims to provide a framework for building and executing software applications that trap non-safe memory instruction calls directly at the hardware level, thus eliminating many memory-related vulnerabilities by making them non-exploitable.
The Dstl technical lead for Edge Avionics emphasises the context and importance of secure by design:
“The UK government support for the world leading CHERI technology through the Innovate UK DSbD initiative is part of a strategy to enable security and resilience using a ‘secure by design’ approach. A CHERI compute solution provides one of the foundation elements for a secure by design system and is being explored through the Edge Avionics technical demonstrator. Secure by design is now a requirement for Ministry of Defence systems."
AdaCore's commercially available SAbD solution provides a complete Ada toolchain to build highly secure bare-metal applications executing on Arm Morello, a CHERI ISA CPU, and an evaluation board. AdaCore's GCC and LLVM bare-metal Ada runtimes have been enhanced to support CHERI pure-capability memory allocators as well as other novel features that bring new security by design options to avionics security development, as explained by Paul Butcher, UK Programme Manager, and AdaCore's Edge Avionics Project Manager:
"CYBERUK has been an excellent venue for AdaCore to showcase our range of security solutions designed for the highest-assurance security systems, and we're excited to present our latest state-of-the-art contribution at CYBERUK 2024. We see microprocessor CHERI Instruction Set Architectures (ISAs) that support capability registers, capability instructions, and pure-capability mode as the ultimate CPU security toolkit upon which the highest assurance software systems can be developed and deployed. Our solution couples the memory-safe programming language Ada with a security-enhanced GNAT Pro Ada runtime designed to fully utilize the pure-capability memory-safety properties the Arm Morello CHERI compatible CPU provides.”
We asked John Goodacre (Director of the Digital Security by Design Challenge Fund) why CYBERUK is important to DSbD and what it means to be co-exhibiting with partners like AdaCore:
"The Digital Security by Design (DSbD) initiative is transitioning into an exciting phase as concrete examples of industry grade CHERI enabled hardware and software emerge. CYBERUK is a perfect venue for DSbD to showcase various efforts that enable a more trustworthy and resilient digital environment. This year, we are attending with multiple partners to demonstrate the results of their efforts and commercial opportunities in delivering memory safety and low cost, enhanced system protections. Through the Edge Avionics programme, AdaCore is demonstrating the benefits of DSbD technology within a defence environment, and DSbD thoroughly supports their work and looks forward to welcoming them and their demonstrator system on the DSbD stand, C2, at CYBERUK 2024."