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

• Type: Conference
• Year: 2006
• Where: CSFW
• Authors: Kevin R. O'Neill, Michael R. Clarkson, Stephen Chong
• Keywords: CSFW 2006, Imperative Programming Language, Information-flow Security, Security Conditions, Security Privacy