Date Added: Jun 2011
This paper explores information-flow control for batch-job programs that are allowed to be re-run with new input provided by the attacker. The authors argue that directly adapting two major security definitions for batch-job programs, termination-sensitive and termination-insensitive noninterference, to multi-run execution would result in extremes. While the former readily scales up to multiple runs, its enforcement is typically over-restrictive. The latter suffers from insecurity: secrets can be leaked in their entirety by multiple runs of programs that are secure according to batch-job termination-insensitive noninterference. Seeking to avoid the extremes, they present a framework for specifying and enforcing multi-run security in an imperative language.