Multi-Execution Lattices Fast and Slow

TL;DR

This paper investigates how the structure of security level lattices affects the efficiency of multi-execution methods for noninterference security policies and proposes using Galois connections to optimize performance.

Contribution

It introduces a novel approach using Galois connections to reduce multi-execution overhead based on lattice structure analysis.

Findings

Galois connections can significantly speed up multi-execution.

Lattice structure impacts the runtime overhead of multi-execution.

Empirical results confirm the effectiveness of the proposed method.

Abstract

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.