Conjuring Correct-by-Construction Code That is Safely Composable System-Wide

The title of our blog post may sound like a directive from a Dungeon Master, but it’s firmly rooted in Galois’s forward-thinking computer science.  C/C++ code is the foundation of our most critical systems – even “new” systems nearly always incorporate legacy code. But this type of component reuse carries its own dangers because we […]

The title of our blog post may sound like a directive from a Dungeon Master, but it’s firmly rooted in Galois’s forward-thinking computer science. 

C/C++ code is the foundation of our most critical systems – even “new” systems nearly always incorporate legacy code. But this type of component reuse carries its own dangers because we can’t know for sure if the components can be safely recombined in new ways. Modifying components to improve safety, security, or performance carries significant risk. 

Galois’s proposed solution is a multi-part project named POLYMORPH (Promotion to Optimal Languages Yielding Modular Operator-driven Replacements and Programmatic Hooks). It’s part of DARPA’s V-SPELLS (Verified Security and Performance Enhancement of Large Legacy Software) program

POLYMORPH seeks to allow domain experts to re-engineer legacy C/C++ systems by replacing components, recomposing existing components, and distributing components to hardware accelerators, all while improving run-time efficiency.

POLYMORPH has four major components: Levitate; Transmute and Augury; and Revivify. 

  • Levitate will provide domain experts with a visual user interface that allows them to take legacy C/C++ software components and lift them to domain-specific languages (DSLs). 
  • Transmute will provide real-time interface consistency checking to developers across component and language boundaries.
  • Augury will provide tools for model-based testing and verification of systems for ensuring semantic interoperability between the unlifted and lifted parts of code.    
  • Revivify will allow users to reassemble the extracted components into a secure and efficient system while ensuring that any compatibility requirements are preserved through the compilation process.

POLYMORPH’s planned result would allow developers to create correct-by-construction, formally verified code without needing to be formal method experts. No incantations necessary. 

For specifics on the POLYMORPH project, please see our project page

This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under Contract No. N66001-21-C-4023. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of DARPA and NIWC Pacific.

DISTRIBUTION STATEMENT C: U.S. Government agencies and their contractors. Other requests shall be referred to DARPA’s Public Release Center via email at [email protected]

Distribution Statement “A” (Approved for Public Release, Distribution Unlimited).  If you have any questions, please contact the Public Release Center.

The post Conjuring Correct-by-Construction Code That is Safely Composable System-Wide appeared first on Galois, Inc..

Source: Galois