Maximilian Algehed, Cormac Flanagan
Methods for automatically, soundly, and precisely guaranteeing the noninterference security policy are predominantly based on multi-execution. All other methods are either based on undecidable theorem proving or suffer from false alarms. The multi-execution mechanisms, meanwhile, work by isolating security levels during program execution and running multiple copies of the target program, once for each security level with carefully tailored inputs that ensure both soundness and precision. When security levels are hierarchically organised in a lattice, this may lead to an exponential number of executions of the target program as the number of possible ways of combining security levels grows. In this paper we study how the lattice structure for security levels influences the runtime overhead of multi-execution. We additionally show how to use Galois connections to gain speedups in multi-execution by switching from lattices with high overhead to lattices with low overhead. Additionally, we give an empirical evaluation that corroborates our analysis and shows how Galois connections have potential to speed up multi-execution.