Eliminating formal flows in automated information flow analysis

Automated flow tools for formal specification languages have the potential to increase assurance and productivity of covert channel analysts by automating much of the work, but they are not reaching that potential now. Perhaps the most serious flaw in existing flow tools is that they typically report large numbers of so-called formal flows. The paper examines the causes of formal flows and describes a technique for eliminating many of them. The result is more practical automated flow analysis. The paper describes an extension for eliminating the formal flows identified by T. Fine (1992), as the major flaw in the ft-policy, and a technique for implementing the extended ft-policy in flow tools. The technique uses a construct called an opaque definition, which is essentially a hint from the specification writer to the flow tool, suggesting semantic information that might be useful in the flow analysis