Information-Flow Security for Interactive Programs

11 years 11 months ago
Information-Flow Security for Interactive Programs
Abstract. Interactive 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 information-flow security conditions for a simple imperative programming language that includes input and output operators, and it encapsulates user behavior as strategies. 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. ...
Kevin R. O'Neill, Michael R. Clarkson, Stephen Cho
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where CSFW
Authors Kevin R. O'Neill, Michael R. Clarkson, Stephen Chong
Comments (0)