Specifying and Verifying the Correctness of Dynamic Software Updates
Specifying and Verifying the Correctness of Dynamic Software Updates
Files
Publication or External Link
Date
2011-11-15
Authors
Hayden, Christopher M.
Magill, Stephen
Hicks, Michael
Foster, Nate
Foster, Jeffrey S.
Advisor
Citation
DRUM DOI
Abstract
Dynamic software updating (DSU) systems allow running programs to be
patched on-the-fly to add features or fix bugs. While dynamic updates
can be tricky to write, techniques for establishing their correctness
have received little attention. In this paper, we present the first
methodology for automatically verifying the correctness of dynamic
updates. Programmers express the desired properties of an updated
execution using client-oriented specifications (CO-specs), which can
describe a wide range of client-visible behaviors. We verify CO-specs
automatically by using off-the-shelf tools to analyze a merged program,
which is a combination of the old and new versions of a program. We
formalize the merging transformation and prove it correct. We have
implemented a program merger for C, and applied it to updates for the
Redis key-value store and several synthetic programs. Using Thor, a
verification tool, we could verify many of the synthetic programs; using
Otter, a symbolic executor, we could analyze every program, often in
less than a minute. Both tools were able to detect faulty patches and
incurred only a factor-of-four slowdown, on average, compared to single
version programs.