Mechanized Information Flow Analysis through Inductive Assertions

We present a method for verifying information flow properties of software programs using inductive assertions and theorem proving. Given a program annotated with information flow assertions at cutpoints, the method uses a theorem prover and operational semantics to generate and discharge verification conditions. This obviates the need to develop a verification condition generator (VCG) or a customized logic for information flow properties. The method is compositional: a subroutine needs to be analyzed once, rather than at each call site. The method is being mechanized in the ACL2 theorem prover, and we discuss initial results demonstrating its applicability.

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young
• Keywords: FMCAD 2008, Formal Methods, Information Flow, Information Flow Properties, Theorem Prover