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
by Paul E. Black
([email protected])
Go to
Black's papers or
NIST home page.