Precise Information Flow Analysis by Program Verification

Information flow analysis algorithms for programs typically overestimate the amount of information flow that occurs in a program, since they must account for all paths through the computation graph, whether or not they are actually possible. This is the source of the information flow anomalies, which are simple situations not properly handled by syntactic information flow analysis. This paper introduces an abstract information content function for state machine models of programs, and applies it to the information firm analysis problem, in conjunction with a semantic analysis of functional behavior provided by a program verification system. Our method fits well within the framework of many existing program verification systems, requiring only a small amount of knowledge of set theory. Some of the more common information flow anomalies are shown to be handled correctly by the method.