A Taxonomy of Information Flow Monitors

Abstract

We propose a rigorous comparison of information flow monitors with respect to two dimensions: soundness and transparency.

For soundness, we notice that the standard information flow security definition called Termination-Insensitive Noninterference (TINI) allows the presence of termination channels, however it does not describe whether the termination channel was present in the original program, or it was added by a monitor. We propose a stronger notion of noninterference, that we call Termination-Aware Noninterference (TANI), that captures this fact, and thus allows us to better evaluate the security guarantees of different monitors. We further investigate TANI, and state its formal relations to other soundness guarantees of information flow monitors. For transparency, we identify different notions from the literature that aim at comparing the behaviour of monitors. We notice that one common notion used in the literature is not adequate since it identifies as better a monitor that accepts insecure executions, and hence may augment the knowledge of the attacker. To discriminate between monitors’ behaviours on secure and insecure executions, we factorized two notions that we call true and false transparency. These notions allow us to compare monitors that were deemed to be incomparable in the past.

We analyse five widely explored information flow monitors: no-sensitive-upgrade (NSU), permissive-upgrade (PU), hybrid monitor (HM), secure multi-execution (SME), and multiple facets (MF).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Motivated by the dynamic nature and an extensive list of vulnerabilities found in web applications in recent years, several dynamic enforcement mechanisms in the form of information flow monitors [5–7, 9, 12, 14, 17, 23, 27, 33], have been proposed. In the runtime monitor literature [8, 13], two properties of monitors are considered specially important: soundness and transparency. In this work, we rigorously compare information flow monitors with respect to these two dimensions. We analyse five widely explored information flow monitor techniques: no-sensitive-upgrade (NSU) [33], permissive-upgrade (PU) [6], hybrid monitor (HM) [14], secure multi-execution (SME) [12], and multiple facets (MF) [7].

Soundness. An information flow monitor is sound when it ensures that observable outputs comply with a given information flow policy. In the case of noninterference, the monitor must ensure equal observable outputs if executions start in equal observable inputs. We notice that some monitoring techniques introduce new termination channels, whereas others don’t. The standard information flow security definition called Termination-Insensitive Noninterference (TINI) does not account for termination: only initial memories in which the program terminates should lead to equal observable outputs. Thus, TINI allows the presence of termination channels, however it does not describe whether the termination channel was present in the original program, or it was added by a monitor. Termination-Sensitive Noninterference (TSNI), on the other hand, is a stronger policy that disallows the presence of any termination channel. However, most information flow monitors do not satisfy TSNI. Hence, existing definitions do not allow us to discriminate between different monitors with respect to the security guarantees that they provide. We propose a notion of noninterference, stronger than TINI but weaker than TSNI, that we call Termination-Aware Noninterference (TANI), that captures the fact that the monitor does not introduce a new termination channel, and thus allows to better evaluate the security guarantees of different monitors. We discovered that HM, SME, and MF do satisfy TANI, while NSU and PU do not satisfy TANI.

Example 1

(NSU introduces a termination channel). Consider the following program, where each variable can take only two possible values: 0 and 1.

This program is leaking confidential information – upon observing output l=0 (l=1), it’s possible to derive that h=1 (h=0). In spite of this fact, NSU allows the execution of this program starting in a memory [h=1, l=0] and blocks the execution otherwise, thus introducing a new termination channel.

Transparency. An information flow monitor is transparent when it preserves program semantics if the execution complies with the policy. In the case of noninterference, the monitor must produce the same output as an original program execution with a value that only depends on observable inputs. We identify different common notions from the literature that aim at comparing the behaviour of monitors: precision, permissiveness, and transparency. We notice that permissiveness is not adequate since it identifies as better a monitor that accepts insecure executions, and hence may augment the knowledge of the attacker, given that the attacker has knowledge based on the original executions. To discriminate between monitors’ behaviours on secure and insecure executions, we factorized two notions that we call true and false transparency. True transparency corresponds to the standard notion of transparency in the field of runtime monitoring: the ability of a monitor to preserve semantics of secure executions. An information flow monitor is false transparent when it preserves semantics of the original program execution that does not comply with the security policy. False transparency might seem contradictory to soundness at first sight but this is not the case since information flow is not a property of one execution [2, 24] but a property of several executions, also called a hyperproperty [11, 29]. These two notions of transparency allow us to compare monitors that were deemed to be incomparable in the past. In particular, we prove that HM is more TSNI precise (more true transparent for the set of TSNI secure programs) than NSU and NSU is more false transparent than HM. Proofs can be found in the companion technical report [1].

Our contributions are the following:

• 1. We propose a new information flow policy called termination-aware noninterference (TANI) that allows us to evaluate monitors according to their soundness guarantees. We prove that TANI is stronger than TINI but weaker than TSNI that disallows any termination channels.

• 2. We identify two different notions of transparency that are used in the literature as the same notion and we call them true and false transparency.

• 3. We generalize previous results from Hedin et al. [16]: we show that dynamic and hybrid monitors become comparable when the two flavors of transparency are separated into true and false transparency.

• 4. We analyse and compare five major monitors previously proved sound for TINI: NSU, PU, HM, SME and MF. Table 1 in Sect. 8 summarizes our results for TANI, true and false transparency.

2 Knowledge

