Deployed cyber and cyber-physical systems need to evolve to respond to newly discovered threats and maintain confidentiality, integrity, and availability. In many cases, this evolution takes the form of patches: small changes to an already-deployed system. Timely patching is crucial, but dangerous: bad patches can weaken or break a system. In high-criticality systems, full system redeployment from source may be unrealistic or too dangerous: in that case, patching vulnerable components directly at the binary level can be beneficial. Binary-level patches reduce downtime, minimize changes, and are less likely to break unrelated components. They are also often necessary when source code is unavailable.
Formal verification is an effective way to prove the correctness and security of self-contained systems, but current techniques struggle with modularity, especially at the low level (particularly challenging aspects are separate compilation and linking). As a result, formal methods for low-level patching are underdeveloped.
We are building a mathematical theory and verified tools for trustworthy low-level patching, and applying them to case studies drawn from real-world use cases, laying the groundwork for end-to-end verification of evolving critical systems.