Specifying and verifying the correctness of dynamic software updates. Hayden, C. M., Magill, S., Hicks, M., Foster, N., & Foster, J. S. In Proc. of the Fourth Int'l Conf. on Verified Software: Theories, Tools, Experiments, pages 278--293, 2012.
abstract   bibtex   
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 \textlessem\textgreaterclient-oriented specifications\textless/em\textgreater (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 \textlessem\textgreatermerged\textless/em\textgreater 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.
@inproceedings{hayden_specifying_2012,
	title = {Specifying and verifying the correctness of dynamic software updates},
	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 {\textless}em{\textgreater}client-oriented specifications{\textless}/em{\textgreater} (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 {\textless}em{\textgreater}merged{\textless}/em{\textgreater} 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.},
	urldate = {2012-12-27TZ},
	booktitle = {Proc. of the {Fourth} {Int}'l {Conf}. on {Verified} {Software}: {Theories}, {Tools}, {Experiments}},
	author = {Hayden, Christopher M. and Magill, Stephen and Hicks, Michael and Foster, Nate and Foster, Jeffrey S.},
	year = {2012},
	pages = {278--293}
}

Downloads: 0