We assume a two-element security lattice with $L\sqsubseteq H$ and we use $\sqcup$ as the least upper bound. A security environment $\varGamma$ maps program variables to security levels. By $\mu _\mathtt {L}$ we denote a projection of low variables of the memory $\mu$, according to an implicitly parameterized security environment $\varGamma$. The program semantics is defined as a big-step evaluation relation $({P}, \mu ) \Downarrow (v, \mu ')$, where ${P}$ is a program that produces only one output v at the end of execution. We assume that v is visible to the attacker at level $L$ and that the program semantics is deterministic. The attacker can gain knowledge while observing output v. Following Askarov and Sabelfeld [3, 4], we define knowledge as a set of low-equal memories, that lead to the program observation v.

Definition 1

(Knowledge). Given a program ${P}$, the low part $\mu _\mathtt {L}$ of an initial memory $\mu$, and an observation v, the knowledge for semantics relation $\Downarrow$ is a set of memories that agree with $\mu$ on low variables and can lead to an observation v: $k_\Downarrow ({P}, \mu _\mathtt {L}, v) = \{ \mu ' \mid \mu _\mathtt {L}= \mu '_\mathtt {L}\wedge \exists \mu ''. ({P}, \mu ') \Downarrow (v, \mu '') \}$.

Notice that knowledge corresponds to uncertainty about the environments in the knowledge set: any environment is a possible program input. The attacker believes that the environments outside of the knowledge set are impossible inputs. Upon observing a program output, the uncertainty might decrease because the new output may render some inputs impossible. This means that the knowledge set may become smaller, thus increasing the knowledge of the attacker.

To specify a security condition, we define what it means for an attacker not to gain any knowledge. Given a program ${P}$, and a low part $\mu _\mathtt {L}$ of an initial memory $\mu$, the attacker’s knowledge before the execution of the program is a set of memories that agree with $\mu$ on low variables. This set is an equivalence class of low-equal memories: $[\mu ]_\mathtt {L}= \{\mu ' \mid \mu _\mathtt {L}= \mu '_\mathtt {L}\}$.

Definition 2

(Possible outputs). Given a program ${P}$ and the low part $\mu _\mathtt {L}$ of an initial memory $\mu$, a set of observable outputs for semantics relation $\Downarrow$ is: $\mathcal O_\Downarrow ({P}, \mu _\mathtt {L}) = \{ v \mid \exists \mu ', \mu ''.\ \mu _\mathtt {L}= \mu '_\mathtt {L}\wedge ({P},\mu ') \Downarrow (v, \mu '') \}$.

In the following, we don’t write the semantics relation $\Downarrow$ when we mean the program semantics; the definitions in the rest of this section can be also used with the subscript parameter $\Downarrow$ when semantics has to be explicit.

We now specify the security condition as follows: by observing a program output, the attacker is not allowed to gain any knowledge.

Definition 3

(Termination-Sensitive Noninterference). Program ${P}$ is ter-mination-sensitively noninterferent for an initial low memory $\mu _\mathtt {L}$, written ${TSNI}({P}, \mu _\mathtt {L})$, if for all possible observations $v \in \mathcal O({P}, \mu _\mathtt {L})$, we have

$$ [\mu ]_\mathtt {L}= k({P}, \mu _\mathtt {L}, v) $$

A program ${P}$ is termination-sensitively noninterferent, written ${TSNI}(P)$, if for all possible initial memories $\mu$, ${TSNI}({P}, \mu _\mathtt {L})$.

The above definition is termination-sensitive because it does not allow an attacker to learn the secret information from program divergence. Intuitively, if the program terminates on all low-equal memories, and it produces the same output v then it satisfies TSNI. If the program doesn’t terminate on some of the low-equal memories, then for all possible observations v, the knowledge $k({P}, \mu _\mathtt {L}, v)$ becomes a subset of $[\mu ]_\mathtt {L}$ and doesn’t satisfy the definition.

Example 2

Consider Program 2. If the attacker observes that l=1, then he learns that h was 0, and if the attacker doesn’t see any program output (divergence), the attacker learns that h was 1. TSNI captures this kind of information leakage, hence TSNI doesn’t hold.

Proposition 1

${TSNI}({P})$ holds if and only if for all pairs of memories $\mu ^1$ and $\mu ^2$, we have: $\mu ^1_\mathtt {L}=\mu ^2_\mathtt {L}\wedge \exists \mu '. ({P}, \mu ^1) \Downarrow (v_1, \mu ') \Rightarrow \exists \mu ''. ({P}, \mu ^2) \Downarrow (v_2, \mu '') \wedge v_1 = v_2.$

Termination-sensitive noninterference sometimes is too restrictive as it requires a more sophisticated program analysis or monitoring that may reject many secure executions of a program. A weaker security condition, called termination-insensitive noninterference (${TINI}$), allows information flows through program divergence, while still offering information flow security.

To capture this security condition, we follow the approach of Askarov and Sabelfeld [4], by limiting the allowed attacker’s knowledge to the set of low-equal memories where the program terminates. Since termination means that some output is observable, a set that we call a termination knowledge, is a union of all knowledge sets that correspond to some program output: $\bigcup _{v'} k({P}, \mu _\mathtt {L}, v')$.

Definition 4

(Termination-Insensitive Noninterference). Program ${P}$ is termination-insensitively noninterferent for an initial low memory $\mu _\mathtt {L}$, written ${TINI}({P}, \mu _\mathtt {L})$, if for all possible observations $v \in \mathcal O({P}, \mu _\mathtt {L})$, we have

$$ \bigcup _{v' \in \mathcal O({P}, \mu _\mathtt {L})} k({P}, \mu _\mathtt {L}, v') = k({P}, \mu _\mathtt {L}, v). $$

A program ${P}$ is termination-insensitively noninterferent, written ${TINI}(P)$, if for all possible initial memories $\mu$, ${TINI}({P}, \mu _\mathtt {L})$.

Example 3

TINI recognises the Program 2 as secure, since the attacker’s termination knowledge is only a set of low-equal memories where the program terminates. For example, for $\mu _\mathtt {L}= [\texttt {{l=0}}]$, only one observation l=1 is possible when h=0, therefore ${TINI}$ holds: $\bigcup _{v' \in \{1\}} k({P}, \texttt {{l=0}}, v') = [\texttt {{h=0, l=0}}] = k({P}, \texttt {{l=0}}, \texttt {{1}})$.

Proposition 2

${TINI}({P})$ holds if and only if for all pairs of memories $\mu ^1$ and $\mu ^2$, we have: $\mu ^1_\mathtt {L}=\mu ^2_\mathtt {L}\wedge \exists \mu '. ({P}, \mu ^1) \Downarrow (v_1, \mu ') \wedge \exists \mu ''. ({P}, \mu ^2) \Downarrow (v_2, \mu '') \Rightarrow v_1 = v_2.$

3 Monitor Soundness

In this section, we consider dynamic mechanisms for enforcing information flow security. For brevity, we call them “monitors”. The monitors we consider are purely dynamic monitors, such as NSU and PU, hybrid monitors in the style of Le Guernic et al. [20, 21] that we denote by HM, secure multi-execution (SME), and multiple facets monitor (MF). All the mechanisms we consider have deterministic semantics denoted by $\Downarrow _M$, where M represents a particular monitor. All the monitors enforce at least termination-insensitive noninterference (TINI).¹ Since TINI accepts termination channels, it also allows the monitor to introduce new termination channels even if an original program did not have any. In the next section, we will propose a new definition for soundness of information flow monitors, capturing that a monitor should not introduce a new termination channel. But, first, we set up the similar definitions of termination-sensitive and -insensitive noninterference for a monitored semantics. Instead of using a subscript $\Downarrow _M$ for a semantics of a monitor M, we will use a subscript M.

Definition 5

(Soundness of TSNI enforcement). Monitor M soundly enforces termination-sensitive noninterference, written ${TSNI}(M)$, if for all possible programs ${P}$, $TSNI_{M}({P})$.

Proposition 1 proves that this definition of TSNI soundness is equivalent to the standard two-run definition if we substitute the original program semantics with the monitor semantics. Similarly, to define a sound TINI monitor, we restate Definition 4 of TINI with the monitored semantics. The definition below is equivalent to the standard two-run definition (see Proposition 2).

Definition 6

(Soundness of TINI enforcement). Monitor M soundly enforces termination-insensitive noninterference, written ${TINI}(M)$, if for all possible programs ${P}$, ${TINI}_M({P})$.

This definition compares the initial knowledge and the final knowledge of the attacker under the monitor semantics. But in practice, an attacker has also the initial knowledge of the original program semantics (see Example 1).

4 Termination-Aware Noninterference

We propose a new notion of soundness for the monitored semantics, called Termination-Aware Noninterference (TANI) that does not allow a monitor to introduce a new termination channel.

Intuitively, all the low-equal memories, on which the original program terminates, should be treated by the monitor in the same way, meaning the monitor should either produce the same result for all these memories, or diverge on all of them. In terms of knowledge, it means that the knowledge provided by the monitor, should be smaller or equal than the knowledge known by the attacker before running the program. Additionally, in the case the original program always diverges, TANI holds if the monitor also always diverges or if the monitor always terminates in the same value.

Definition 7

(Termination-Aware Noninterference). A monitor $\Downarrow _M$ is Termination-Aware Noninterferent (TANI), written ${TANI}(M)$, if for all programs ${P}$, initial memories $\mu$, and possible observations $v \in \mathcal O_M({P}, \mu _\mathtt {L})$, we have:

• $\mathcal O({P}, \mu _\mathtt {L}) \ne \emptyset ~ \implies ~ \bigcup _{v' \in \mathcal O({P}, \mu _\mathtt {L})} k({P}, \mu _\mathtt {L}, v') \subseteq k_M({P}, \mu _\mathtt {L}, v)$

• $\mathcal O({P}, \mu _\mathtt {L}) = \emptyset ~ \implies (\mathcal O_M({P}, \mu _\mathtt {L})= \emptyset \vee [\mu ]_\mathtt {L}= k_M({P}, \mu _\mathtt {L}, v) )$

Notice that, for the case that the original program sometimes terminate ($\mathcal O({P}, \mu _\mathtt {L}) \ne \emptyset )$), we do not require equality of the two sets of knowledge since the knowledge set of the monitored program can indeed be bigger than the knowledge set of the attacker before running the program². The knowledge set may increase when a monitor terminates on the memories where the original program did not terminate (e.g., SME from Sect. 5 provides such enforcement).

Example 4

(TANI enforcement). Coming back to Program 1, TANI requires that on two low-equal memories [h=0, l=0] and [h=1, l=0] where the original program terminates, the monitor behaves in the same way: either it terminates on both memories producing the same output, or it diverges on both memories.

It is well-known that TSNI is a strong form of noninterference that implies TINI. We now formally state the relations between TINI, TANI and TSNI.

Theorem 1

${TSNI}(M) \Rightarrow {TANI}(M)$ and ${TANI}(M) \Rightarrow {TINI}(M)$.

5 Which Monitors Are TANI?

We now present five widely explored information flow monitors and prove whether these monitors comply with TANI. In order to compare the monitors, we first model all of them in the same language. Thus, our technical results are based on a simple imperative language with one output (see Fig. 1). The language’s expressions include constants or values (v), variables (x) and operators ($\oplus$) to combine them. We present the standard big-step program semantics in Fig. 2.

Fig. 1.

Language syntax

Fig. 2.

Language semantics

The semantics relation of a command ${S}$ is denoted by $pc \vdash (\varGamma , {S}, \mu ) \Downarrow _M (\varGamma ', \mu ')$ where pc is a program counter, M is the name of the monitor and $\varGamma$ is a security environment mapping variables to security levels. All the considered monitors are flow-sensitive, and $\varGamma$ may be updated during the monitored execution. We assume that the only output produced by the program is visible to the attacker at level $L$. Since our simple language supports only one output at the end of the program, the output rule of the monitors is defined only for $pc = L$, and thus only checks the security level of an output variable x.

No-Sensitive Upgrade (NSU). The no-sensitive upgrade approach (NSU) first proposed by Zdancewic [33] and later applied by Austin and Flanagan [5] is based on a purely dynamic monitor that controls only one execution of the program. To avoid implicit information flows, the NSU disallows any upgrades of a low security variables in a high security context. Consider Program 1: since the purely dynamic monitor accepts its execution when h=1, it should block the execution when h=0 to enforce TINI. NSU does so by blocking the second execution since the low variable l is updated in a high context

Fig. 3.

NSU semantics

Our NSU formalisation for a simple imperative language is similar to that of Bichhawat et al. [10]. The main idea of NSU appears in the assign rule: the monitor blocks “sensitive upgrades” when a program counter level pc is not lower than the level of the assigned variable x. Figure 3 represents the semantics of NSU monitor. We use $\varGamma (e)$ as the least upper bound of all variables occurring in expression e. If e contains no variables, then $\varGamma (e)=L$. NSU was proven to enforce termination-insensitive noninterference (TINI) (see [5, Theorem 1]).

Example 5

(NSU is not TANI). Consider Program 1 and an initial memory [h=1, l=0]. NSU does not satisfy TANI, since the monitor terminates only on one memory, i.e., $k_M({P}, \mu _\mathtt {L}, v)$ = [h=1, l=0], while the original program terminates on both memories, low-equal to [l=0].

Permissive Upgrade (PU). The NSU approach suffices to enforce TINI, however it often blocks a program execution pre-emptively. Consider  Program 3. This program is TINI, however NSU blocks its execution starting in memory  [h=0, l=0] because of a sensitive upgrade under a high security context.

Austin and Flanagan proposed a less-restrictive strategy called permissive upgrade (PU) [6]. Differently from NSU, it allows the assignments of low variables under a high security context, but labels the updated variable as partially-leaked or ’P’. Intuitively, P means that the content of the variable is H but it may be L in other executions. If later in the execution, there is a branch on a variable marked with P, or such variable is to be output, the monitor stops the execution.

Fig. 4.

PU semantics

We present a permissive upgrade monitor (PU) for a two-point lattice extended with label P with $H \sqsubset P$. The semantics of PU is identical to the one of NSU (see Fig. 3) except for the assign and if rules, that we present in Fig. 4. Rule assign behaves like the assign rule of NSU, if $pc \sqsubseteq \varGamma (x)$ and $\varGamma (x) \ne P$. Otherwise, the assigned variable is marked with P. Rule if is similar to the rule if in NSU, but the semantics gets stuck if the variable in the test condition is partially leaked. PU was proven to enforce TINI (see [6, Theorem 2]). However, PU is not TANI since it has the same mechanism as NSU for adding new termination channels.

Example 6

(PU is not TANI). Consider  Program 1 and an initial memory [h=1, l=0]. PU does not satisfy TANI, since the monitor terminates only on one memory, i.e., $k_M({P}, \mu _\mathtt {L}, v)$ = [h=1, l=0], while the original program terminates on both memories, low-equal to [l=0].

Hybrid Monitor (HM). Le Guernic et al. were the first to propose a hybrid monitor (HM)  [14] for information flow control that combines static and dynamic analysis. This mechanism statically analyses the non-executed branch of each test in the program, collecting all the possibly updated variables in that branch. The security level of such variables are then raised to the level of the test, thus preventing information leakage.

Example 7

Consider  Program 1 and its execution starting in [h=1, l=0]. This execution is modified by HM because the static analysis discovers that variable l could have been updated in a high security context in an alternative branch.

Fig. 5.

HM semantics

The semantics of HM is identical to NSU except for the assign, if and output rules that we show in Fig. 5. The assign rule does not have any specific constraints. The static analysis $\mathsf{Analysis}({S}, pc, \varGamma )$ in the if rule explores variables assigned in ${S}$ and upgrades their security level according to pc. We generalize the standard notation $\varGamma [x \mapsto l]$ to sets of variables and use $\mathsf{Vars}({S})$ for the sets of variables assigned in command ${S}$.

$$ \mathsf{Analysis}({S},pc,\varGamma ) = \varGamma [\{ y \mapsto pc \sqcup \varGamma (y) \mid y \in \mathsf{Vars}({S}) \} $$

HM was previously proven to enforce TINI [14, Thm.1] and we prove in the companion technical report [1] that HM satisfies TANI.

Theorem 2

HM is TANI.

Secure Multi-Execution (SME). Devriese and Piessens were the first to propose secure multi-execution (SME)  [12]. The main idea of SME is to execute the program multiple times: one for each security level. Each execution receives only inputs visible to its security level and a fixed $\textsf {default}$ value for each input that should not be visible to the execution. Different executions are executed with a low priority scheduler to avoid leaks due to divergence of high executions because SME enforces TSNI.

Example 8

(SME “fixes” termination channels). Consider Program 4:

Assume $\mu _\mathtt {L}= [\texttt {{l=0}}]$ and the default high value used by SME is h=1. Then, there exists a memory $\mu '$ = [h=0, l=0], low-equal to $\mu _\mathtt {L}$, on which the original program doesn’t terminate: $\mu ' \not \in \bigcup _{v'} k({P}, \mu _\mathtt {L}, v')$, but SME terminates: $\mu ' \in k_M({P}, \mu _\mathtt {L}, \texttt {{l=0}})$. Notice that SME makes the attacker’s knowledge smaller.

Fig. 6.

SME semantics

The SME adaptation for our while language is given in Fig. 6, with executions for levels L and H. The special value $\bot$ represents the idea that no value can be observed and we overload the symbol to also denote a memory that maps every variable to $\bot$. Using memory $\bot$ we simulate the low priority scheduler of SME in our setting: if the execution corresponding to the H security level does not terminate, the SME semantics still terminates. In this case all the variables with level H, which values should correspond to values obtained in the normal execution of the program, are given value $\bot$.

SME was previously proven TSNI [12, Theorem 1] and we prove that it also enforces TANI: this can be directly inferred from our Theorem 1.

Theorem 3

SME is TANI.

Multiple Facets. Austin and Flanagan proposed multiple facets (MF) in [7]. In MF, each variable is mapped to several values or facets, one for each security level: each value corresponds to the view of the variable from the point of view of observers at different security levels. The main idea in MF is that if there is a sensitive upgrade, MF semantics does not update the observable facet. Otherwise, if there is no sensitive upgrade, MF semantics updates it according to the original semantics.

Example 9

Consider the TINI  Program 5. In MF, the output observable at level L (or the L facet of variable l) is always the initial value of variable l since MF will not update a low variable in a high context. Therefore, all the executions of  Program 5 starting with l=1 are modified by MF, producing the output l=1.

Fig. 7.

Multiple Facets semantics

Our adaptation of MF semantics is given in Fig. 7 where we use the following notation: a faceted value, denoted $\langle v_1:v_2\rangle$, is a pair of values $v_1$ and $v_2$. The first value presents the view of an observer at level H and the second value the view of an observer at level L. In the syntax, we interpret a constant v as the faceted value $\langle v:v\rangle$. Faceted memories, ranged over $\hat{\mu }$, are mappings from variables to faceted values. We use the notation $\hat{\mu }(x)_i$ ($i\in \{1,2\}$) for the first or second projection of a faceted value stored in x. As in SME, the special value $\bot$ represents the idea that no value can be observed. MF was previously proven TINI [7, Theorem 2] and we prove that it satisfies TANI.

Theorem 4

MF is TANI.

6 Precision, Permissiveness and Transparency

A number of works on dynamic information flow monitors try to analyse precision of monitors. Intuitively, precision describes how often a monitor blocks (or modifies) secure programs. Different approaches have been taken to compare precision of monitors, using definitions such as “precision”, “permissiveness” and “transparency”. We propose a rigorous comparison of these definitions.

In the field of runtime monitoring, a monitor should provide two guarantees while enforcing a security property: soundness and transparency. Transparency [8] means that whenever an execution satisfies a property in question, the monitor should output it without modifications³.

Precision (versus well typed programs). Le Guernic et al. [21] were among the first to start the discussion on transparency for information flow monitors. The authors have proved that their hybrid monitor accepts all the executions of a program that is well typed under a flow-insensitive type system similar to the one of Volpano et al. [31]. Le Guernic [19] names this result as partial transparency. Russo and Sabelfeld [25] prove a similar result: they show that a hybrid monitor accepts all the executions of a program that is well typed under the flow-sensitive type system of Hunt and Sands [18].

Precision (versus secure programs). Devriese and Piessens [12] propose a stronger notion, called precision, that requires a monitor to accept all the executions of all secure programs. Notice that this definition is stronger because not only the monitor should recognise the executions of well typed programs, but also of secure programs that are not well typed. Devriese and Piessens have proven that such precision guarantee holds for SME versus TSNI programs.

Transparency (versus secure executions). As a follow-up, Zanarini et al. [32] have proven that another monitor based on SME satisfies transparency for TSNI. This monitor accepts all the TSNI executions of a program, even if the program itself is insecure.

Permissiveness (versus executions accepted by other monitors). In his PhD thesis, Le Guernic [19] compares his hybrid monitor with another hybrid monitor that performs a more precise static analysis, and proves an improved precision theorem stating that whenever the first hybrid monitor accepts an execution, the second monitor accepts it as well. Following this result, Besson et al. [9] investigate other hybrid monitors and prove relative precision in the style of Le Guernic, and Austin and Flanagan [6, 7] use the same definition to compare their dynamic monitors. Hedin et al. [16] name the same notion by permissiveness and compare the sets of accepted executions: one monitor is more permissive than another one if its set of accepted executions contains a set of accepted executions of the other monitor.

To compare precision of different information flow monitors, we propose to distinguish two notions of transparency. True transparency defines the secure executions accepted by a monitor, and false transparency defines the insecure executions accepted by a monitor.

True Transparency. We define a notion of true transparency for TINI. Intuitively, a monitor is true transparent if it accepts all the TINI executions of a program.

Definition 8

(True Transparency). Monitor M is true transparent if for any program ${P}$, and any memories $\mu$, $\mu '$ and output v, the following holds:

$$ {TINI}({P}, \mu _\mathtt {L}) \wedge ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ') $$

There is a well-known result that a truncation automata cannot recognise more than computable safety properties [15, 28]. Since noninterference can be reduced to a safety property that is not computable [29], and NSU and PU can be modeled by truncation automata, it follows that they are not true transparent. We show that the monitors of this paper, that cannot be modeled by truncation automata, are not true transparent for TINI neither.

Example 10

(HM is not true transparent). Consider  Program 5: it always terminates with l=0 and hence it is secure. Any execution of this program will be modified by HM because l will be marked as high.

Example 11

(MF is not true transparent). Consider again TINI  Program 5. The MF semantics will not behave as the original program semantics upon an execution starting in [h=1, l=1]. The sensitive upgrade of the test will assign faceted value $\left[ {\texttt {l=}}\langle 0:1\rangle \right]$ to variable l and the output will produce the low facet of l which is 1, while the original program would produce an output 0. Hence, this is a counter example for true transparency of MF.

Example 12

(SME is not true transparent for TINI). Since SME enforces TSNI, it eliminates all the termination channels, therefore even if the original program has TINI executions, SME might modify them to achieve TSNI.

Consider TINI  Program 4 and an execution starting in [h=0,l=1]. SME (with default value h=1) will diverge because it’s “low” execution will diverge upon h=1. Therefore, SME is not true transparent for TINI.

Even though none of the considered monitors are true transparent for TINI, this notion allows us to define a relative true transparency to better compare the behaviours of information flow monitors when they deal with secure executions.

Given a program ${P}$ and a monitor M, we define a set of initial memories that lead to secure terminating executions of program ${P}$, and a monitor M does not modify these executions:

$$ \mathcal {T}(M, {P}) = \{ \mu \mid {TINI}({P}, \mu _\mathtt {L}) \wedge \exists \mu ', v.\ ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ')\} $$

Definition 9

(Relative True Transparency). Monitor A is more true transparent than monitor B, written $A \supseteq _{\mathcal {T}}B$, if for any program ${P}$, the following holds: $\mathcal {T}(A, {P}) \supseteq \mathcal {T}(B, {P}).$

Austin and Flanagan [5, 6] have proven that MF is more true transparent than PU and PU is more true transparent than NSU. We restate this result in our notations and provide a set of counterexamples showing that for no other couple of analysed monitors relative true transparency holds.

Theorem 5

$MF \supseteq _{\mathcal {T}}PU \supseteq _{\mathcal {T}}NSU$.

Example 13

($NSU \not \supseteq _{\mathcal {T}}PU, NSU \not \supseteq _{\mathcal {T}}HM$) Consider TINI  Program 3: an execution in initial memory with [h=0] is accepted by PU and HM because the security level of l becomes low just before the output, and it is blocked by NSU due to sensitive upgrade.

Example 14

($NSU \not \supseteq _{\mathcal {T}}SME, NSU \not \supseteq _{\mathcal {T}}MF, PU \not \supseteq _{\mathcal {T}}HM$, $PU \not \supseteq _{\mathcal {T}}SME$ and $PU \not \supseteq _{\mathcal {T}}MF$).

 Program 6 is TINI since l’ does not depend on h. With initial memory [h=0, l=1], HM, SME (with default value chosen as 0) and MF terminate with the same output as normal execution. However, NSU will diverge due to sensitive upgrade and PU will diverge because of the branching over a partially-leaked variable l.

Example 15

($HM \not \supseteq _{\mathcal {T}}NSU, HM \not \supseteq _{\mathcal {T}}PU, HM \not \supseteq _{\mathcal {T}}SME, HM \not \supseteq _{\mathcal {T}}MF$). Consider  Program 1 and its secure execution starting in [h=1, l=1]. NSU, PU, SME (the default value of SME does not matter in this case) and MF terminate with the same output as original program execution, producing l=1. However, HM modifies it because the security level of l is raised by the static analysis of the non-executed branch.

Example 16

($SME \not \supseteq _{\mathcal {T}}NSU, SME \not \supseteq _{\mathcal {T}}PU, SME \not \supseteq _{\mathcal {T}}HM, SME \not \supseteq _{\mathcal {T}}MF$). All the terminating executions of TINI  Program 4 are accepted by NSU, PU, HM and MF, while an execution starting in [h=0, l=1] with default value for SME set to h=1 doesn’t terminate in SME semantics.

Example 17

($MF \not \supseteq _{\mathcal {T}}HM$).  Program 7 is TINI for any execution. HM with [h=1,l=0,l’=0] terminates with the original output because the output variable [l’] is low. However, MF with [h=1,l=0,l’=0] doesn’t terminate.

Example 18

($MF \not \supseteq _{\mathcal {T}}SME$).  Program 5 is TINI for any execution. With [h=0, l=1] it terminates in the program semantics and SME semantics (with any default value) producing l=0. However, the MF semantics produces l=1.

Precision We have discovered that certain monitors (e.g., HM and NSU) are incomparable with respect to true transparency. To compare them, we propose a more coarse-grained definition that describes the monitors’ behaviour on secure programs.

Definition 10

(Precision). Monitor M is precise if for any program ${P}$, the following holds:

$$ {TINI}({P}) \wedge \forall \mu . (\exists \mu ', v. ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ')) $$

This definition requires that all the executions of secure programs are accepted by the monitor. NSU, PU, HM and MF are not precise since they are not true transparent. SME is precise for TSNI, and this result was proven by Devriese and Piessens [12], however SME it not precise for TINI (see Example 12).

To compare monitors’ behaviour on secure programs, we define a set of a TINI programs ${P}$, where a monitor accepts all the executions of ${P}$:

$$ \mathcal {P}(M) = \{ {P}\mid {TINI}(P) \wedge \forall \mu . (\exists \mu ', v. ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ')) \} $$

