Paul E. Black and Phillip J. Windley, Formal
Verification of Secure Programs in the Presence of Side Effects,
Proceedings of the
Thirty-first Annual Hawai'i International Conference on System
Sciences (HICSS-31), Kohala Coast, Hawai'i, USA (January 1998),
edited by Ralph H. Sprague, Jr., IEEE Computer Science Press, 1998,
volume III, pages 327-334.
Much software is written in industry standard programming languages,
but these languages often have complex semantics making them hard to
formalize. For example, the use of expressions with side effects is
common in C programs. We present new inference rules for conditional
(if) statements and looping constructs (while) with
pre- and postevaluation side effects in their test expressions. These
inference rules allow us to formally reason about the security
properties of programs.
We maintain that formal verification of secure programs written in
common languages is feasible and can be worthwhile. To support our
claim, we give an example of how our verification of a secure web
server uncovered some previously unknown problems.
Automated theorem proving assistants can help deal with complex
inference rules, but many components must be brought together to make
a broadly useful system. We propose elements of a formal verification
system which could be widely useful.
Get the paper in
Postscript (122k), or
This page's URL is /~black/Papers/hicss31.html
Wed Jul 10 10:27:23 2002
by Paul E. Black
Black's papers or
NIST home page.