Information-Flow Security for Interactive Programs

dc.contributor.authorO'Neill, Kevin R.en_US
dc.contributor.authorClarkson, Michael R.en_US
dc.contributor.authorChong, Stephenen_US
dc.description.abstractInteractive programs allow users to engage in input and output throughout execution. The ubiquity of such programs motivates the development of models for reasoning about their information-flow security, yet no such models seem to exist for imperative programming languages. Further, existing language-based security conditions founded on noninteractive models permit insecure information flows in interactive imperative programs. This paper formulates new strategy-based information-flow security conditions for a simple imperative programming language that includes input and output operators. The semantics of the language enables a fine-grained approach to the resolution of nondeterministic choices. The security conditions leverage this approach to prohibit refinement attacks while still permitting observable nondeterminism. Extending the language with probabilistic choice yields a corresponding definition of probabilistic noninterference. A soundness theorem demonstrates the feasibility of statically enforcing the security conditions via a simple type system. These results constitute a step toward understanding and enforcing information-flow security in real-world programming languages, which include similar input and output operators.en_US
dc.format.extent375074 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleInformation-Flow Security for Interactive Programsen_US
dc.typetechnical reporten_US


Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
366.28 KB
Postscript Files