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, whic...

Full description

Saved in:
Bibliographic Details
Main Authors: Landauer, Christopher, Crocker, Stephen
Format: Conference Proceeding
Language:English
Subjects:
Abstracts
Aggregates
Radiation detectors
Radio access networks
Security
Semantics
Set theory
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1540-7993
1558-4046
DOI:10.1109/SP.1982.10003