Gurvan Le Guernic
email: gleguern@gmail.com

Precise Dynamic Verification of Noninterference

Confidentiality is maybe the most popular security property to be formally or informally verified. Noninterference is a baseline security policy to formalize confidentiality of secret information manipulated by a program. Many static analyses have been developed for the verification of noninterference. In contrast to those static analyses, this paper considers the run-time verification of the respect of confidentiality by a single execution of a program. It proposes a dynamic noninterference analysis for sequential programs based on a combination of dynamic and static analyses. The static analysis is used to analyze some unexecuted pieces of code in order to take into account all types of flows. The static analysis is sensitive to the current program state. This sensitivity allows the overall dynamic analysis to be more precise than previous work. The soundness of the overall dynamic noninterference analysis with regard to confidentiality breaches detection and correction is proved.

Introduction

Language-based security is an active field of research. The majority of work on confidentiality in this field focuses on static analyses [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Recent years have seen a resurgence of dynamic analyses aiming at enforcing confidentiality at run time [START_REF] Guernic | Automaton-based Confidentiality Monitoring of Concurrent Programs[END_REF][START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF][START_REF] Shroff | Dynamic dependency monitoring to secure information flow[END_REF]. The first reason is that nowadays it is nearly impossible for consumers to prevent the execution of "bad" code on their devices -for example, in September 2007 Yahoo served 12 million times a flash ad installing a Trojan horse [START_REF] Goodin | Yahoo feeds Trojan-laced ads to MySpace and PhotoBucket users[END_REF] and cybercriminals introduced malicious scripts into webpages of a US Consulate [START_REF] Leyden | Trojan planted on US Consulate website[END_REF]. Moreover, there are two main potential advantages of dynamic analyses over static analyses [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF]. The first one is the increased knowledge of the execution environment and behavior at run time, including the knowledge of the precise control flow followed by the current execution. This increased knowledge allows the dynamic analysis to be more precise than a static analysis in some cases; as, for example, with the program on page 14. The second advantage lies in the ability of sound information flow monitors to run some "safe" executions of an "unsafe" program while still guarantying the confidentiality of secret data. In order to take into account all indirect flows (flows originating in control statements) dynamic analyses relies on static analyses of some, but not all, unexecuted pieces of code.

This paper proposes to increase the precision of such dynamic information flow analyses. This is done by taking advantage, at the static analysis level, of the dynamic nature of the overall analysis. To do so, when statically analyzing an unexecuted piece of code, the current program state is taken into account in order to reduce the program space to analyze. The following piece of code is a motivating example for this work. It corresponds to the body of the main loop of an Instant Messaging (IM) program. This one has the appealing "movie-like" feature of displaying messages characters by characters as they are typed. This IM program is a malware developed by "sexyPirate". When someone uses this software to communicate with a user other than sexyPirate, everything goes as expected and no secret is revealed. However, if a user communicates with sexyPirate using this IM then information about the user's secret key is leaked to the pirate. When the integer value of the characters typed by the user since the last time tmp has been reset to 0 reaches the integer value of the user's secret key, a special character (that sexyPirate is able to distinguish) appears on the pirate's screen. Therefore, by iterating the process, sexyPirate is able to get an accurate approximation of the user's secret key. Any sound static analysis would reject this program; and therefore, all its executions. One of the advantages of dynamic information flow analysis, if it is precise enough, is to allow use of this program for communicating with users other than sexyPirate, while still guarantying the confidentiality of the secret key in any case. However, none of the previous work are precise enough. When statically analyzing lines 4 and 5, no knowledge about the value of the variable to is taken into account. Therefore, the overall dynamic analysis will always consider that the value of c may be modified; which implies a flow from userSecretKey to c. With such dynamic analyses, line 7 must then be corrected in order to prevent any potential leakage of the value of the secret key to the outside world. In the work proposed in this paper, the static analysis used for lines 4 and 5 takes into account the run time value of the variable to. This allows the overall dynamic analysis proposed to detect that there is no flow from userSecretKey to c whenever to is different from sexyPirate. Therefore, it allows use of this IM program for communicating with any user different from sexyPirate; while still preserving the confidentiality of the user's secret key even when trying to use this program to communicate with sexyPirate.

The next section defines various notions used in this paper and introduces the principles of the dynamic analysis proposed in this paper. Section 3 formalizes the dynamic information flow analysis. The main properties of this analysis are exposed in Sect. 4 before concluding in Sect. 6.

Definitions and Principles

The current section starts by introducing some terminology. It then gives some formal definitions which are used to formalize the execution property that the dynamic analysis has to verify. Subsequently, it introduces succinctly the principles of the dynamic analysis.

A direct flow is a flow from the right side of an assignment to the left side. Executing "x := y" creates a direct flow from y to x. An explicit indirect flow is a flow from the test of a conditional to the left side of an assignment in the branch executed. Executing "if c then x := y else skip end" when c is true creates an explicit indirect flow from y to x. An implicit indirect flow is a flow from the test of a conditional to the left side of an assignment in the branch which is not executed. Executing "if c then x := y else skip end" when c is false creates an implicit indirect flow from y to x.

At any execution step, a variable or expression is said to carry variety [2, Sect.1] if its values is not completely constrained by the public inputs of the program. In other words, a variable or expression carries variety if its value is influenced by the private inputs; therefore, if it may have a different value at this given execution step if the values of the private inputs were different.

A "safe" execution is a noninterfering execution. In this article, as commonly done, noninterference is defined as the absence of strong dependencies between the secret inputs of an execution and the final values of some variables which are considered to be publicly observable at the end of the execution. For every execution of a given program P, two sets of variable identifiers are defined. The set of variables corresponding to the secret inputs of the program is designated by S(P). The set of variables whose final value are publicly observable at the end of the execution is designated by O(P). No requirements are put on S(P) and O(P) other than requiring them to be subsets of X (the domain of variables). A variable x is even allowed to belong to both sets. In such a case, in order to be noninterfering, the program P would be required to, at least, reset the value of x. In the following definitions, we consider that a program state may contain more than just a value store. This is the reason why a distinction is done between program states (X) and value stores (σ).

Definition 2.1 (V -Equivalent States).

Let V be a set of variables. Two program states X 1 , respectively X 2 , containing the value stores σ 1 , respectively σ 2 , are V -equivalent with regards to a set of variables V , written X 1 V = X 2 , if and only if the value of any variable belonging to V is the same in σ 1 and σ 2 :

X 1 V = X 2 ⇐⇒ ∀x ∈ V : σ 1 (x) = σ 2 (x)
Definition 2.1 states a formal relation among program states. This relation defines equivalence classes of program states with regard to a given set of variables. If two program states are V -equivalent, it means that it is impossible to distinguish them solely by looking at the value of the variables belonging to the set V . This relation is used to define the confidentiality property which is verified by the dynamic analysis presented in this paper.

Definition 2.2 (Noninterfering Execution).

Let ⇓ s denote a big-step semantics. Let S(P) be the complement of S(P) in the set X. For all programs P, program states X 1 and X 1 , an execution with the semantics ⇓ s of the program P in the initial state X 1 and yielding the final state X 1 is noninterfering, written ni(P, s, X 1 ), if and only if, for every program states X 2 and X 2 such that the execution with the semantics ⇓ s of the program P in the initial state X 2 yields the final state X 2 :

X 1 S(P) = X 2 ⇒ X 1 O(P) = X 2
Definition 2.2 states that an execution is safe -i.e. it has the desired confidentiality property -if any other execution started with the same public (non-secret) values yields a final program state which is O(P)-equivalent to the final program state of the execution analyzed. It means that, by looking only at the final values of the variables observable at the end of the execution, it is impossible to distinguish this execution from any other execution whose initial program state differs only in the values of the secret inputs. Therefore, for such an execution, it is impossible to deduce information about the secret inputs of the program by looking solely at the values of the publicly observable outputs.

The dynamic analysis is based on a flow and state sensitive static analysis. During the execution, every variable is associated a tag which reflects the fact that the variable may or may not carry variety -i.e. may or may not be influenced by the secret inputs of the program. A tag store in the program state keeps track of those associations. The dynamic analysis treats directly the direct and explicit indirect flows. For implicit indirect flows, a static analysis is run on the unexecuted branch of every conditional whose test carries variety.

The static analysis is context sensitive. An unexecuted branch P is analyzed in the context of the program state at the time the test of the conditional, to which P belongs, has been evaluated. The static analysis is then aware of the exact value of the variables which do not carry variety. During the analysis, the context (value store and tag store used for the analysis) is modified to reflect loss of knowledge (in fact, only the tag store is modified). The static analysis does not compute the values of variables. Therefore, when analyzing an assignment to a variable x, the context of the static analysis is modified to reflect the fact that the static analysis does not anymore have knowledge of the precise value of the variable x. When analyzing a conditional whose test value can be computed in the current context (using only the values of the variables whose tag is ⊥), only the branch designated by the test is analyzed. As the value of any variable which does not carry variety depends only on the public inputs, branches which are not designated by the test value would never be executed by any execution started with the same public inputs as the monitored execution. Implicit indirect flows and explicit indirect flows must be treated with the same precision in order to prevent the creation of a new covert channel [START_REF] Guernic | Monitoring Information Flow[END_REF]. This particular point is discussed in Sect. 4. As the static analysis detects implicit indirect flows more accurately than context insensitive analyses, explicit indirect flows can also be treated more accurately.

The next section formalizes the mechanisms presented above. It presents a monitoring semantics incorporating a dynamic noninterference analysis.

The Monitoring Semantics

The dynamic information flow analysis and the monitoring semantics are defined together in Fig. 2. Information flows are tracked using tags. At any execution step, every variable has a tag which reflects whether this variable may carry variety or not. The static analysis used for the analysis of some unexecuted branches is characterized in Fig. 3.

The language studied is an imperative language for sequential programs. Its syntax is given in Fig. 1. In this grammar, ident stands for a variable identifier. expr is an expression of values and variable identifiers. Expressions in this language are deterministic -their evaluation in a given program state always results in the same value -and are free of side effects -their evaluation has no influence on the program state.

A program expressed with this language is either a skip statement (skip) which has no effect, an assignment of the value of an expression to a variable, a sequence of programs ( prog ; prog ), a conditional executing one program -out of two -depending on the value of a given expression (if statements), or a loop executing repetitively a given program as long as a given expression is true (while statements).

A Semantics Making Use of Static Analysis Results

Let X be the domain of variable identifiers, D be the semantics domain of values, and T be the domain of tags. In the remainder of this article, T is equal to { , ⊥}. Those tags form a lattice such that ⊥ . is the tag associated to variables that may carry variety -i.e. whose value may be influenced by the secret inputs.

The monitoring semantics described in Fig. 2 is presented as standard inference rules for sequents written in the format:

ζ,

ρ(x)

The semantics rules make use of static analyses results. In Fig. 2, application of a static information flow analysis to the piece of code P in the context ζ is written: [[ζ P]] G . The analysis of a program P in a monitoring execution state ζ must return a subset of X. This set, usually written X, is an over-approximation of the set of variables which are potentially defined in an execution of P in the context ζ. This static information flow analysis can be any such analysis that satisfies a set of formal constraints which are stated in Sect. 3.2.

The monitoring semantics rules are straightforward. As can be expected, the execution of a skip statement with the semantics given in Fig. 2 yields a final state equal to the initial state. The monitored execution of the assignment of the value of the expression e to the variable x yields a monitored execution state (σ , ρ ). The final value store (σ ) is equal to the initial value store (σ) except for the variable x. The final value store maps the variable x to the value of the expression e evaluated with the initial value store (σ(e)).

Similarly, the final tag store (ρ ) is equal to the initial tag store (ρ) except for the variable x. The tag of x after the execution of the assignment is the least upper bound of the program counter tag (t pc ) and the tag of the expression computed using the initial tag store (ρ(e)). ρ(e) corresponds to the level of the information flowing into x through direct flows. t pc corresponds to the level of the information flowing into x through explicit indirect flows.

The monitored execution of a conditional whose test expression does not carry variety (ρ(e) = ⊥) follows the same scheme as with a standard semantics. For a conditional whose test expression e carries variety, the branch (P v ) designated by the value of e (v) is executed and the other one (P ¬v ) is analyzed. The final value store is the one returned by the execution of P v . The final tag store (ρ ) is the least upper bound of the tag store returned by the execution of P v and a new tag store (ρ e ) generated from the result of the analysis of P ¬v (X). By definition, ρ ρ is equal to λx.ρ(x) ρ (x). The new tag store (ρ e ) reflects the implicit indirect flows between the value of the test of the conditional and the variables (X) which may be defined in an execution of P ¬v . In ρ e , the tag of a variable x is equal to the initial tag of the test expression of the conditional (ρ(e)) if and only if x belongs to X; otherwise, its tag is ⊥.

The Static Analysis Used

Fig. 3 defines some constraints characterizing a set of static analyses which can be used by the dynamic noninterference analysis. The result X of a static analysis of a given program (P) in a given context (ζ) is acceptable for the dynamic analysis only if the result satisfies those rules. This is written in the format: X |= (ζ P). In the definitions of those rules, {[S true , S false ]} t v returns either the set S true , the set S false or the union of both depending on the tag t and the boolean v. Its formal definition follows.

{[S true , S false ]} t v = S true ∪ S false iff t = S v iff t = ⊥ ζ, t pc skip ⇓ M ζ (σ, ρ), t pc x := e ⇓ M (σ[x → σ(e)], ρ[x → ρ(e) t pc ]) ζ, t pc P h ⇓ M ζ h ζ h , t pc P t ⇓ M ζ ζ, t pc P h ; P t ⇓ M ζ ρ(e) = ⊥ σ(e) = v (σ, ρ), t pc ⊥ P v ⇓ M ζ (σ, ρ), t pc if e then P true else P false end ⇓ M ζ ρ(e) = σ(e) = v (σ, ρ), t pc P v ⇓ M (σ v , ρ v ) [[(σ, ρ) P ¬v ]] G = X ρ e = (X × { }) ∪ (X × {⊥}) (σ, ρ), t pc if e then P true else P false end ⇓ M (σ v , ρ v ρ e )
ρ(e) = ⊥ σ(e) = false (σ, ρ), t pc while e do P l done ⇓ M (σ, ρ)

ρ(e) = ⊥ σ(e) = true (σ, ρ), t pc ⊥ P l ; while e do P l done ⇓ M ζ (σ, ρ), t pc while e do P l done ⇓ M ζ ρ(e) = σ(e) = true (σ, ρ), t pc P l ; while e do P l done ⇓ M (σ , ρ e ) (σ, ρ), t pc while e do P l done ⇓ M (σ , ρ ρ e ) ρ(e) = σ(e) = false [[(σ, ρ) P l ; while e do P l done]] G = X ρ e = (X × { }) ∪ (X × {⊥}) (σ, ρ), t pc while e do P l done ⇓ M (σ, ρ ρ e ) Figure 2: Rules of the monitoring semantics

Properties of the Monitoring Semantics

Section 3 formally defines the dynamic information flow analysis proposed in this article. In the current section, this dynamic noninterference analysis is proved to be sound with regard to the enforcement of the notion of noninterfering execution given in Definition 2.2. This means that, any monitor enforcing

∅ |= ( (σ, ρ) skip ) {x} |= ( (σ, ρ) x := e )
X |= (σ, ρ) P h ; P t iff there exist X h and X t such that:

X h |= ((σ, ρ) P h ) let ρ = ρ ((X h × ) ∪ (X h × ⊥)) in X t |= ((σ, ρ ) P t ) X = X h ∪ X t X |= (σ, ρ
) if e then P true else P false end iff there exist X true and X false such that:

X true |= ((σ, ρ) P true ) X false |= ((σ, ρ) P false ) X = {[X true , X false ]} ρ(e) σ (e)
X |= (σ, ρ) while e do P l done iff there exists X l such that:

let ρ = ρ ((X l × ) ∪ (X l × ⊥)) in X l |= ((σ, ρ ) P l ) X = {[X l , ∅]} ρ(e) σ(e)
Figure 3: Constraints on the static analysis results noninterference using this dynamic analysis would be able to ensure that: for any two monitored executions of a given program P started with the same public inputs (variables which do not belong to S(P)), the final values of observable outputs (variables which belong to O(P)) are the same for both executions. Theorem 4.1 proves that the dynamic analysis is sound with regard to information flow detection. Any variable, whose tag at the end of the execution is ⊥, has the same final value for any executions started with the same public inputs.

Theorem 4.1 (Detection Soundness).

For all programs P, monitoring execution states (σ 1 , ρ 1 ), (σ 1 , ρ 1 ), (σ 2 , ρ 2 ) and (σ 2 , ρ 2 ) such that:

• (σ 1 , ρ 1 ), ⊥ P ⇓ M (σ 1 , ρ 1 ) , • (σ 2 , ρ 2 ), ⊥ P ⇓ M (σ 2 , ρ 2 ) , • ∀x / ∈ S(P). σ 1 (x) = σ 2 (x),
• ∀x ∈ S(P). ρ 1 (x) = the following holds:

∀x. (ρ 1 (x) = ⊥) ⇒ (σ 1 (x) = σ 2 (x))
Proof summary. The detailed formal proof can be found in the appendices (Lemma A.6). This proof goes by induction on the derivation tree of " (σ 1 , ρ 1 ), ⊥ P ⇓ M (σ 1 , ρ 1 ) " and by cases on the last evaluation rule used. The proof aims at showing that the invariant which relates the fact, for every variable, of having a ⊥ tag and not carrying variety -i.e. not being influenced by the secret inputs -is preserved during the execution. The invariant preservation is obvious for skip statements. If the tag of a variable x after an assignment of e to x is ⊥, then it means, first, that the control flow does not carry variety (t pc = ⊥) and therefore that the assignment will always be executed with similar public inputs. It also means that the tag of every variable appearing in e is ⊥, therefore the expression does not carry variety and the invariant property is preserved by the execution of assignments. For sequence statements, if the invariant is preserved by the first and second statements then it is preserved by the sequential execution of both statements.

For branching statements (if statements), things get a little bit more complex. If the tag of the condition of the branching statement is ⊥, then the condition does not carry variety and any execution started with the same public inputs evaluates the same branch as the execution monitored. As, by induction, the execution of the branch preserves the invariant, the invariant is also preserved by the execution of a branching statement whose condition's tag is ⊥. If the condition's tag is , then all the executions started with the same public inputs do not evaluate the same branch. However, as the tag of the control flow (t pc ) is updated to for the evaluation of the designated branch, all the variables assigned to in the branch have a tag of after the execution of the branching statement (follows from the rule for assignments and is detailed in Lemma A.5 in the appendices). Additionally, any variable which may have been assigned to by the execution of the other branch are in the set returned by the static analysis (follows from the rules in Fig. 3 and is detailed in Lemma A.1 in the appendices), therefore, at the end of the evaluation of the branching statement, their tag is also . Hence, the invariant relating ⊥ and not carrying variety is preserved by the execution of a branching statement whose condition carries variety.

For loops (while statements), the proof goes by cases, first, on the tag of the condition and then on its value. If the condition of the loop does not carry variety (its tag is ⊥) then, if its value is false the loop is equivalent to a skip and the invariant is preserved. If the condition does not carry variety (its tag is ⊥) and is true, the proof of preservation of the invariant follows by induction from the sub-derivation tree corresponding to the evaluation of the body of the loop at least once. If the condition carries variety (its tag is ), then all the executions started with the same public inputs do not execute the body of the loop the same number of times. However, for the same reasons as the case for branching statements (t pc = and the static analysis of the body of the loop returns all the variables which may be assigned by an evaluation of the loop), the tag of all the variables whose value may be modified by the loop is after the evaluation of the loop. Therefore, the invariant property is also preserved by loops whose condition carries variety.

Variables whose final tags are not ⊥ may have different final values for two executions started with the same public inputs. Therefore, a monitor enforcing noninterference must reset to a default value any variable belonging to O(P) whose final tag is not ⊥. However, as shown by Le Guernic and Jensen [START_REF] Guernic | Monitoring Information Flow[END_REF], if the correction of "bad" information flows is done without enough care, the correction mechanism itself can become a new covert channel carrying secret information. Theorem 4.2 proves that the final tag of a variable does not depend on the secret inputs of the program. Therefore, any variable belonging to O(P) whose final tag is not ⊥ can safely be reset to a default value without creating a new covert channel.

Theorem 4.2 (Correction Soundness).

For all programs P, monitoring execution states (σ 1 , ρ 1 ), (σ 1 , ρ 1 ), (σ 2 , ρ 2 ) and (σ 2 , ρ 2 ) such that:

• (σ 1 , ρ 1 ), ⊥ P ⇓ M (σ 1 , ρ 1 ) , • (σ 2 , ρ 2 ), ⊥ P ⇓ M (σ 2 , ρ 2 ) ,
• ∀x / ∈ S(P). σ 1 (x) = σ 2 (x),

• ∀x ∈ S(P). ρ 1 (x) =

• ρ 1 = ρ 2 the following holds:

ρ 1 = ρ 2 .
Proof summary. The detailed formal proof can be found in the appendices (Lemma A.8). This proof goes by induction on the derivation tree of " (σ 1 , ρ 1 ), ⊥ P ⇓ M (σ 1 , ρ 1 ) " and by cases on the last evaluation rule used. In order to be able to use induction, Lemma A.8 proves a generalization of the theorem stated above with two differences in its statement. The first one concerns the tag of the program counter (t pc ) which is not constrained to be ⊥, but must be the same for the two executions compared. The second difference is the substitution of the 2 hypotheses concerning S(P) by a single hypothesis stating that the variables containing data which is considered non secret (ρ 1 (x) = ⊥) must have the same value in both executions (σ

1 (x) = σ 2 (x)).
The case for skip is direct. For assignments, the only tag modified is the one of the variable assigned. It is set to ρ(e) t pc . As the two tag stores are initially equal, ρ 1 (e) is equal to ρ 2 (e). As explained above, the proof is for a generalization of the theorem where t pc1 is equal to t pc2 . Therefore, both tag stores (ρ 1 and ρ 2 ) are equal after the execution of the assignment. For the sequential execution of S 1 ; S 2 , the inductive hypothesis implies that both tag stores are equal before the execution of S 2 and the generalization of Theorem 4.1 (Lemma A.6) implies that the hypothesis ρ 1 (x) = ⊥ ⇒ ρ 1 (e) = ρ 2 (e) also holds before the execution of S 2 . Therefore the inductive hypothesis can be applied and implies that both tag stores are equal after the execution of the sequential statement.

For if statements, if the tag of the condition is ⊥ then the condition evaluates to the same value for both executions. Therefore, the same branch is executed and the inductive hypothesis implies that both tag stores are equal at the end of the execution of the branching statement. If the tag of the condition is but both executions evaluate the same branch, then for similar reasons both tag stores are equal at the end of the execution of the branching statement. If two different branches are executed then the tag of the program counter is . Therefore, as exposed in the proof of Theorem 4.1 and detailed in Lemma A.5, the tag of every assigned variable is (as long as the execution of the branch is not over new tags are always ). Additionally, during the execution of this branch, for every branching statement whose condition's tag is the unexecuted branch is analyzed and the tag of every variable which may have been assigned to by an execution of this branch is set to . Fig. 3 constrains the analysis to make the same choices with regard to which subbranches to ignore and which ones to analyze. Therefore, the set of variables returned by the analysis of the unexecuted branch is exactly the set of variables whose tag would have been set to by an execution of this branch (this particular point is detailed in Lemma A.3). Therefore, whatever branch is executed or analyzed, the same set of variables have their tag set to . Hence, the final tag stores are equal after the execution of the if statement.

For while statements, if the condition evaluates to the same value for both executions then the inductive hypothesis implies that the tag stores at the end of both executions are equal. If the condition evaluates to two different values then it means that its tag is . Therefore the final tag store is the least upper bound of the initial tag store (equal for both executions) and a new tag store ρ e . This new tag store is either the tag store returned by the execution of the while statement (executing the body at least once) with program counter tag (t pc ) equal to or the analysis of the same statement. As exposed in the case of if statements (and detailed in Lemma A.3), in both cases the tags of the exact same set of variables are set to and they are the only tag modified. Hence, the final tag stores are equal after the execution of the while statement.

Related Work

The vast majority of research on noninterference concerns static analyses and involves type systems [START_REF] Pottier | Information flow inference for free[END_REF][START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Some "real size" languages together with security type system have been developed (for example, JFlow/JIF [START_REF] Myers | JFlow: Practical mostly-static information flow control[END_REF] and Flow-Caml [START_REF] Pottier | Information flow inference for ML[END_REF]). Dynamic information flow analyses [1,[START_REF] Fenton | Memoryless subsystems[END_REF][START_REF] Weissman | Security controls in the adept-50 timesharing system[END_REF][START_REF] Woodward | Exploiting the dual nature of sensitivity labels[END_REF] are not as popular as static analyses for information flow, but there has been interesting research. For example, RIFLE [START_REF] Vachharajani | Rifle: An architectural framework for user-centric information-flow security[END_REF] is a complete run-time information flow security system based on an architectural framework and a binary translator. Masri et al. [START_REF] Masri | Detecting and debugging insecure information flows[END_REF] present a dynamic information flow analysis for structured or unstructured languages. Venkatakrishnan et al. [START_REF] Venkatakrishnan | Provably correct runtime enforcement of non-interference properties[END_REF] propose a program transformation for a simple deterministic procedural language that ensures a sound detection of information flows. However, none of those three later works prove that the correction mechanisms of "bad" flows proposed do not create a new covert channel that can reveal secret information -see, e.g., [START_REF] Guernic | Monitoring Information Flow[END_REF]. In fact, those correction mechanisms do create a new covert channel. Theorem 4.2 proves that a correction mechanism of "bad" flows can be based on the dynamic analysis proposed in this paper as the results of the dynamic analysis are the same for every executions started with the same public inputs. More recently, Shroff, Smith, and Thober [START_REF] Shroff | Dynamic dependency monitoring to secure information flow[END_REF] proposed a dynamic information flow analysis which tracks direct flows and collects indirect flows dynamically. The information collected about indirect flows is transferred from one execution to another using a cache mechanism. After an undetermined number of executions, the analysis will know about all indirect flows in the program and thus will then be sound with regard to the detection of all information flows. This information about indirect flows can be precomputed using a static analysis at the cost of a decrease of precision. Using this approach they are able to handle a language including alias and method calls.

Contrary to common assumption, none of the related works on dynamic information flow analysis known to the author take enough context information into account to detect that the program on page 2 is noninterfering when using it to communicate with users other than sexyPirate. For example, the transformation of Venkatakrishnan et al. [START_REF] Venkatakrishnan | Provably correct runtime enforcement of non-interference properties[END_REF] updates the security label of c with the security label of the condition on line 3 before executing line 7. Therefore, at line 7, c is always considered as secret even if the user is not communicating with sexyPirate. When executing the assignment of line 5, the program counter of Shroff et al.'s work [START_REF] Shroff | Dynamic dependency monitoring to secure information flow[END_REF] contains a reference to the program point of line 3 and therefore is added to the set of source of implicit flows to c. Consequently, any complete implicit dependency cache contains a reference to the implicit flow from line 3 to line 7. As the test of line 3 is always executed, Shroff et al.'s work always considers line 7 as displaying secret information. The dynamic analysis proposed in this paper is able to detect the noninterfering behavior of the program on page 2 when communicating with someone other than sexyPirate.

Conclusion

This article addresses the problem of information flow verification and correction at run time in order to enforce the confidentiality of secret data. The confidentiality property to monitor is expressed using the property of noninterference between secret inputs of the execution and its public outputs. The language taken into consideration is a sequential language with assignments and conditionals (including loops). The main difference between the monitoring mechanism proposed in this article and the ones of related works lies in the static analysis used to detect implicit indirect flows. The static information flow analyses used by the dynamic analysis proposed in this article are sensitive to the current program state. This allows to increase the precision of the overall dynamic information flow analysis for the detection of implicit and explicit indirect flows. In Sect. 4, the proposed noninterference monitor is proved to be sound both with regard to the detection of information flows and with regard to their correction when necessary.

Benefits of monitoring compared to static analyses. Monitoring an execution has a cost. So, what are the main benefits of noninterference monitoring compared to static analyses? The first concerns the possibility that a monitoring mechanism can be used to change the security policy for each execution. In the majority of cases, running a static analysis before every execution would be more costly than using a monitor. The second reason is that noninterference is a rather strong property. Many programs are rejected by static analyses of noninterference. In such cases it is still possible to use a monitoring mechanism with the possibility that some executions will be altered by the monitoring mechanism. However behavior alteration is an intrinsic feature of any monitoring mechanism. Monitoring noninterference ensures confidentiality while still allowing testing with regard to other specifications using unmonitored executions as perfect oracle -at least as perfect as the original program.

There are two main reasons why it is interesting to use a noninterference monitor on a program rejected by a static analysis. The first one is that a monitoring mechanism may be more precise than static analyses because during execution the monitoring mechanism gets some accurate information about the "path behavior" of the program. As an example, let us consider the following program where h is the only secret input and l the only other input (a public one). 1 i f ( t e s t 1 ( l ) ) then tmp := h e l s e s k i p end; 2 i f ( t e s t 2 ( l ) ) then x := tmp e l s e s k i p end; 3 output x Without information on test1 and test2 (and often, even with), a static analysis would conclude that this program is unsafe because the secret input information could be carried to x through tmp and then to the output. However, if test1 and test2 are such that no value of l makes both predicates true, then any execution of the program is perfectly safe. In that case, the monitoring mechanism would allow any execution of this program. The reason is that, l being a public input, only executions following the same path as the current execution are taken care of by the monitoring mechanism. So, for such configurations where the branching conditions are not influenced by the secret inputs, a monitoring mechanism is at least as precise as any static analysis -and often more precise.

The second reason lies in the granularity of the noninterference property. Static analyses have to take into consideration all possible executions of the program analyzed. This implies that if a single execution is unsafe then the program (thus all its executions) is rejected. Whereas, even if some executions of a program are unsafe, a monitor still allows this program to be used. The unsafe executions, which are not useful, are altered to enforce confidentiality while the safe executions are still usable. For example, the program on page 2 being interfering, any static noninterfering analysis rejects this program. Therefore, users would be advised not to use this program at all. However, using a noninterference monitor, it is possible to safely use this program. When communicating with any user other than sexyPirate, monitored executions of this program have their normal behavior. When communicating with sexyPirate, monitored executions are safely detected as potentially interfering and can therefore be corrected to prevent any secret leakage. Of course, when attempting to communicate with sexyPirate, executions of this program are altered and it is therefore not possible to communicate with sexyPirate. However, this is the desired behavior of a noninterference monitor when confidentiality is more important than the service provided by the program. For all monitoring execution states (σ, ρ), (σ i , ρ i ) and (σ o , ρ o ), program counter tags t pc , programs P, and analysis results X such that:

A Appendix: Proofs

A.1 Static Analysis Properties

1. ∀x : (ρ(x) = ⊥) ⇒ σ i (x) = σ(x), 2. (σ i , ρ i ), t pc P ⇓ M (σ o , ρ o ) ,
the following holds:

[[(σ, ρ) P]] G = X ⇒ ∀x / ∈ X. σ o (x) = σ i (x)
Proof. This lemma is obvious once we are convinced that the result of the static analysis contains all the variables whose value may be modified by any execution of the analyzed program in the context of the analysis (i.e. for any initial state where the value of the variables whose tag is ⊥ in ρ have the same value has the one in σ). Going by induction on the structure of the analyzed program, it is obvious for skip statements and assignments. When analyzing the second part of a sequence "P 1 ; P 2 ", the tags of the variables which may have been modified by the execution of P 1 are set to to reflect the fact that the analysis does not know anymore the exact value of those variables at the beginning of P 2 . Therefore, it is easy to prove by induction that the property holds for sequences. The result of the analysis of an if-statement is the result of the analysis of the branch designated by the condition if and only if the tag of this condition is ⊥ (i.e. any initial state compatible with the context of execution evaluates the condition to the same value as the analysis); otherwise, it is the union of the analysis of both branches. Once again, a simple induction on the structure of the analyzed program proves the desired property for if-statements. For whilestatements, the result of the analysis is empty if and only if the analysis is able to determine that, any execution started in an initial state compatible with the context of the analysis do not execute the body of the loop. Otherwise, the result of the analysis of the while-statement relies on fix point computation.

It corresponds to the result of the analysis of the body of the loop considering that the value of any variable whose value may be modified by an execution of the body of the loop is unknown at the beginning of the analysis (Thus taking into account any number of execution of the body of the loop). Therefore, an induction on the structure of the while-statements using the properties of fix points allow to prove the property for while-statements.

Lemma A.2 (Static analysis is deterministic with regard to public data).

For all monitoring execution states (σ, ρ) and (σ , ρ ), and programs P such that:

1. ρ = ρ , 2. ∀x : (ρ(x) ⊥) ⇒ σ(x) = σ (x),
the following holds:

[[(σ, ρ) P]] G = [[(σ , ρ ) P]] G
Proof. As the constraints stated in Fig. 3 use only the precise value of variables whose tag is ⊥ and never reset a tag to ⊥ for included constraints, this lemma is direct for any deterministic analysis satisfying the constraints of Fig. 3.

Lemma A.3 (Correctness of the static analysis for information flow correction).

For all monitoring execution states (σ, ρ) and (σ , ρ ), programs P, and analysis results X such that:

1. (σ, ρ), P ⇓ M (σ , ρ ) , 2. [[(σ, ρ) P]] G = X,
the following holds:

ρ = ρ (X × { }) ∪ (X × {⊥})
Proof. This lemma is proved by induction on the structure of P. It is obvious for skip statements and assignments. For a sequence "P 1 ; P 2 ", the induction on P 1 give that the tag store used for the evaluation of P 2 is the same as the one used for the analysis of P 2 . And lemmas A.1 and A.2 give that the value store used for the evaluation of P 2 is equivalent to the initial value store from the point of view of the analysis. Therefore, two simple inductions prove the lemma for sequences. For if-statements, if the tag of the condition is ⊥ then the tag store after evaluation is the tag store after evaluation of the branch designated by the condition and the result of the analysis is the result of the analysis of the branch designated by the condition. Therefore, a simple induction proves the lemma whenever the tag of the condition is ⊥. If the tag of the condition is then the tag store after evaluation is the least upper bound of the tag store after the evaluation of the branch designated by the condition and a tag store equal to (X v × { }) ∪ (X v × {⊥}) with X v the result of the analysis of the unexecuted branch. The result of the analysis is the union of the result of the analysis of both branches. Therefore, a simple induction on the branch executed proves the lemma whenever the tag of the condition is . The evaluation of a whilestatement always ends up evaluating this while-statement with the condition being false (at the end of the execution of the while-statement). Therefore, at the end of the evaluation, the tag of all the variables appearing in the result of the analysis of the while-statement are set to . For the same reasons as with sequences (lemmas A.1 and A.2) with the addition of the fix point property, the value stores and tag stores at the beginning of the evaluation and at the end of the evaluation of the loop are equivalent from the point of view of the analysis. The analysis of the while-statement returns the same result as the static analysis run by the evaluation and the lemma holds for every variable appearing in the result of the static analysis. All the other variables can not be assigned to by the evaluation of the while-statement (cause of lemma A.1 which can be extracted from it by observing that the analysis does not compare the value assigned to a variable from its value before the analysis). Therefore, at the end of the evaluation , they have the same tag than at the beginning and the lemma also holds for those variables.

A.2 Detection Soundness

Lemma A.4 (Public expressions are stable). For all tag stores ρ, value stores σ 1 and σ 2 , and expression e such that for all variable x the following holds

(ρ(x) = ⊥) ⇒ σ 1 (x) = σ 2 (x), if ρ(e) = ⊥ then σ 1 (e) = σ 2 (e).
Proof. The proof is straightforward. It follows directly from the facts that expression evaluation is deterministic, the tag of an expression is the least upper bound of the tags of its free variables and that public (⊥) variables have the same value in σ 1 and σ 2 .

Lemma A.5 (Tag of assigned variables contains t pc ). For all value stores σ i , tag stores ρ i , and statement S such that:

• (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o )
it is true that:

• ∀x : t pc ρ o (x) ⇒ (σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x))
Proof. The proof goes by induction on the derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ". Assume the lemma holds for any sub-derivation tree, if the last rule used is:

(E M -IF ⊥ ) then we can conclude that :

(1) S is "if e then S true else S f alse end" and " (σ i , ρ i ),

t pc ⊥ S v ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ".

It follows directly from the definition of the rule (E

M -IF ⊥ ). (•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
This is obtained by a simple induction because t pc ⊥ = t pc .

(E M -IF ) then we can conclude that :

(1) S is "if e then S 1 else S 2 end" and there exist S v and ρ v such that:

• " (σ i , ρ i ), t pc S v ⇓ M (σ o , ρ v ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • ∀x : ρ v (x) ρ o (x)
It follows directly from the definition of the rule (E M -IF ).

(2) ∀x :

t pc ρ v (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ v (x)
. It follows directly from the inductive hypothesis and the local conclusion (1).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
As t pc ρ o (x) implies t pc ρ v (x) (from the local conclusion (1)), the above result follows directly from the local conclusions ( 1) and [START_REF] Cohen | Information transmission in computational systems[END_REF].

(E M -WHILE skip ) then we can conclude that :

(1) S is "while e do S 1 done" and

σ o = σ i ∧ ρ i = ρ o .
It follows directly from the definition of the rule (E M -WHILE skip ).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
It follows directly from the local conclusion (1).

(E M -WHILE true ⊥ ) then we can conclude that :

(1) S is "while e do S 1 done" and there exist S , t e and ρ such that:

• " (σ i , ρ i ), t pc ⊥ S ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E M -WHILE true ⊥ ).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
It follows directly from the inductive hypothesis and the local conclusion (1).

(E M -WHILE true ) then we can conclude that :

(1) S is "while e do S 1 done" and there exist S and ρ such that:

• " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • ∀x : ρ (x) ρ o (x)
It follows directly from the definition of the rule (E M -WHILE true ).

(2) ∀x :

t pc ρ (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ (x)
. It follows directly from the inductive hypothesis and the local conclusion (1).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
As t pc ρ o (x) and ρ (x) ρ o (x) imply t pc t e ρ (x), the above result follows from the local conclusions (1) and [START_REF] Cohen | Information transmission in computational systems[END_REF].

(E M -WHILE false ) then we can conclude that :

(1) S is "while e do S 1 done", σ o = σ i and ∀x : ρ i (x) ρ o (x).

It follows directly from the definition of the rule (E M -WHILE false ).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
It follows directly from the local conclusion (1).

(E M -SEQUENCE) then we can conclude that :

(1) S is "S 1 ; S 2 " and there exist σ 1 and ρ 1 such that:

• " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E M -SEQUENCE).

(2) ∀x :

t pc ρ 1 (x) ⇒ σ 1 (x) = σ i (x) ∧ ρ i (x) ρ 1 (x) and ∀x : t pc ρ o (x) ⇒ σ o (x) = σ 1 (x) ∧ ρ 1 (x) ρ o (x).
It follows directly from the inductive hypothesis and the local conclusion (1).

(•) ∀x : t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
From the local conclusion (1), if t pc ρ o (x) then ρ 1 (x) ρ o (x). Hence, t pc ρ 1 (x). Then, combining the results of the local conclusion ( 2

), "σ o (x) = σ 1 (x) = σ i (x) ∧ ρ i (x) ρ 1 (x) ρ o (x)"
(E M -ASSIGN) then we can conclude that : (•) ∀x :

t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
From (1), if x = id then t pc ρ o (x). Otherwise, x = id and

σ o (x) = σ i (x) ∧ ρ i (x) = ρ o (x)
(E M -SKIP) then we can conclude that :

(1) S is "skip" and

σ o = σ i ∧ ρ i = ρ o .
It follows directly from the definition of the rule (E M -SKIP).

(•) ∀x :

t pc ρ o (x) ⇒ σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).

It follows directly from the local conclusion (1).

Lemma A.6 (Correctness for information flow detection with semantics ⇓ M ).

For all:

• variable x,

• value stores σ i , σ o , σ i , and σ o ,

• tag stores ρ i , ρ o , ρ i , and ρ o ,

• tags t pc and t pc ,

• and statement S such that:

1 ∀y : (ρ i (y) = ⊥) ⇒ σ i (y) = σ i (y), 2 (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) , 3 (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) , 4 ρ o (x) = ⊥
it is true that:

• σ o (x) = σ o (x).
Proof. The proof goes by induction on the derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ". Assume the lemma holds for any sub-derivation tree, if the last rule used is:

(E -IF ⊥ ) then we can conclude that :

(1) S is "if e then S true else S f alse end" and there exists v ∈ {true, f alse} such that:

• σ i (e) = v and ρ i (e) = ⊥ • " (σ i , ρ i ), t pc ⊥ S v ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E -IF ⊥ ).

(2) There exist a value v , a tag t , and a tag store ρ such that:

• σ i (e) = v and ρ i (e) = t • " (σ i , ρ i ), t pc t S v ⇓ M (σ o , ρ ) "
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "if e then S true else S f alse end" ((E -IF ⊥ ) and (E -IF )).

(

) v = v . 3
This result comes from lemma A.4, the global hypothesis 1 and local conclusions ( 1) and ( 2).

(•) σ o (x) = σ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ i , ρ i ),

t pc ⊥ S v ⇓ M (σ o , ρ o ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc t S v ⇓ M (σ o , ρ ) " (because v = v ).
(E -IF ) then we can conclude that :

(1) S is "if e then S true else S f alse end" and there exist v ∈ {true, f alse}, two tag store ρ v and ρ e , and an analysis result X such that:

• " (σ i , ρ i ), t pc S v ⇓ M (σ o , ρ v ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • [[σ i ; ρ i S ¬v ]] G = X • ρ v (x) ρ o (x) • ρ e = (X × { }) ∪ (X × {⊥}) • ρ e (x) ρ o (x)
It follows directly from the definition of the rule (E -IF ⊥ ).

(2) There exist a value v ∈ {true, f alse}, a tag store ρ v , and a tag t e such that:

• " (σ i , ρ i ), t pc t e S v ⇓ M (σ o , ρ v ) "
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "if e then S true else S f alse end"

((E -IF ⊥ ) and (E -IF )). Case 1: v = v (a) ρ v (x) = ⊥.
It follows from the local conclusion (1) and the global hypothesis

4 . (•) σ o (x) = σ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ i , ρ i ), t pc S v ⇓ M (σ o , ρ v ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc t e S v ⇓ M (σ o , ρ v ) ". It is possible to apply the inductive hypothesis because of the local conclusion (a) and the fact that, by the case hypothesis, v = v ).

Case 2: v = v (which implies that v = ¬v) (a) σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x).
From the global hypothesis 4 , ρ o (x) = ⊥. Hence, from lemma A.5 applied to " (σ i , ρ i ),

t pc S v ⇓ M (σ o , ρ v ) ", σ o (x) = σ i (x) ∧ ρ i (x) ρ o (x). (b) σ o (x) = σ i (x).
From the local conclusion (1), the global hypothesis 4 , and the definition of ρ e in the local conclusion (1), x ∈ X. Hence, from the local conclusion (1) and the lemma A.1 applied to "

(σ i , ρ i ), t pc t e S v ⇓ M (σ o , ρ v ) ", σ o (x) = σ i (x). (c) σ i (x) = σ i (x).
From the local conclusion (a) and the global hypothesis 4 , we get that ρ i (x) = ⊥. Hence, from the global hypothesis 1 , we get that

σ i (x) = σ i (x). (•) σ o (x) = σ o (x).
It follows directly from the local conclusions (a), (b), and (c).

(E -WHILE skip ) then we can conclude that :

(1) S is "while e do S 1 done" and:

• σ i (e) = false and ρ i (e) = ⊥ • σ i = σ o and ρ i = ρ o
It follows directly from the definition of the rule (E -IF ⊥ ).

(2) There exist a value v and a tag t such that:

• σ i (e) = v and ρ i (e) = t
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

(

) σ i = σ o . 3
From lemma A.4, the global hypothesis 1 and the local conclusions (1) and ( 2), we get v = f alse. Hence, from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" whenever e is false ((E -WHILE skip ) and (E -WHILE false )),

σ i = σ o . (4) σ i (x) = σ i (x).
From the local conclusion (1) and the global hypothesis 4 , we get that ρ i (x) = ⊥. Hence, from the global hypothesis 1 , we get that

σ i (x) = σ i (x). (•) σ o (x) = σ o (x).
It follows directly from the local conclusions (1), (3), and (4).

(E -WHILE true ⊥ ) then we can conclude that :

(1) S is "while e do S 1 done" and:

• σ i (e) = true and ρ i (e) = ⊥ • " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E -WHILE true ⊥ ).

(2) There exist a value v and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

(3) v = true. It follows directly from the local conclusions (1) and (2), lemma A.4 and global hypothesis 1 .

(4) There exists a tag store ρ l such that:

• " (σ i , ρ i ), t pc t e S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) "

It follows from the global hypothesis 5 , the local conclusions (1), ( 2) and ( 3), and the definitions of the rules applying to "while e do S 1 done" whenever e is true ((E -WHILE true ⊥ ) and (E -WHILE true )).

(•) σ o (x) = σ o (x).
By applying the inductive hypothesis on the derivations " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) " and " (σ i , ρ i ), t pc t e S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) ", it is possible to deduce that σ o (x) = σ o (x).

(E -WHILE true ) then we conclude that :

(1) S is "while e do S 1 done" and there exist a tag t e and a tag store ρ l such that:

• σ i (e) = true and ρ i (e) = • " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • ρ l ρ o
It follows directly from the definition of the rule (E -WHILE true ).

(2) ρ l (x) = ⊥.

It follows from the local conclusion (1) and the global hypothesis 4 .

(3) There exist a value v and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

Case 1: v = true (a) There exists a tag store ρ l such that:

• " (σ i , ρ i ), t pc t e S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " It follows from the global hypothesis 5 , the local conclusions (1) and (3), the case hypothesis, and the definitions of the rules applying to "while e do S 1 done" whenever e is true ((E -WHILE true ⊥ ) and (E -WHILE true )).

(•) σ o (x) = σ o (x).
By applying the inductive hypothesis on the derivations " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " and " (σ i , ρ i ), t pc t e S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) ", it is possible to deduce, using the local conclusion [START_REF] Cohen | Information transmission in computational systems[END_REF], that σ o (x) = σ o (x).

Case 2: v = false (a) σ o (x) = σ i (x).
It follows directly from the local conclusions (1), the fact that "t pc ρ l (x)" (from the local conclusion (2)), and the lemma A.5 applied to " (σ i , ρ i ), t pc S 1 ; while e do S 1 done

⇓ M (σ o , ρ l ) ". (b) σ o (x) = σ i (x).
From the global hypothesis 5 , the local conclusions ( 1) and ( 3), the case hypothesis, and the definitions of the rules applying to "while e do S 1 done" whenever is false ((E -WHILE skip ) and (E -WHILE false )),

σ i = σ o . (c) σ i (x) = σ i (x).
From the local conclusion (2) and lemma A.5 applied to " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) ", ρ i (x) = ⊥. Hence, from the global hypothesis 1 , we get that

σ i (x) = σ i (x). (•) σ o (x) = σ o (x).
It follows directly from the local conclusions (a), (b), and (c).

(E -WHILE false ) then we can conclude that :

(1) S is "while e do S 1 done" and there exist two tag stores ρ 1 and ρ e such that:

• σ i (e) = false and ρ i (e) = • [[σ i ; ρ i S 1 ; while e do S 1 done]] G = X • σ o = σ i • ρ e = (X × { }) ∪ (X × {⊥}) • ρ e (x) ρ o (x) and ρ i (x) ρ o (x)
It follows directly from the definition of the rule (E -WHILE true ).

(2) There exist a value v ∈ {true, false} and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ) and (E -WHILE false )).

(

) σ i (x) = σ i (x). 3
From the local conclusion (1) (ρ i (x) ρ o (x)) and the global hypothesis 4 , ρ i (x) = ⊥. Hence, from the global hypothesis 1 , we get that σ i (x) = σ i (x). 2), the case hypothesis, and the definition of the rule applying to "while e do S 1 done" whenever e evaluates to true. (b) x ∈ X.

