Precise Enforcement of Confidentiality for Reactive Systems

In the past years, researchers have been focusing on applying information flow security to web applications. These mechanisms should raise a minimum of false alarms in order to be applicable to millions of existing web pages. A promising technique to achieve this is secure multi-execution (SME). If a program is already secure, its secure multi- execution produces the same output events; otherwise, this correspondence is intentionally broken in order to preserve security. Thus, there is no way to know if unexpected results are due to bugs or due to semantics changes produced by SME. Moreover, SME provides no guarantees on the relative ordering of output events from different security levels. We argue that these shortcomings limit the applicability of SME. In this article, we propose a scheduler for secure multi- execution which makes it possible to preserve the order of output events. Using this scheduler, we introduce a novel com- bination between monitoring and SME, called multi-execution monitor, which raises alarms only for actions breaking the non-interference notion of ID-security for reactive systems. Additionally, we show that the monitor guarantees trans- parency even for CP-similarity, a progress-sensitive notion of observation.