Mechanized Information Flow Analysis through Inductive Assertions

W. A. Hunt, Jr., R. B. Krug, S. Ray, and W. D. Young

In A. Cimatti and R. B. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-aided Design (FMCAD 2008), Portland, OR, November 2008, pages 227-230. IEEE Computer Society.

© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

Abstract

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.

Relevant files


BibTex

@Inproceedings{hunt-mechanized,
  author    = "Hunt, Jr., W. A. and R. B. Krug and S. Ray and W. D. Young",
  title     = "{Mechanized Information Flow Analysis through Inductive Assertions}",
  editor    = "A. Cimatti and R. B. Jones",
  booktitle = "{Proceedings of the $8$th International Conference on 
                Formal Methods in Computer-Aided Design (FMCAD 2008)}",
  address   = "{Portland, OR}",
  month     = nov,
  pages     = "227-230",
  year      = 2008,
  publisher = "IEEE Computer Society"
}