Formal Verification of Secure Programs in the Presence of Side Effects

Published

January 1, 1998

Author(s)

Paul E. Black, P J. Windley

Abstract

Much software is written in industry standard programming languages, but these 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 statements (while) with pre-and post evaluation 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.

Proceedings Title

Proceedings of the Thirty-First Annual Hawaii International Conference on Systems Science, Kohala Coast, Hawaii, January 6-9, 1998

Volume

3

Conference Dates

January 1, 1998

Conference Title

Hawaii International Conference on System Sciences

Pub Type

Conferences

Keywords

axiomatic semantics, formal verification, inference rules, side effects, software security

Citation

Black, P. and Windley, P. (1998), Formal Verification of Secure Programs in the Presence of Side Effects, Proceedings of the Thirty-First Annual Hawaii International Conference on Systems Science, Kohala Coast, Hawaii, January 6-9, 1998 (Accessed October 31, 2024)