From the local conclusion (1) (ρ e (x) ρ o (x)) and the global hypothesis 4 , we get that ρ e (x) = ⊥. Hence, from the definition of ρ e given in the local conclusion (1), x ∈ X.

(c) σ o (x) = σ i (x).
From the local conclusion (b), the lemma A.1 applied to the analysis from the local conclusion (1) and the derivation from the local conclusion (a),

σ o (x) = σ i (x). (•) σ o (x) = σ o (x).
It follows directly from the local conclusions (1), (

(E -SEQUENCE) then we can conclude that :

(1) S is "S 1 ; S 2 " and there exist σ 1 and ρ 1 such that:

• " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " is a sub-derivation tree of " (σ i , ρ i ),

t pc S ⇓ M (σ o , ρ o ) " • " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E M -SEQUENCE).

(2) There exist σ 1 and ρ 1 such that:

• " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " • " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) "
It follows directly from the global hypothesis 5 , the local conclusion (1), and the definition of the only rule applying to "S 1 ; S 2 " ((E M -SEQUENCE)).

(

) ∀y : (ρ 1 (y) = ⊥) ⇒ σ 1 (y) = σ 1 (y). 3
This result is obtained by applying the inductive hypothesis on " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " for any variable y such that ρ 1 (y) = ⊥.

