  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.
