I. Introduction
Automatic data processing has become an important backbone of modern society. The ever-increasing amount of processed data, at finer levels of granularity, together with new economic models that focus on data acquisition, pushes the need to ensure its confidentiality. This can be achieved by enforcing security properties such as noninterference [1]. Unfortunately, traditional Information Flow Control (IFC) systems that monitor a single execution at a time are unable to do so precisely [2]. Noninterference is a 2-safety hyperproperty in nature [3], [4] and, thus, can only be validated precisely by relating sets of execution traces. This has given rise to multi-execution enforcement systems such as Secure Multi-Execution (SME) [5]. In Secure Multi-Execution, a program is executed once per level in the underlying security lattice. Each execution is responsible for output on channels with matching security classification and only has access to information from channels with equal or lower classification. It is secure by design; since output at one level is produced by an execution that does not obtain information with higher classification, there can be no interference. Given the right scheduling, SME is also transparent [6] and timing-sensitive [7]. Hence, it fulfills the main requirements for binary rewriting enforcement mechanisms as defined in Hamlen et al. [8]. Still, we do not see a lot of SME systems used in the wild.