(•) σ o (x) = σ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " using the local conclusion [START_REF] Fenton | Memoryless subsystems[END_REF].

(E -ASSIGN) then we can conclude that :

(1) S is "id := e". (E -SKIP) then we can conclude that :

(1) S is "skip", σ o = σ i and ρ o = ρ i . It follows directly from the definition of the rule (E -SKIP). (2) σ o = σ i .

It follows directly from the global hypothesis 5 , the local conclusion (1), and the definition of the only rule applying to "skip" ((E -SKIP)).

(1) S is "if e then S true else S f alse end" and there exists v ∈ {true, f alse} such that:

• σ i (e) = v and ρ i (e) = ⊥ • " (σ i , ρ i ), t pc ⊥ S v ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E -IF ⊥ ).

(2) There exist a value v and a tag t such that:

• σ i (e) = v and ρ i (e) = t
It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "if e then S true else S f alse end" ((E -IF ⊥ ) and (E -IF )).

(3) t = ⊥ and v = v . It follows directly from the local conclusion ( 1) and ( 2), lemmas A.7 and A.4 and the global hypotheses 1 and 2 .

(4) " (σ i , ρ i ), t pc ⊥ S v ⇓ M (σ o , ρ o ) " It follows from the global hypothesis 5 , the local conclusions (1), [START_REF] Cohen | Information transmission in computational systems[END_REF], and (3), and the definition of the rule applying to "if e then S true else S f alse end" whenever the tag of e is ⊥ ((E -IF ⊥ )).