Definition 11

(Relative Precision). Monitor A is more precise than monitor B, written $A \supseteq _{\mathcal {P}}B$, if $\mathcal {P}(A) \supseteq \mathcal {P}(B).$

We have found out that no couple of the five monitors are in relative precision relation. Below we present the counterexamples that demonstrate our findings.

Example 19

($HM \not \supseteq _{\mathcal {P}}SME$). Consider TINI  Program 5. All the executions of this program are accepted by SME. However, HM modifies the program output to default because the security level of l is upgraded to H by the static analysis of the non-executed branch.

Example 20

($HM \not \supseteq _{\mathcal {P}}NSU$, $HM \not \supseteq _{\mathcal {P}}PU$). Consider the following program:

This TINI program terminates only when [h=0]. This execution is accepted by NSU and PU, but the program output is modified by HM since HM analyses the non-executed branch and upgrades the level of l to $H$.

Example 21

($HM \not \supseteq _{\mathcal {P}}MF$). Consider TINI  Program 9. MF accepts all of its executions, while HM modifies the program output to default because the security level of l is raised to high.

The rest of relative precision counterexamples demonstrated in Table 1 of Sect. 8 are derived from the corresponding counterexamples for relative true transparency.

Since relative precision does not hold for any couple of monitors, we propose a stronger definition of relative precision for TSNI programs. We first define a set of a TSNI programs ${P}$, where a monitor accepts all the executions of ${P}$:

