Paul E. Black and Phillip J. Windley, Verifying Resilient Software, Thirtieth Hawai'i International Conference on System Sciences (HICSS-30), Maui, Hawai'i, USA (January 1997), edited by Ralph H. Sprague, Jr., IEEE Computer Science Press, 1997, volume V, pages 262-266.

Abstract:

    We explore the tension between adding functionality to create resilient software and minimizing functionality to make it more feasible to formally verify software. To illustrate the effects of this trade-off, we examine a tiny example in detail. We show how code written with a good style may be hard to verify, specifically that the test condition is troublesome. We also show that a test condition "improved" in an attempt to make the verification more straight-forward worsens the failure characteristics.

    To demonstrate the effect in an actual situation, we examine a secure web server, thttpd, its design principles and security features. We discuss how the security features introduce redundancies making verification harder, but also present some of its formal verification to show that verification is feasible.

    We conclude that software should be designed with necessary redundancies and that the temptation to oversimplify the design in order to formally verify it should be resisted.

Get the paper in DVI (37k), Postscript (99k), or PDF (169k).

This page's URL is /~black/Papers/hicss30.html

Updated Wed Jul 10 10:29:27 2002

Go to Black's papers or NIST home page.