Formal verification of secure programs in the presence of side effects

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