Paul E. Black, Axiomatic Semantics Verification
of a Secure Web Server, Ph.D. dissertation, Brigham Young
University, Utah, USA (February 1998).
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
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
Postscript, gzip'd (243k),
Postscript (735k), or
The SML HOL source code files for the proof is available
This page's URL is /~black/Papers/dissertation.html
Thu Mar 19 10:29:24 2009
by Paul E. Black
Black's papers or
NIST home page.