Specifying and Verifying the Correctness of Dynamic Software Updates

Recently, there has been much interest in Dynamic Software Updating (DSU) systems, which allow running programs to be patched on-the-fly to add features or fix bugs. Open-source and commercial products are now available to support dynamic updates to OS kernels, desktop applications, server programs, and embedded devices. However, despite the many recent advances in DSU mechanisms, techniques to reason that dynamic updates are correct have lagged behind, focusing largely on simple properties like type safety. In this paper, the authors present a more complete framework for specifying and verifying the correctness of dynamic updates.