polymorph
As part of DARPA's Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) Program, Galois developed three tools – Taphos, Walrus, and Oxide – to help modernize legacy codebases by incorporating Model-Based Engineering practices, enabling safer updates with machine-checkable guarantees and streamlined certification.
How it works
Our process begins with a legacy codebase that needs to be updated. This often shows up as a tangled mess of C code, which is difficult to understand, may have security vulnerabilities, and is challenging to modify.
taphos
To accelerate human understanding of the legacy code base, we use Taphos, which is designed to recognize patterns in a domain, analyzing the code and creating a visual model of the functions, components, and relationships with guidance from a domain expert.
Once the target program has been analyzed, the Taphos-generated model can be used to identify and extract components and interfaces that need to be upgraded or modified. This process can be performed repeatedly (and automatically) on current and future versions of the system to capture the evolution of the target program.
Walrus
Next, we use the Walrus co-compiler to lift the pieces of C code identified by Taphos into more high level and compositional SCADE and Lustre models.
Now that the code has been translated into model form, it can be patched, modified, or maintained at the model level.
OXIDE OR SCADE
At this point, users have two possible paths forward: Either they can use SCADE for immediate compilation, generating DO-178C certified, memory safe C code; or they can use our Oxide tool as a more robust, continuous assurance option.
Both options generate memory-safe, compatible C-code that can be reincorporated back into the legacy codebase with improvements and modifications intact.
The key difference is that Oxide verifies that every compilation step preserves memory safety. It does this using type-checking techniques heavily inspired by Rust. This allows code to be re-checked for security properties after it is compiled, and after it is linked into a complete system.
This also gives Oxide an edge over Rust-based compilation. Whereas Rust prevents many memory-related errors in the initial writing of code, once compiled, Rust code can still be compromised if linked to unsafe components.
By contrast, Oxide’s continuous assurance approach ensures safety not only when the code is generated, but during compilation and after it has been reintegrated into the legacy system.
Value Add
In short: Galois has developed a cohesive tool chain that allows users to lift C code from a legacy code base, automatically generate a model for easy analysis, modify or upgrade discrete blocks of code, and easily slot the modified code back into the legacy system for higher security or improved performance.
Equipped with these tools, users can treat legacy codebases as modular systems – upgrading them incrementally over time, all while benefiting from greater understanding of their codebases and the peace of mind that comes from continuous, provable correctness.
This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA). The views, opinions, and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.
Distribution Statement A: Approved for Public Release, Distribution Unlimited
