Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Formal Verification of Secure Programs in the Presence of Side Effects

Published

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

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 April 24, 2024)
Created January 1, 1998, Updated February 17, 2017