(•) ρ o (x) = ρ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ i , ρ i ),

t pc ⊥ S v ⇓ M (σ o , ρ o ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc ⊥ S v ⇓ M (σ o , ρ o ) ".
(E -IF ) then we can conclude that :

(1) S is "if e then S true else S f alse end" and there exist v ∈ {true, f alse}, two tag stores ρ v and ρ e , and an analysis result X such that:

• σ i (e) = v and ρ i (e) = • " (σ i , ρ i ), t pc S v ⇓ M (σ o , ρ v ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • [[(σ i , ρ i ) S ¬v ]] G = X • ρ e = (X × { }) ∪ (X × {⊥}) • ρ o = ρ v ρ e

It follows directly from the definition of the rule (E -IF ).

(2) There exist a value v ∈ {true, f alse} and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "if e then S true else S f alse end" ((E -IF ⊥ ) and (E -IF )).

(3) t e = .

It follows directly from the local conclusions ( 1) and ( 2), the lemma A.7 and the global hypothesis 2 .

(4) There exists an analysis result X and two tag stores ρ v and ρ e such that:

•

" (σ i , ρ i ), t pc t e S v ⇓ M (σ o , ρ v ) " • [[(σ i , ρ i ) S ¬v ]] G = X • ρ e = (X × { }) ∪ (X × {⊥}) • ρ o = ρ v ρ e
It follows from the global hypothesis 5 , the local conclusions (1), (2), and (3), and the definition of the rule applying to "if e then S true else S f alse end" whenever the tag of e is ((E -IF )).

Case 1: v = v (a) ρ e (x) = ρ e (x).
It follows from the definitions of ρ e and ρ e (given in the local conclusions ( 1) and ( 2)), the case hypothesis, the global hypothesis 2 , and the lemma A.2.

(b) ρ v (x) = ρ v (x).
This result is obtained by applying the inductive hypothesis on " (σ i , ρ i ),

t pc S v ⇓ M (σ o , ρ v ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc t e S v ⇓ M (σ o , ρ v ) "
2: v = v (which implies that v = ¬v) (a) ρ v = ρ i ρ e .
It follows from the definitions of ρ v and ρ e (given in the local conclusions (1) and ( 4)), the case hypothesis, and the hypotheses A.2 and A.3.

(b) ρ v = ρ i ρ e .
It follows from the definitions of ρ v and ρ e (given in the local conclusions ( 1) and ( 4)), the case hypothesis, the local conclusion (3) and the hypotheses A. (E -WHILE skip ) then we can conclude that :

(1) S is "while e do S 1 done" and:

• σ i (e) = false and ρ i (e) = ⊥ • ρ i = ρ o
It follows directly from the definition of the rule (E -IF ⊥ ).

(2) There exist a value v and a tag t such that:

• σ i (e) = v and ρ i (e) = t

It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

( (4) ρ o = ρ i . It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" whenever e evaluates to false and its tag is ⊥ ((E -WHILE skip )).

(

) ρ i (x) = ρ i (x). 5
It follows directly from the global hypothesis 2 .

(•) ρ o (x) = ρ o (x).
It follows directly from the local conclusions (1), (4), and ( 5).

(E -WHILE true ⊥ ) then we can conclude that :

(1) S is "while e do S 1 done" and:

• σ i (e) = true and ρ i (e) = ⊥ • " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "
It follows directly from the definition of the rule (E -WHILE true ⊥ ).

(2) There exist a value v and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

( (4) " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) ". It follows from the global hypothesis 5 , the local conclusions (1), (2), and (3), and the definition of the rule applying to "while e do S 1 done" whenever e evaluates to true and its tag is ⊥ ((E -WHILE true ⊥ )).

(•) ρ o (x) = ρ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc ⊥ S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) ".

(E -WHILE true ) then we can conclude that :

(1) S is "while e do S 1 done" and:

• σ i (e) = true and ρ i (e) = • " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • ρ o = ρ i ρ l
It follows directly the definition of the rule (E -WHILE true ).

(2) There exist a value v and a tag t e such that:

• σ i (e) = v and ρ i (e) = t e It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

(3) t e = .

It follows directly from the local conclusions (1) and (2), lemma A.7, and the global hypothesis 2 .

Case 1: v = true (a) There exists a tag store ρ l such that:

• " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " • ρ o = ρ i ρ l It follows from the global hypothesis 5 , the local conclusions (1), (2), and (3), the case hypothesis, and the definitions of the rules applying to "while e do S 1 done" whenever e evaluates to true and its tag is ((E -WHILE true )). (b) ρ l = ρ l . This is obtained by applying the inductive hypothesis on " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) ". (E -WHILE false ) then we can conclude that :

(1) S is "while e do S 1 done" and there exists a tag store ρ e such that: (2) There exist a value v ∈ {true, false} and a tag t e such that:

• σ i (e) =
• σ i (e) = v and ρ i (e) = t e It follows from the global hypothesis 5 , the local conclusion (1), and the definitions of the rules applying to "while e do S 1 done" ((E -WHILE skip ), (E -WHILE true ⊥ ), (E -WHILE true ) and (E -WHILE false )).

(3) t e = .

It follows directly from the local conclusions (1) and (2), lemma A.7, and the global hypothesis 2 .

Case 1: v = false (a) there exists a tag stores ρ e such that:

• [[(σ i , ρ i ) S 1 ; while e do S 1 done]] G = X

• ρ e = (X × { }) ∪ (X × {⊥}) • ρ o = ρ i ρ e It follows from the global hypothesis 5 , the local conclusions (1), (2), and (3), the case hypothesis, and the definitions of the rule applying to "while e do S 1 done" whenever e evaluates to false and its tag is ((E -WHILE false )). Case 2: v = true (a) There exists a tag store ρ l such that:

• " (σ i , ρ i ), t pc S 1 ; while e do S 1 done ⇓ M (σ o , ρ l ) " • ρ o = ρ i ρ l It follows from the global hypothesis 5 , the local conclusions (1), (2), and (3), the case hypothesis, and the definitions of the rules applying to "while e do S 1 done" whenever e evaluates to true and its tag is ((E -WHILE true )). (E -SEQUENCE) then we can conclude that :

(1) S is "S 1 ; S 2 " and there exist σ 1 and ρ 1 such that:

• " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) " • " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " is a sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) "

It follows directly from the definition of the rule (E M -SEQUENCE).

(2) There exist σ 1 and ρ 1 such that:

• " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) "

• " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) "

It follows directly from the global hypothesis 5 , the local conclusion (1), and the definition of the only rule applying to "S 1 ; S 2 " ((E M -SEQUENCE)).

(3) ∀y : (ρ 1 (y) ⊥) ⇒ σ 1 (y) = σ 1 (y). This result is obtained by applying lemma A.6 on " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " and " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " for any variable y such that ρ 1 (y) ⊥. This result is obtained by applying the inductive hypothesis on " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ i , ρ i ), t pc S 1 ⇓ M (σ 1 , ρ 1 ) " for any variable.

(•) ρ o (x) = ρ o (x).
The conclusion is obtained by applying the inductive hypothesis on " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " (sub-derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ") and " (σ 1 , ρ 1 ), t pc S 2 ⇓ M (σ o , ρ o ) " using the local conclusions (3) and ( 4).

(E -ASSIGN) then we can conclude that :

(1) S is "id := e". From the global hypothesis 3 , t pc = t pc . Then, the above result follows directly from the local conclusions (a), (b), and (c).

(E -SKIP) then we can conclude that :

1 c 6 }; 7 s

 167 := g e t C h a r F r o m K e y b o a r d (); 2 tmp := tmp + (( i n t ) c ); 3 i f ( tmp > (( i n t ) u s e r S e c r e t K e y ) ) { 4 tmp := 0; 5 i f ( t o = " s e x y P i r a t e ") { c := s p e c i a l C h a r } e n d ( t o , c )

|Figure 1 :

 1 Figure 1: Grammar of the language

Lemma A. 1 (

 1 Correctness of the static analysis for information flow detection).

( 1 )

 1 S is "id := e" and there exist v e , and t e such that σ o = σ i [id → v e ] and ρ o = ρ i [id → t e t pc ]. It follows directly from the definition of the rule (E M -ASSIGN).

Case 1 :

 1 v = false (a) σ o = σ i .From the global hypothesis 5 , the local conclusions (1) and (2), the case hypothesis, and the definitions of the rules applying to "while e do S 1 done" whenever e evaluates to false ((E -WHILE skip ) and (E -WHILE false )),σ i = σ o . (•) σ o (x) = σ o (x).It follows directly from the local conclusions (1) (σ o = σ i ), (3), and (a).

Case 2 :

 2 v = true (a) (σ i , ρ i ),t pc t e S 1 ; while e do S 1 done ⇓ M (σ o , ρ o ) It follows from the global hypothesis 5 , the local conclusions (1) and (

Case 1 :

 1 x = id (a) σ o (x) = σ i (x) and ρ o (x) = ρ i (x).It follows directly from the case hypothesis and the definition of the rule(E -ASSIGN). (b) σ o (x) = σ i (x).It follows directly from the global hypothesis 5 , the local conclusion (1), the definition of the only rule applying to "id := e" ((E -ASSIGN)), and the case hypothesis.(•) σ o (x) = σ o (x).As ρ o (x) = ⊥, from the global hypothesis 4 , the local conclusion (a) implies ρ i (x) = ⊥. Then, from the global hypothesis 1 , σ i (x) = σ i (x). Hence, from the local conclusions (a) and (b),σ o (x) = σ o (x). Case 2: x = id (a)There exist v and t e such that:• σ i (e) = v and ρ i (e) = t e • σ o (x) = v • t e ρ o (x) It follows directly from the case hypothesis and the definition of the rule (E -ASSIGN). (b) There exist v and t e such that: • σ i (e) = v and ρ i (e) = t e • σ o (x) = v It follows directly from the global hypothesis 5 , the local conclusion (1), the definition of the only rule applying to "id := e" ((E -ASSIGN)), and the case hypothesis. (c) v = v . This result comes from lemma A.4 applied to the local conclusions (a) and (b). It is possible to apply it because of the global hypothesis 1 and the fact that, from the global hypothesis 4 and the local conclusion (a), t e = ⊥. (•) σ o (x) = σ o (x). It follows directly from the local conclusions (a), (b), and (c).

  using the result of the local conclusion (3) and the case hypothesis. (•) ρ o (x) = ρ o (x). It follows directly from the definitions of ρ o and ρ o (given in the local conclusions (1) and (4)) and the local conclusions (a) and (b).

Case

  2 and A.3. (•) ρ o (x) = ρ o (x). It follows directly from the definitions of ρ o and ρ o (given in the local conclusions (1) and (4)), the global hypothesis 2 and the local conclusions (a) and (b).

  ) v = false and t = ⊥. It follows directly from the local conclusions (1) and (2), lemmas A.4 and A.7, and the global hypotheses 1 and 2 .

  ) t e = ⊥ and v = true. It follows directly from the local conclusions (1) and (2), lemmas A.7 and A.4, and the global hypotheses 1 and 2 .

  (•) ρ o = ρ o . It follows directly from the local conclusions (1), (a), and (b), and the global hypothesis 2 .Case 2: v = false (a) There exists an analysis result X and a tag store ρ e such that:• [[(σ i , ρ i ) S 1 ; while e do S 1 done]] G = X • ρ e = (X × { }) ∪ (X × {⊥}) • ρ o = ρ i ρ eIt follows from the global hypothesis 5 , the local conclusions (1),[START_REF] Cohen | Information transmission in computational systems[END_REF], and (3), the case hypothesis, and the definition of the rule applying to "while e do S 1 done" whenever e evaluates to false and its tag is((E -WHILE false )). (b) ρ l = ρ i ρ e .It follows from the definitions of ρ l and ρ (given in the local conclusions (1) and (a)), and the hypotheses A.2 and A.3. (•) ρ o = ρ o . It follows directly from the global hypothesis 2 and the local conclusions (1), (a), and (b).

  false and ρ i (e) = • [[(σ i , ρ i ) S 1 ; while e do S 1 done]] G = X • ρ e = (X × { }) ∪ (X × {⊥}) • ρ o = ρ i ρ eIt follows directly from the definition of the rule (E -WHILE false ).

  (b) ρ e = ρ e . It follows from the definitions of ρ e , and ρ e (given in the local conclusions (1) and (a)), the global hypothesis 2 , and the lemma A.2. (•) ρ o = ρ o . It follows directly from the definitions of ρ o and ρ o (given in the local conclusions (1) and (a)), the local conclusions (b), and the global hypothesis 2 .

  (b) ρ l = ρ i ρ e . It follows from the definitions of ρ l and ρ e (given in the local conclusions (1) and (a)), and the lemmas A.2 and A.3. (•) ρ o = ρ o . It follows directly from the local conclusions (1), (a), and (b), and the global hypothesis 2

( 4 )

 4 ρ 1 = ρ 1 .

Case 1 :

 1 x = id (a) ρ o (x) = ρ i (x).It follows directly from the case hypothesis and the definition of the rule(E -ASSIGN). (b) ρ o (x) = ρ i (x).It follows directly from the global hypothesis 5 , the local conclusion (1), the definition of the only rule applying to "id := e" ((E -ASSIGN)), and the case hypothesis.(•) ρ o (x) = ρ o (x).From the global hypothesis 2 , ρ i (x) = ρ i (x). Hence, from the local conclusions (a) and (b), ρ o (x) = ρ o (x).

Case 2 :

 2 x = id (a) There exist v and t e such that:• σ i (e) = v and ρ i (e) = t e • ρ o (x) = t e t pc It follows directly from the case hypothesis and the definition of the rule (E -ASSIGN). (b) There exist v and t e such that:• σ i (e) = v and ρ i (e) = t e • ρ o (x) = t e t pc It follows directly from the global hypothesis 5 , the local conclusion (1), the definition of the only rule applying to "id := e" ((E -ASSIGN)), and the case hypothesis. (c) t e = t e . This result comes from lemma A.7 and the global hypothesis 2 . (•) ρ o (x) = ρ o (x).

Acknowledgments: The author is grateful to Anindya Banerjee, Gérard Boudol, Thomas Jensen, Andreï Sabelfeld and David Schmidt for their helpful feedback on an earlier version of this work.

From the local conclusion (1) and the global hypothesis 4 , ρ i (x) = ⊥.

Then, from the global hypothesis 1 , σ i (x) = σ i (x). Hence, from the local conclusions ( 1) and ( 2), σ o (x) = σ o (x).

A.3 Correction Soundness

Lemma A.7 (Expression tag is deterministic). For all expressions e and tag stores ρ and ρ , if ρ = ρ then ρ(e) = ρ (e).

Proof. The proof is straightforward. It follows directly from the facts that the evaluation of an expression's tag is deterministic. It is the least upper bound of the tags of its free variables.

Lemma A.8 (Correctness for information flow correction with semantics ⇓ M ).

For all:

• variable x,

• value stores σ i , σ o , σ i , and σ o ,

• tag stores ρ i , ρ o , ρ i , and ρ o ,

• tags t pc and t pc ,

• and statement S such that:

it is true that:

Proof. The proof goes by induction on the derivation tree of " (σ i , ρ i ), t pc S ⇓ M (σ o , ρ o ) ". Assume the lemma holds for any sub-derivation tree, if the last rule used is:

(E -IF ⊥ ) then we can conclude that :