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.

Abstract:

    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 DVI (53k), Postscript (122k), or PDF (192k).

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

Updated Wed Jul 10 10:27:23 2002

Go to Black's papers or NIST home page.