CHERI on Top: AdaCore’s Hardware ‘Fix’ for Legacy C/C++ Code
As federal agencies and contractors face a potential 2026 deadline to move away from C and C++ code due to memory safety concerns, many organizations are grappling with a significant challenge: what to do with millions of lines of existing legacy code.
For organizations with massive codebases that have already been certified for critical applications, complete rewrites aren’t feasible — yet security vulnerabilities stemming from memory safety issues remain a pressing concern.
Tony Aiello, head of product and innovation at AdaCore, and Jose Ruiz, the company’s product manager for embedded targets, spoke with The New Stack about practical approaches to addressing memory safety in legacy software systems. AdaCore, a provider of high-integrity systems development tools, offers an interesting perspective on this industry-wide challenge.
The Legacy Software Dilemma
“Legacy software is hard,” Aiello told The New Stack frankly. “It’s been a hard problem for a long time.”
The difficulty is apparent in the Defense Advanced Research Projects Agency’s (DARPA) ongoing efforts to tackle software correctness and memory safety. While many proposed solutions work well for new development, they often falter when applied to existing systems. DARPA’s recent “Tractor” initiative, which aims to develop automated tools to rewrite C code in Rust, underscores just how challenging the legacy code problem remains.
CHERI: A Runtime Solution for Legacy Code
For organizations unable to rewrite their legacy C/C++ codebases, AdaCore is working with an emerging hardware-based solution called CHERI (Capability Hardware Enhanced RISC Instructions).
“We are working on developing a tool chain on top of a new kind of hardware which is called CHERI, which basically allows you to detect and add information to that hardware so that it can automatically detect some potential or some actual memory safety problems,” Ruiz explained.
What makes CHERI particularly valuable for legacy systems is that it doesn’t require rewriting code — only recompiling it. The technology provides specialized hardware instructions that check memory safety at runtime, halting the program if violations occur, he said.
Although CHERI hardware is still “quasi-experimental” according to Ruiz, AdaCore provides an emulator that allows developers to recompile their legacy software and detect memory vulnerabilities without requiring actual CHERI hardware. This approach is particularly useful in testing scenarios, such as fuzzing campaigns to detect memory safety issues.
“CHERI will keep you safe effectively by halting the program if it does the wrong thing,” Aiello said. “It’s protecting you in the sense that it provides confidentiality and integrity at the expense of availability, because it’s going to kill off the software if the software does something wrong.”
Strategic Rewrites With Spark and Rust
For critical components where program termination isn’t an acceptable outcome, AdaCore recommends targeted rewrites of the most critical code sections using memory-safe languages like Spark (a dialect of the Ada programming language) or Rust.
Aiello pointed to NVIDIA as an example: “NVIDIA was initially very concerned about some security properties of their firmware and chose to rewrite portions of the firmware that had previously been written in C in Spark, and prove correctness of safety properties while they did this rewrite.”
To support this approach, AdaCore provides toolchains for C/C++, Rust, and Spark that work well together, enabling organizations to gradually improve security in their most critical components while maintaining their existing codebase, Aiello said.
Spark: Formal Verification for Critical Systems
When discussing alternatives to C/C++, Aiello highlighted Spark, a dialect of Ada that enables formal verification – a powerful capability for security-critical applications.
“Spark permits you to do functional verification using formal proof,” Aiello explained. “For a given function in your software, you state preconditions, constraints on the inputs to the function, and then you state the expected output of the function. Spark will prove automatically that the implementation makes the post-condition true when the precondition holds.”
This capability is particularly valuable for security because Spark automatically proves that code doesn’t have runtime errors — including memory safety issues. While Ada provides runtime checking of range values and memory access, Spark can statically prove at design time that none of these checks will fail, allowing developers to disable them for performance without sacrificing safety.
The Rust Appeal: Why Organizations Are Looking Beyond C/C++
While AdaCore has deep roots in Ada and Spark, they’re also embracing Rust as part of their solution portfolio. Aiello identified three key factors driving Rust’s popularity:
- Memory safety: Rust’s ownership model prevents memory safety issues at compile time
- Growing talent pool: Unlike Ada, companies can find developers who already know Rust
- Rich ecosystem: Rust’s extensive library of third-party “crates” accelerates development
“The excitement behind Rust means that there are a lot of people, a growing number of people, who know Rust and who really want to use it in their professional career,” noted Aiello. “There’s a lot of grassroots that I’ve been hearing about at basically every company you can think of where engineers are agitating for the use of Rust.”
The Future: AI + Formal Methods
Looking ahead, Aiello said he sees potential in combining generative AI with formal methods like Spark to accelerate secure software development. While acknowledging that AI-generated code can contain errors, he suggests that formal verification could provide a powerful safety net.
“You could provide requirements for your software, maybe write some preconditions and post-conditions, some contracts that state formally what you want your software to do and then push a button and have a generative system implement it for you, and then run Spark and prove that the implementation matches the contracts,” Aiello said.
This approach would maintain human creativity for architecture and design while delegating implementation details to AI systems, with formal verification ensuring correctness, he noted.
A Multitiered Response
As organizations face growing pressure to address memory safety, AdaCore’s approach offers a realistic pathway forward. Rather than demanding complete rewrites of legacy systems, they propose a combination of strategies:
- Using CHERI hardware/emulation to detect memory safety issues in existing code.
- Strategically rewriting critical components in memory-safe languages like Spark or Rust.
- Employing formal verification to mathematically prove the absence of memory safety issues.
This pragmatic, multilayered approach acknowledges both the business reality of legacy code and the critical importance of improving security — offering a blueprint for organizations navigating the complex transition away from C/C++.