$$ \mathcal {P}^*(M) = \{ {P}\mid {TSNI}(P) \wedge \forall \mu . (\exists \mu ', v. ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ')) \} $$

Definition 12

(Relative TSNI precision). A monitor A is more TSNI precise than a monitor B, written $A \supseteq _{\mathcal {P}}^*B$, if $\mathcal {P}^*(A) \supseteq \mathcal {P}^*(B)$.

Theorem 6

For all programs without dead code, $HM \supseteq _{\mathcal {P}}^*NSU, HM \supseteq _{\mathcal {P}}^*PU$.

Notice that SME was proven to be precise for TSNI programs (see [12, Theorem 2]), therefore SME is more TSNI precise than any other monitor. We demonstrate this in Table 1 of Sect. 8.

False Transparency To compare monitors with respect to the amount of insecure executions they accept, we propose the notion of false transparency. Notice that false transparency violates soundness.

Definition 13

(False Transparency). Monitor M is false transparent if for any program ${P}$, for all executions starting in a memory $\mu$ and finishing in memory $\mu '$ with value v, the following holds:

$$ \lnot {TINI}({P}, \mu ) \wedge ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v,\mu '). $$

Given a program ${P}$ and a monitor M, we define a set of initial memories, where a program ${P}$ terminates, and a monitor M is false transparent for ${P}$:

