Verifying resilient software

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