Paul E. Black, Axiomatic Semantics Verification of a Secure Web Server, Ph.D. dissertation, Brigham Young University, Utah, USA (February 1998).

Abstract:

    We formally verify that a particular web server written in C is secure, that is, a remote user cannot get files he shouldn't or change the server's files. Although the code was thoroughly reviewed and tested, the verification located some heretofore unknown behavioral weaknesses.

    To verify this code, we invented new inference rules for reasoning about expressions with side effects, which occur often in C. We also formalized aspects of Unix file systems and processes, operating system and library calls, parts of the C languages, and security properties.

    We propose an architecture for a software verification system which could be widely useful, and argue that our proof demonstrates that real world software written in real world languages can be verified.

Get the paper in DVI (527k), Postscript, gzip'd (243k), Postscript (735k), or PDF (870k).

The SML HOL source code files for the proof is available here.

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

Updated Thu Mar 19 10:29:24 2009

Go to Black's papers or NIST home page.