$$ \mathcal {F}(M, {P}) = \{ \mu \mid \lnot {TINI}({P}, \mu _\mathtt {L}) \wedge \exists \mu ', v. ({P}, \mu ) \Downarrow (v, \mu ') \Rightarrow ({P}, \mu ) \Downarrow _M(v, \mu ')\} $$

Definition 14

(Relative False Transparency). Monitor A is more false transparent than monitor B, denoted $A \supseteq _{\mathcal {F}}B$, if for any program ${P}$, the following holds: $\mathcal {F}(A, {P}) \supseteq \mathcal {F}(B, {P}).$

Theorem 7

The following statements hold: $NSU \supseteq _{\mathcal {F}}HM$, $PU \supseteq _{\mathcal {F}}NSU$, $PU \supseteq _{\mathcal {F}}HM$, $SME \supseteq _{\mathcal {F}}HM$, $MF \supseteq _{\mathcal {F}}NSU$, $MF \supseteq _{\mathcal {F}}PU$ and $MF \supseteq _{\mathcal {F}}HM$.

Example 22

($NSU \not \supseteq _{\mathcal {F}}PU$). Execution of  Program 10 in the initial memory $\mu$= [h=0, l=0, l’=0] is interfering since it produces an output l=0, while an execution in the low-equal initial memory where [h=1] produces l=1. An execution started in $\mu$ is accepted by PU but blocked by NSU.

Example 23

($NSU \not \supseteq _{\mathcal {F}}SME$, $PU \not \supseteq _{\mathcal {F}}SME$). Execution of  Program 11 starting in memory [h=0, l=0] is not TINI and it is accepted by SME (with default value h=0). However, it is rejected by NSU because of sensitive upgrade and by PU because on the branching over a partially-leaked variable l.

Example 24

($NSU \not \supseteq _{\mathcal {F}}MF$). The following program always terminates in the normal semantics coping the value of h into l. Hence all of its executions are insecure. Every execution leads to a sensitive upgrade and NSU will diverge with any initial memory. However, in the MF semantics the program will terminate with l=0 if started with memory [h=0,l=0] since the sensitive upgrade of the true branch will assign faceted value $\left[ {\texttt {l=}}\langle 0:0\rangle \right]$ to variable l. Hence, this is a counter example for NSU being more false transparent than MF.

Example 25

($PU \not \supseteq _{\mathcal {F}}MF$).  Program 11 is not TINI for all executions. However MF with [h=1,l=1,l’=1] terminates in the same memory as normal execution, while PU will diverge because l is marked as a partial leak.

Example 26

($HM \not \supseteq _{\mathcal {F}}NSU$, $HM \not \supseteq _{\mathcal {F}}PU$, $HM \not \supseteq _{\mathcal {F}}SME$, $HM \not \supseteq _{\mathcal {F}}MF$). Consider  Program 1 and an execution starting in memory [h=1, l=0]. This execution is not secure and it is rejected by HM, however NSU, PU and MF accept it. SME also accepts this execution in case the default value for h is 1.

Example 27

($SME \not \supseteq _{\mathcal {F}}NSU$, $SME \not \supseteq _{\mathcal {F}}PU$). Execution of  Program 13 starting in memory [h=0, l=0] is interfering and it is accepted by both NSU and PU, producing an output l=0. However, SME (with default value chosen as 1) modifies this execution and produces l=1.

Example 28

($SME \not \supseteq _{\mathcal {F}}MF$ and $MF \not \supseteq _{\mathcal {F}}SME$).  Program 14 is not TINI if possible values of h are 0, 1, and 2. MF with [h=1,l=1] terminates in the same memory than normal execution but SME (with default value 0) always diverges.

On the other hand, with initial memory [h=1, l=0], SME (using default value 1) terminates in the same memory as the normal execution, producing l=1 but MF produces a different output l=0.

7 Related Work

In this section, we discuss the state of the art for taxonomies of information flow monitors with respect to soundness or transparency.

For soundness, no work explicitly tries to classify information flow monitors. However, it is folklore that TSNI, first proposed in [30], is a strong form of noninterference that implies TINI. Since most well-known information flow monitors are proven sound only for TINI [5–7, 14, 33], it is easy, from the soundness perspective, to distinguish SME from other monitors because SME is proven sound for TSNI [12]. However, to the best of our knowledge, no work tries to refine soundness in order to obtain a more fine grain classification of monitors as we achieve with the introduction of TANI.

For transparency, Devriese and Piessens [12] prove that SME is precise for TSNI and Zanarini et al. [32] notice that the result could be made more general by proving that SME is true transparent for TSNI, which makes of SME an effective enforcement [22] for TSNI. In this work, we first compare transparency for TINI: none of the monitors that we have studied is true transparent for TINI. Hedin et al. [16] compare hybrid (HM) and purely dynamic monitors (NSU and PU), and conclude that for these monitors permissiveness is incomparable. By factorizing the notion of permissiveness, we can compare HM and NSU: HM is more precise for TSNI than NSU and PU, and NSU and PU are more false transparent than HM. Using the same definition of permissiveness, Austin and Flanagan [6, 7] prove that PU is more permissive than NSU and that MF is more permissive than PU. Looking at this result and the definition of MF, our intuition was that MF could accept exactly the same false transparent executions as NSU and PU. However, we discovered that not only MF is more true transparent than NSU and PU (this is an implication of Austin and Flanagan results) but also MF is strictly more false transparent than NSU and PU. Bichhawat et al. [10] propose two non-trivial generalizations of PU, called puP and puA, to arbitrary lattices and show that puP and puA are incomparable w.r.t. permissiveness. It remains an open question if puP and puA can be made comparable by discriminating true or false transparency, as defined in our work.

8 Conclusion

In this work we proposed a new soundness definition for information flow monitors, that we call Termination-Aware Noninterference (TANI). It determines whether a monitor adds a new termination channel to the program. We have proven that HM, SME and MF, do satisfy TANI, whereas NSU and PU introduce new termination channels, and therefore do not satisfy TANI.

We compare monitors with respect to their capability to recognise secure executions, i.e., true transparency [8]. Since it does not hold for none of the considered monitors, we weaken this notion and define relative true transparency, that determines “which monitor is closer to being transparent”. We then propose even a more weaker notion, called precision, that compares monitor behaviours on secure programs, and allows us to conclude that HM is more TSNI precise than NSU and PU that previously were deemed incomparable [16]. We show that the common notion of permissiveness is composed of relative true and false transparency and compare all the monitors with respect to these notions in Table 1.

Table 1. Taxonomy of five major information flow monitors

For simplicity, we consider a security lattice of only two elements, however we expect our results to generalise to multiple security levels. In future work, we plan to compare information flow monitors with respect to other information flow properties, such as declassification [26].