O'Neill, K.R.Clarkson, M.R.Chong, Stephen2020-05-21O'Neill, K.R, M.R Clarkson, and S. Chong. 2006. Information-flow Security for Interactive Programs. 19th IEEE Computer Security Foundations Workshop (CSFW'06), Venice, Italy, 5-7 July 2006, 9077925. IEEE.0769526152http://nrs.harvard.edu/urn-3:HUL.InstRepos:42668601Interactive programs allow users to engage in input and output throughout execution. The ubiquity of such pro- grams motivates the development of models for reasoning about their information-flow security, yet no such models seem to exist for imperative programming languages. Fur- ther, 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 lan- guage enables a fine-grained approach to the resolution of nondeterministic choices. The security conditions lever- age this approach to prohibit refinement attacks while still permitting observable nondeterminism. Extending the lan- guage with probabilistic choice yields a corresponding def- inition of probabilistic noninterference. A soundness theo- rem demonstrates the feasibility of statically enforcing the security conditions via a simple type system. These re- sults constitute a step toward understanding and enforcing information-flow security in real-world programming lan- guages, which include similar input and output operators.en-USConference Paper2018-07-2120062020-05-2110.1109/csfw.2006.16