Sciweavers

Share
FMCAD
2008
Springer

Mechanized Information Flow Analysis through Inductive Assertions

12 years 3 months ago
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.
Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FMCAD
Authors Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young
Comments (0)
books