Frédéric Besson

Nataliia Bielova

Thomas Jensen

Hybrid Monitoring of Attacker Knowledge

Enforcement of noninterference requires proving that an attacker's knowledge about the initial state remains the same after observing a program's public output. We propose a hybrid monitoring mechanism which dynamically evaluates the knowledge that is contained in program variables. To get a precise estimate of the knowledge, the monitor statically analyses non-executed branches. We show that our knowledgebased monitor can be combined with existing dynamic monitors for non-interference. A distinguishing feature of such a combination is that the combined monitor is provably more permissive than each mechanism taken separately. We demonstrate this by proposing a knowledge-enhanced version of a no-sensitive-upgrade (NSU) monitor. The monitor and its static analysis have been formalized and proved correct within the Coq proof assistant.

I. Introduction

Information-flow control provides a promise of a strong information security property [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Today most research has focused on monitors for noninterference [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF], [START_REF] Austin | Permissive dynamic information flow analysis[END_REF], [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF], [START_REF] Zdancewic | Programming languages for information security[END_REF], that block executions where secret inputs flow into public outputs. Such flow can happen due to explicit or implicit information flow. An explicit flow occurs when secret information is stored in a public variable visible to an attacker. An implicit flow happens when assignments to public variables are made under secret control (i.e., following a test on a secret variable), like in Program 1. 1Program 1 1 l = 0; if (h) then l = 1; output l There is an implicit flow from h to l because by observing the value of l the attacker can deduce the secret value h.

Dynamic monitors control one execution of the program and propagate a security label to each program variable. If the monitor suspects a possible flow (explicit or implicit) from secret inputs to a variable labeled as public, it blocks the execution. Such purely dynamic information flow control was first proposed by Fenton [START_REF] Fenton | Memoryless subsystems[END_REF] and has recently regained interest [START_REF] Austin | Permissive dynamic information flow analysis[END_REF], [START_REF] Zdancewic | Programming languages for information security[END_REF] for (at least) two reasons. First, some languages, such as JavaScript, are so dynamic that a precise static analysis is practically impossible. Therefore, an attractive alternative is to resort to dynamic monitoring, either by extending an interpreter for the language or by inlining a monitor in the program. Second, even if a program may have some insecure executions, there may be other executions that are perfectly secure. While a static analysis would reject such programs, dynamic monitors can identify and allow some secure executions of insecure programs.

However, dynamic monitors also have several limitations, due to the fact that they analyse only one execution of a program. As a result, they make the worstcase assumption about what happens later on in the current execution, and what could happen in other executions. Dynamic information flow control first proposed by Zdancewic [START_REF] Zdancewic | Programming languages for information security[END_REF] and later used by Austin and Flanagan [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF] is based on the no-sensitive-upgrade (NSU) principle: it halts an execution when a public variable gets assigned under secret control. This principle severely limits the permissiveness of dynamic monitors in certain cases.

• They may block executions too early: if later a variable is updated, then there is no information leakage.

Program 2 1 if (h) then l = 1; 2 l = 0; 3 output l Program 2 is secure but its execution is blocked by NSU when h = true.

• If the variable is assigned the same value on both branches, there is no leakage. Program 3 is secure but NSU blocks all its executions.

Program 3 1 x = 1; 2 if (h) then l = 1 else l = x; 3 output l The first problem of blocking execution too early was addressed by the permissive-upgrade (PU) principle [START_REF] Austin | Permissive dynamic information flow analysis[END_REF], by introducing a special "partially leaked" label. The second problem requires knowledge about other executions and has motivated a strand of research in hybrid information flow monitors that combine static and dynamic analysis.

Hybrid monitors (e.g. [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF], [START_REF] Guernic | Precise Dynamic Verification of Confidentiality[END_REF], [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF], [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF]) analyse the source code of each non-executed branch under secret control to detect possible implicit flows. A dynamic monitor can be enhanced with a variety of static analyses. Le Guernic [START_REF] Guernic | Precise Dynamic Verification of Confidentiality[END_REF] proposed the first combination of dynamic information flow monitors with static dependency analyses. Besson et al. [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF] extended this work to a more sophisticated constant propagation and dependency analysis. Recently, Hedin et al. have shown how to improve their dynamic information flow analysis for JavaScript [START_REF] Hedin | Information-flow security for a core of JavaScript[END_REF] with a pointsto analysis [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF].

Permissiveness. All the monitors discussed above provably enforce noninterference, however some of them (a) from Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF].

(b) our result Fig. 1: Relative permissiveness revisited. may block more program executions than others. Intuitively, permissiveness defines how many program executions are accepted by the monitor even if the program may be insecure. Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF] have proven that purely dynamic and hybrid monitors are incomparable in their permissiveness. For example, a dynamic NSU monitor allows execution of Program 1 when h = false, while the hybrid monitor stops it. On the other hand, the dynamic NSU monitor will stop execution of Program 2 when h = true while the hybrid monitor will allow it. Figure 1a graphically shows the secure programs, and programs, for which the static, dynamic and hybrid analysis identify as secure all its executions (from Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF]).

In this paper, we propose a knowledge-based hybrid monitor that is able to reach a level of permissiveness that was deemed impossible for standard hybrid monitors. Figure 1b graphically shows that all the executions of all the secure programs that are accepted by dynamic monitors, are also accepted by an enhanced version of our knowledge-based hybrid monitor.

Modelling attacker knowledge. Basic information flow control detects whether or not a program execution may leak information, but will not provide a more precise description of what information is being leaked, or equivalently, what knowledge an attacker gains from an observation. However, switching to such knowledgebased analysis can provide a finer control over information flow. In a previous paper [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF], the authors have proposed a hybrid information flow control that combines dynamic monitoring and static analysis. This technique computes the leakage of a concrete program execution by labeling every program variable with a logic formula over the secret inputs. This formula is a logical description of the knowledge that an attacker can deduce about the initial state of the program when he observes the value of a variable. Consider the following program and its execution when h1 = false and h2 = true. Given the same initial memory where h1 = false and h2 = true, the hybrid monitor of Besson et al. [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF] associates the knowledge to the variable after analysing each test: the first test on h1 fails, thus the value of y remains unchanged and the knowledge of y is ¬h1; upon the second test, the monitor concludes that the value of x is 1 in the true branch and 0 in the false branch. As the values are not the same, the knowledge of the output x = 1 might depend on h2 and on the knowledge of y. Therefore, the knowledge computed by the monitor is:

Approximated knowledge: ¬h1 ∧ h2
As is readily seen, the approximated knowledge is much less precise than the real attacker knowledge. The reason for this gap between estimated and actual knowledge is in the choice of the model of knowledge domain. Intuitively, the knowledge in [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF] is limited to a set of environments that can contribute to the current value of x.

A more expressive knowledge domain. In this paper, we propose a more general representation of attacker knowledge: the knowledge associated with a variable x is the set of environments that lead to a particular value of x for several possible values of x. In other words, the knowledge in x groups the initial environments into equivalence classes, such that two environments are equivalent if they lead to the same value of x. This models much more of the input-output relation of the program.

This new knowledge domain leads to several advantages over the existing previous work [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF]. The first advantage is that it empowers the monitor to reason about several executions, and hence to prove noninterference in more cases than in previous work [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF]. For a concrete example, see Example 1 in Section IV-B. With the previous knowledge representation in [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF], we would infer that z depends on x and y; while with the new representation we prove that x and y do not interfere with z.

The second advantage of this more expressive knowledge domain is that it enables a composition with other monitors, and we demonstrate such composition with the no-sensitive upgrade (NSU) monitor. The new knowledge domain allows the hybrid monitor to reason about the other executions that would be blocked by the other dynamic monitor for non-executed paths. This leads to a composition of monitors that is strictly more permissive that each monitor separately. We summarise this result in Figure 1b, showing that the knowledge-based hybrid monitor accepts more secure executions than any purely dynamic monitor it is built upon2 .

The third advantage is that the proposed knowledge domain allows us to design a more precise static analysis. Our knowledge domain is used for both the dynamic analysis of the executed branch and the static analysis of nonexecuted branched. This gives a pleasant uniformity to the theory and provides a more general framework, compared to the ad-hoc static analyses for the non-executed branches in [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF].

Contributions.

• We propose a hybrid monitor that computes the knowledge of the attacker Our monitor combines a dynamic analysis with a static analysis of the nonexecuted branches. The knowledge domain allows the monitor to compute an attacker's knowledge more precisely than in previous works [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF]. • The knowledge-based hybrid monitor is proved to be correct (it safely over-approximates the attacker's knowledge) and sound (it can be used to enforce noninterference). The proof has been formalized in the Coq proof assistant [START_REF]Formalisation of the Hybrid Monitor in Coq[END_REF]. • The proposed monitor can be combined with existing dynamic or hybrid monitors for non-interference. A distinguishing feature of such a combination is that the combined monitor is provably more permissive than the monitor it builds upon. • We have proposed an effective and symbolic representation of knowledge and implemented the computation of knowledge as part of our Coq formalization.

The results reported in this paper are all computed with this implementation.

II. Attacker knowledge and non-interference A. Attacker model

We consider a classical attacker model, following the definition of gadget attacker [START_REF] Barth | Securing frame communication in browsers[END_REF]. An attacker provides the program source code and this program runs in an environment that contains secret information, producing some outputs, observable to the attacker.

B. Attacker knowledge

Given an observation at the end of an execution, an attacker knowledge is the set of all possible input environments that can lead to that observation. This naturally induces an equivalence relation on input environments. Landauer and Redmond [START_REF] Landauer | A lattice of information[END_REF] propose a lattice of equivalence classes of environments for representing the knowledge of an attacker. Askarov and Sabelfeld [START_REF] Askarov | Gradual release: Unifying declassification, encryption and key release policies[END_REF] and Askarov and Chong [START_REF] Askarov | Learning is change in knowledge: Knowledge-based security for dynamic policies[END_REF] give a characterisation of non-interference in terms of attacker knowledge. The remainder of this section summarizes notions and results from these papers.

We assume a security policy in the form of a lattice of two security levels ({L, H}, ), where L H and we use as the least upper bound. A labelling function Γ assigns security levels to all program variables. We write ρ L for the L-projection of the environment ρ onto those variables x whose level is lower than L, i.e., for which Γ(x) L, and in the future notations we drop an implicit labelling function Γ. We write [ρ] L for the set of environments that agree with ρ on low variables:

[ρ] L = {ρ | ρ L = ρ L }.
The program semantics is given by a relation (P, ρ) ↓ v, where P is a program that produces output v at the end of the execution. This output is visible to the attacker. The knowledge is defined as the set of low-equivalent environments that can produce the same output v. Definition 1 (Attacker knowledge). Given a program P , an initial environment ρ, and a final observation v, the attacker knowledge is the set of environments that agree with ρ on low variables and leads to the observation of v:

K ↓ (P, v, ρ) = {ρ | ρ L = ρ L ∧ (P, ρ ) ↓ v}.
Notice that a smaller knowledge set represents fewer possible inputs that produce the same program output, thus a smaller set corresponds to a bigger amount of information. Therefore, a smaller knowledge set is a safe approximation of the actual attacker knowledge.

C. Termination-Insensitive Noninterference

In the following, we describe the relationship between knowledge and the standard notion of noninterference. We shall focus on termination-insensitive noninterference (TINI), and hence restrict attention to a terminationinsensitive version of knowledge that only considers environments in which the program terminates and where the program output is visible to the attacker. The knowledge obtained just from observing termination, given an initial observation ρ L is called initial attacker knowledge. Definition 2 (Initial attacker knowledge). Given program P and an environment ρ, the initial attacker knowledge is:

I ↓ (P, ρ) = {ρ | ρ L = ρ L ∧ ∃v.(P, ρ ) ↓ v]}.
Later on, we omit the superscript ↓ when it can be inferred from the context.

The security condition states that the attacker's knowledge should not grow with the new observation produced by the program execution. Definition 3 (Knowledge-based security for input environment ρ). Program P is secure for an initial input environment ρ if whenever (P, ρ) ↓ v then

K(P, v, ρ) = I(P, ρ).
Notice that if the program P does not terminate in an environment ρ, then P is considered secure for ρ. However, the program still might be insecure for any other low-equal environment, in which the program terminates.

The standard notion of termination-insensitive noninterference (TINI) is stated by comparing pairs of lowequivalent initial environments.

Definition 4 (TINI). A program P is terminationinsensitively noninterferent (TINI) if whenever ρ 1

L = ρ 2 L , and (P, ρ 1 ) ↓ v 1 and (P,

ρ 2 ) ↓ v 2 , then v 1 = v 2 .
Askarov and Sabelfeld [START_REF] Askarov | Gradual release: Unifying declassification, encryption and key release policies[END_REF]Prop. 2] have shown that there is an equivalence between the knowledge-based security and TINI for a lattice with two elements.

Lemma 1. A program P satisfies TINI if and only if P

is secure for all initial environments ρ.

III. Preliminaries

A. Language

We use a simple untyped imperative language extended with a specific output command output x which evaluates the variable x and outputs its value. This output is visible to the attacker at security level L. All the commands of the language are standard, except perhaps for the assume(e) operator, which evaluates e and continues or halts an execution depending on whether its value is true or false. The syntax of this language is as follows:

P P ::= c; output x E e ::= n | x | e 1 ⊕ e 2 | ¬e C c ::= skip | x:= e | c 1 ; c 2 | assume(e) | if e then c 1 else c 2 | while e do c
The set of expressions contains the usual numeric and Boolean expressions. Every expression can be interpreted as a boolean value, and hence conditional commands take an arbitrary expression as condition. The exact interpretation of expressions as booleans is, however, not essential to the results in this paper and will be left unspecified. We use ⊕ to denote an arbitrary binary operator.

An environment ρ ∈ Env = Var → V maps variables to values. The big-step program semantics is presented in Figure 2. The semantics of commands is denoted by a binary relation (c, ρ) ↓ ρ meaning that command c when executed in environment ρ will evaluate to ρ and the semantics of programs is denoted by (P, ρ) ↓ v meaning that program P when executed in environment ρ will produce an output v.

skip (skip, ρ) ↓ ρ assign (x := e, ρ) ↓ ρ[x → e ρ ] seq (c 1 , ρ) ↓ ρ (c 2 , ρ ) ↓ ρ (c 1 ; c 2 , ρ) ↓ ρ assume C e ρ = tt (assume(e), ρ) ↓ ρ if C e ρ = α (c α , ρ) ↓ ρ (if e then c tt else c ff , ρ) ↓ ρ while (if e then c; while e do c else skip, ρ) ↓ ρ (while e do c, ρ) ↓ ρ output (c, ρ) ↓ ρ x ρ = v (c; output x, ρ) ↓ v where x ρ = ρ(x) n ρ = n e 1 ⊕ e 2 ρ = e 1 ρ ⊕ e 2 ρ
Fig. 2: Language semantics Let B denote the set of boolean values. To accommodate the fact that any expression can be used as a condition, we assume a function C : V → B that specifies how each value is interpreted as a boolean. C satisfies the following two constraints which ensure that ¬e represents the negation of the expression e and e = e models the fact that e and e evaluates to the same value:

C( ¬e ρ ) = ¬C( e ρ ) C( e = e ρ ) = ( e ρ = e ρ )

B. Notations

Given sets A and V , we write V for V ∪ {⊥, }. In domains of the form V we write v to assert that v is an element that is neither ⊥ nor . For a function f

∈ A → V , we write f (a) = v for f (a) = v ∧ v / ∈ {⊥, } and f -1 (v) = {a | f (a) = v } for the pre-image of v.
Given a domain V , we get a flat lattice (V , , ⊥, ) such that ⊥

x, x and x x . Given x, y, we write x y (resp. x y) the the least upper bound (resp. greatest lower bound) of x and y. The ordering, least upper bound and greatest lower bound are lifted to functions in the standard pointwise fashion:

f g iff ∀x, f (x) g(x); (f g)(x) = f (x) g(x); (f g)(x) = f (x) g(x).
Given a unary operator o : V → W , we define an operator o : V → W as follows

o (x) = if x ∈ {⊥, } then x else o(x).
Similarly, for a binary operator ⊕ :

V → V → V we define ⊕ : V → V → V as x ⊕ y =    v 1 ⊕ v 2 if x = v 1 ∧ y = v 2 ⊥ if x = ⊥ ∨ y = ⊥ otherwise.
We define a binary operator assume : B → V → V which returns its second argument if the first argument is either true or , and undefined otherwise.

assume(b, v) = if (b = true ∨ b = ) then v else ⊥.
Finally, we define a conditional operator if : B → V → V → V built from assume, where ¬ is a standard negation operator extended to the domain B :

if (b, v, v ) = assume(b, v) assume(¬ b, v ).
Given c : A → V and f, g ∈ A → V , we write Assume(c, f ) and IF (c, f, g) for the assume and conditional operators lifted to functions:

Assume(c, f )(a) = assume(C (c(a)), f (a)) IF (c, f, g)(a) = if (C (c(a)), f (a), g(a)).
where C is the function C lifted to the domain V → B .

IV. A hybrid knowledge-based monitor Our hybrid information flow analysis computes the knowledge of a program's input-output behaviour that the attacker obtains by observing the result of a given execution of the program. More precisely, we shall define the domain K of knowledge to be the set of functions K that maps environments ρ to values v, with the intention that K(ρ) = v if the program when started in initial environment ρ will either produce an output v or not terminate. If the hybrid monitor from initial state ρ calculates final value v and knowledge K, then K -1 (v) is a safe approximation of the set of all the environments that produce v. This set will allow us to safely approximate the attacker's knowledge (see Theorem 1). Definition 5 (Knowledge). The domain K of knowledge is defined by:

K = Env → V .
Notice that the monitor may compute knowledge K ∈ K that will map an environment to ⊥ or . This is due to the presence of the static analysis. If K(ρ) = ⊥ then the static analysis has established that computation started in ρ will not terminate. On the other hand, K(ρ) = means that approximations in the static analysis made it impossible for the monitor to determine what value will result from an execution starting in ρ. This means that ρ cannot be added to the knowledge set K -1 (v) for any possible output v. Recall that a knowledge analysis may always safely under-approximate the knowledge set

K -1 (v) of output v, so having K(ρ) =
for some ρ makes the knowledge analysis more conservative than an analysis that is capable of determining the exact output for ρ.

A. Monitor semantics

We now define a hybrid knowledge monitor that combines dynamic monitor with static analysis. The hybrid monitor executes the program and at the same time computes an over-approximation of the knowledge of the initial state that can be deduced from the current state at a given point in the execution. The semantic state of the hybrid monitor is thus a pair (ρ, κ), where the first component is either an environment Env containing the current values of the variables, or an empty environment • that will be used by the static analysis; the second component κ ∈ Var → K is an environment containing the knowledge present in each variable. At branching points, the monitor will execute one branch and will statically analyse the other, non-executed branch. This static analysis will help refining the computation of the actual knowledge stored in variables.

Given a concrete initial environment ρ, the initial state of the hybrid monitor init(ρ) is such that each variable x has the knowledge of the current value of x in the initial environment: init(ρ) = (ρ, κ 0 ) with κ 0 = λx.λρ .ρ (x). To see this, suppose that the program immediately outputs the value v of variable x i.e. v = ρ(x). The set of environments {ρ | ρ (x) = v} that produce v is modeled exactly by κ 0 (x)

-1 (v).

From the initial state, the monitor executes according to the rules of Figure 3. The concrete execution and the static analysis are combined into one reduction relation ⇓. The rules skip and seq are standard. For the other language constructs, there are two rules: a dynamic rule describing the monitored execution of the construct, and a static rule describing the static analysis of it. The dynamic rules will operate on environments with the actual values of the variables. The static analysis, on the other hand, is intended to provide information about all other possible executions so it will not have information about concrete values. In the formalization, this means that the static rules apply only when the environment is undefined (denoted by •).

The two rules assignDyn and assignStat for assignment use the function _ κ to evaluate the knowledge about the initial environment contained in the value of the expression e. The function takes the current knowledge environment κ as parameter. In addition, the dynamic rule updates the value of x in the environment ρ.

The rule ifDyn describes the monitored execution of conditional statements of form if e then c tt else c ff . The outcome of the test α is the value of the expression e computed in the environment ρ and the appropriate branch is executed with that environment, producing a new environment ρ and a new knowledge environment κ α . The non-executed branch c ᾱ is statically analysed, using an undefined environment of values and the current knowledge environment. The knowledge environment κ ᾱ obtained from this static analysis must be combined with the knowledge environment from the execution κ α . To this end, we construct the function IF( e κ , κ tt , κ ff ) that uses a conditional operator IF (c, f, g) from Section III-B. We later show that in programs without loops the IF operator allows us to precisely model the attacker's knowledge.

For the while loop, the dynamic rules whileDynTrue and whileDynFalse are standard unfolding semantic rules that apply when the environment is defined. The static rule whileStat states that any s whose knowledge safely approximates the knowledge before entering the loop (condition s s ) as well as the knowledge after executing the body of the loop (condition s 1 s ) is a valid result of the static analysis of the loop. The rule leaves room for an actual implementation to compute more or less precise approximations of the attacker knowledge after a loop. Our implementation (Section VII) employs an iterative fixpoint computation to this end.

We do not define a rule for analysing the output command output x, because it does not change the knowledge of any variable. The output x command is important because it is at this point that we must decide what to output and, hence, what security property to enforce. In Section V, we shall propose rules for the output command that will enforce enforce non-interference.

B. Examples

To illustrate the expressive power of our hybrid monitor, we provide a number of examples. They show when the monitor computes precise knowledge but also limitations due to the static analysis of loops. They also illustrate the role played by the static detection of termination.

skip (skip, s) ⇓ s seq (c 1 , s) ⇓ s (c 2 , s ) ⇓ s (c 1 ; c 2 , s) ⇓ s assignDyn e ρ = v e κ = e (x := e, (ρ, κ)) ⇓ (ρ[x → v], κ[x → e ]) assignStat e κ = e (x := e, (•, κ)) ⇓ (•, κ[x → e ]) assumeDyn C e ρ = tt (assume(e), (ρ, κ)) ⇓ (ρ, A( e κ , κ)) assumeStat (assume(e), (•, κ)) ⇓ (•, A( e κ , κ)) ifDyn C e ρ = α (c α , (ρ, κ)) ⇓ (ρ , κ α ) (c ᾱ, (•, κ)) ⇓ (•, κ ᾱ) (if e then c tt else c ff , (ρ, κ)) ⇓ (ρ , IF( e κ , κ tt , κ ff )) ifStat (c tt , (•, κ)) ⇓ (•, κ tt ) (c ff , (•, κ)) ⇓ (•, κ ff ) (if e then c tt else c ff , (•, κ)) ⇓ (•, IF( e κ , κ tt , κ ff )) whileDynTrue C e ρ = tt
(if e then c; while e do c else skip, s)

⇓ s s = (ρ, κ) (while e do c, s) ⇓ s whileDynFalse C e ρ = ff
(if e then while e do c else skip, s)

⇓ s s = (ρ, κ) (while e do c, s) ⇓ s whileStat (assume(e); c, s ) ⇓ s 1 s 1 s s s (assume(¬e), s ) ⇓ s s = (•, κ) (while e do c, s) ⇓ s where x κ = κ(x) n κ = λρ. n e 1 ⊕ e 2 κ = λρ. e 1 κ (ρ) ⊕ e 2 κ (ρ) IF(c, κ 1 , κ 2 )(x) = IF (c, κ 1 (x), κ 2 (x)) A(c, κ)(x) = Assume(c, κ(x)) (ρ, κ) (ρ , κ ) iff κ κ ∧ ρ = ρ
(z) = λρ.if (C h ρ , x + y ρ , y -x ρ ).
The program is loop-free and therefore κ(z) is a function which encodes exactly the function computing the final value of z from the initial environment. Suppose that the final value of z is 1, the knowledge of the output 1 is obtained by κ(z)

-1 (1) = {ρ | if (C h ρ , x + y ρ , y -x ρ ) = 1}.
Suppose that initially h = true, x = 0 and y = 1. As a result, L-equivalent environments are {ρ | ρ(x) = 0 ∧ ρ(y) = 1} 3 . This program is indeed secure for the given initial environment (see Definition 3) since all L-equivalent environments output the value 1. Notice that all of them are included in κ(z)

-1 (1): if x = 0 and y = 1 then the condition if (h, x + y, y -x) = 1 always holds:

if (h, 0 + 1, 1 -0) = 1 ⇔ if (h, 1, 1) = 1 ⇔ 1 = 1.
3 As z is set in both branches, its initial value is irrelevant.

Notice that both dynamic monitors and the standard hybrid monitors block all executions of this program either because there is a low assignment under a high security context in both branches, or because an output variable z explicitly depends on h. We will show in Section VI-C that this power of proving non-interference allows our monitor to be more permissive than other monitors.

Example 2 (Detection of loop non-termination). Interestingly, our monitor may be more precise than other monitors even in the presence of loops in a high security context. Consider Program 6.

Program 6

1 l := 0; 2 if h then skip 3 else while true do l := 1; 4 output l When h is true, the purely dynamic monitors would accept this execution, while the previous hybrid monitors [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF], [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF] would block it since the hybrid monitor would detect that a value of l might change in the non-executed branch.

However, our monitor is able to detect the nontermination of the while loop. On line 2, we apply the IfDyn rule, and compute κ(l) = λρ.if (C h ρ , κ 0 (l), κ (l)), where κ 0 (l) = λρ.0 and κ is computed by the WhileStat rule. The first three premises of this rule ensure that in state s = (⊥, κ ), we have κ (l) = λρ. since l is updated in the loop body. However, the forth premise ((assume(¬e), s ) ⇓ s ) ensures that κ (l) = λρ.⊥ thus being able to conclude that whenever h is f alse, the program does not terminate.

Example 2 shows that our static analysis allows us to detect non-termination of the loops in some cases. Notice that this capability does not give us soundness for termination-sensitive noninterference, but gives more precision for termination-insensitive noninterference. In contrast, the knowledge monitor in our previous work [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF] is not able to prove termination-insensitive noninterference for Example 2 since its static analysis only determines that the output l may depend on the secret h.

C. Limitations

Our hybrid monitor is not always capable of computing the exact knowledge. A fundamental reason is that the knowledge is computed for each variable independently. Therefore, it cannot express a relation, e.g., the equality of variables.

Example 3 (Imprecise knowledge computation). For Program 7 and its execution when h = true, our static analysis does not infer that, at the end of the loop y is equal to x. Hence, it fails at deducing that in the other branch y is 0.

Program 7 1 y = 1; x = N; 2 if h then skip; 3 else while x > 0 do x = x-1; y = x; 4 output y When h is true, we statically analyse the while-loop. The loop invariant is s = (•, κ ), where κ defines a knowledge for each variable. To model the fact that x is decremented at each iteration, the static analysis computes

κ (x) = 0≤n≤N λρ.n = λρ.
This information is propagated towards y by the assignment y = x and we get κ (y) = λρ. . At the end of the loop, the test ¬x > 0 i.e., x = 0 -providing x is a natural integer -allows to recover the fact that x is necessarily 0. However, as the equality between x and y is not propagated, the value of y cannot be recovered. As a result, the final knowledge in y is κ(y) = λρ.if (C h ρ , 1, ), while the real attacker knowledge is λρ.if (C h ρ , 1, 0). As a result of the imprecise knowledge computation, the static analysis is not always capable to detect the loop termination. If we have κ(x)(ρ) = ⊥, we know for certain that the program does not terminate for initial environment ρ. However, if κ(x)(ρ) = v for some v, there is no certainty. The program either terminates and the value is indeed v or the program does not terminate.

(y) = λρ.if (C h ρ , 1, ).
The static analysis of the while loop detects that the value of x in the loop body is always 1 and the knowledge in variable x is κ(x) = λρ.1. However, since the knowledge in y is not precise, the static analysis is unable to determine the non-termination of the loop.

V. Correctness and Soundness

Given a monitor's knowledge κ, a variable x and its value v, we can express the set of possible environments that can produce v as the inverse of κ: κ(x)

-1 (v). The Monitor Correctness Theorem 1 states that this set of environments intersected with the low-equivalence class [ρ i ] L is a correct approximation of the attacker knowledge for environment ρ i , as defined in Definition 1.

Theorem 1 (Monitor Correctness). Let c ∈ C, ρ, ρ ∈ Env, κ ∈ Var → K and assume that (c, init(ρ)) ⇓ (ρ , κ). Then for all v ∈ V, x ∈ Var and ρ i ∈ Env,

κ(x) -1 (v) ∩ [ρ i ] L ⊆ K(c; output x, v, ρ i ).
Proof sketch. The Correctness Theorem is a consequence of a more general, inductive invariant. It states that if we are given sound knowledge κ about a program c 0 executed in environment ρ then monitoring another program c with κ as initial knowledge will produce final knowledge κ which is sound for the sequential composition c 0 ; c when executed in environment ρ. To state this invariant, we define the predicate soundK which states that the knowledge κ ∈ Var → K is sound for an execution of program c in initial environment ρ i . Formally, we write soundK (c, ρ i , κ) if for all v ∈ V, x ∈ Var and ρ f ∈ Env,

ρ i ∈ κ(x) -1 (v) (c, ρ i ) ↓ ρ f ⇒ ρ f (x) = v.
The invariant can then be stated as follows:

(c, (ρ 0 , κ)) ⇓ (ρ 1 , κ ) soundK (c 0 , ρ, κ) ⇒ soundK (c 0 ; c, ρ, κ ).
The proof of this invariant is by structural induction over the relation ⇓ and by case analysis over the hybrid monitoring rules of Figure 3. Instantiating this invariant with c 0 = skip and κ = κ 0 , we get that (c, init(ρ)) ⇓ (ρ , κ) ⇒ ∀ρ i .soundK (c, ρ i , κ).

Theorem 1 then follows from the observation that all knowledge that is sound according to the predicate soundK is a subset of the attacker knowledge, as defined in Definition 1. Formally, if soundK(c, ρ, κ)) then

κ(x) -1 (v) ∩ [ρ] L ⊆ K(c; output x, v, ρ).
We complete the semantics of a hybrid monitor with an additional rule to deal with outputs, presented below. The output rule uses the NI (ρ, K, v) predicate that uses the knowledge K to check whether all low-equal initial environments would either produce the same value v or would not terminate (indicated by a value ⊥). In Section VII-D we describe how to efficiently implement the computation of predicate NI . This predicate is defined by

NI (ρ, K, v) = [ρ] L ⊆ K -1 (v) ∪ K -1 (⊥).
The rule for output is then given by:

outNI (c, init(ρ)) ⇓ (ρ , κ) ρ (x) = v NI (ρ, κ(x), v) (c; output x, ρ) ⇓ v
With this output rule, we have the property of a knowledge-based hybrid monitor that the monitor either accepts the output of a program, or blocks.

Lemma 2. If a knowledge-based hybrid monitor produces a value v for a program P from an initial environment ρ, then the original program P computes the same value:

(P, init(ρ)) ⇓ v ⇒ (P, ρ) ↓ v.
We can then prove (using Theorem 1) that the knowledge-based hybrid monitor completed with an output rule outNI enforces knowledge-based security.

Theorem 2 (Monitor Soundness). A program P , monitored by a knowledge-based hybrid monitor with output rule outNI, is TINI under the monitor semantics ⇓: whenever

ρ 1 L = ρ 2 L and (P, init(ρ 1 )) ⇓ v 1 and (P, init(ρ 2 )) ⇓ v 2 , then v 1 = v 2 .
Example 5 (Permissiveness). Program 6 of Example 2 demonstrates when our analysis is able to detect nontermination of the program. Our monitor computes the knowledge in variable l as κ(l) = λρ.if (C h ρ , 0, ⊥). Then, when a variable l is to be output, the outNI rule ensures that on all possible low-equal environments, either the program outputs 0 or does not terminate -the predicate NI holds.

Given that our monitor is sometimes able to model when the program does not terminate, it might be tempting to enforce termination-sensitive noninterference (TSNI). To achieve it, one could substitute the NI predicate with a TSNI predicate requiring that in all the low-equal memories either the program terminates producing v, or it does not terminate:

TSNI (ρ, K, v) = [ρ] L ⊆ K -1 (v) ∨ [ρ] L ⊆ K -1 (⊥).
The problem with this approach is that whenever κ(x)(ρ) = v, there is no certainty that the program terminates, since v approximates ⊥.

Example 6 (TSNI counterexample). The composed program from Example 4 is TINI but not TSNI since it terminates on h = true and does not terminate when h = false. The hybrid monitor computes the knowledge in x as κ(x) = λρ.1 that would satisfy TSNI predicate, however this would not be a sound enforcement of TSNI.

VI. Combination with other monitors

We now show how an existing dynamic monitor based on security levels can be combined with our knowledge-based hybrid monitor. The combined monitor will admit more executions than each of the monitors taken in separation, and will still be secure. To compare the precision of monitors, Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF] propose the notion of "permissiveness" that compares a set of program executions accepted by two monitors and defines a monitor to be more permissive if it accepts a strictly bigger set of executions.

Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF] observe that purely dynamic monitors (e.g., NSU [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF]) and simple hybrid monitors (e.g., Le Guernic et al. [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF]) are not necessarily comparable with respect to their permissiveness. For example, the execution of Program 1 in environment h = false is accepted by a dynamic monitor NSU because the test is false, but it is rejected by a hybrid monitor since the static analysis concludes that there might be a leak on the non-executed branch. On the other hand, NSU rejects an execution of Program 2 when h = true (because of a sensitive upgrade on line 1), while a hybrid monitor accepts it (because the security level of l is downgraded to L on line 2).

A. Hybrid monitor reusing an inlined monitor

We assume that a monitor based on security levels (for example, a purely dynamic monitor), is inlined in the program following the inlining technique simultaneously proposed by Chudnov and Naumann [START_REF] Chudnov | Information Flow Monitor Inlining[END_REF] and Russo and Sabelfeld [START_REF] Magazinius | On-the-fly inlining of dynamic security monitors[END_REF]. Here, a program c is transformed into a program c, where each variable x has a shadow variable x representing the security label of x. The monitoring is not intrusive in the sense that the values of x are the same for c and c. In other words, the computation of security levels has no impact on the computed values. We will present the instantiation to NSU in Section VI-B below.

Given a program P = c; output x, the monitor usually decides to output x if the label of x is lower or equal than the level L 4 . A hybrid monitor can choose to mimic the t-skip G, S skip skip

t-seq ∀i = 1..2.G, S c i c i G, S c 1 ; c 2 c 1 ; c 2 t-if S(x) = x y / ∈ dom(S) ∪ rng(S) ∧ y / ∈ G ∀i = 1..2.
( c, init(ρ)) ⇓ (ρ , κ) ρ (x) = v ρ ( x) L ( c; output x), ρ ⇓ v
This rule ensures that the inlined monitor only outputs a value v when the security level of the variable x is below L. We make one assumption about the inlined monitor viz., that it correctly computes the security labels of the variables that can be used to enforce noninterference.

Assumption 1 (Correct labels of inlined monitor). Consider a program P = c; output x. If it outputs a value v according to the following output rule:

outL ( c, ρ) ↓ ρ ρ (x) = v ρ ( x) L ( c; output x), ρ ↓ v
Then the label of variable x is computed correctly in the final environment ρ , meaning

K(P, v, ρ) = I(P, ρ).
As a consequence, a hybrid monitor only using the outL output rule soundly enforces noninterference.

To gain more precision, the hybrid monitor can first use its own knowledge about the output variable x (applying the rule outNI), and only if it is unable to prove noninterferfence, it can then try to apply the default output rule outL of the inlined monitor.

We can gain even more precision by reasoning about the knowledge contained in the shadow variables. This will allow the monitor to output certain values, even if neither the rule outNI nor the rule outL holds. The idea is to provide the knowledge-based monitor with the extra information that certain variables would never be output because the dynamic monitor would block them. Environments that lead to an output that is certain to be blocked by the dynamic monitor can be disregarded when computing the set of possible outcome of the program. Concretely, we add a new security level B ("will be blocked by the monitor"), such that H B. An additional output rule outH exploits this new label. It requires that:

• the value of x can be output (because ρ( x) B), and • all the environments that will not be blocked by a monitor, written NotB( K), and low-equal to ρ would produce the same value v. Formally, we get the following output rule outH that combines information computed by the hybrid monitor and the inlined dynamic monitor.

outH ( c, init(ρ)) ⇓ (ρ , κ) ρ (x) = v ρ ( x) L ρ ( x) B single(ρ, κ(x), κ( x), v) ( c; output x), ρ ⇓ v
The predicate single ensures that we only produce a single unique value. It exploits the new blocked level B and is defined as follows.

single(ρ, K, K, v) = ([ρ] L ∩ NotB( K)) ⊆ K -1 (v) NotB( K) = (Env\ K -1 (B)).
With this rule, the combination of the hybrid monitor and a dynamic monitor can be strictly more permissive than either of them.

B. Application to NSU

In the No-Sensitive Upgrade monitor (NSU) [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF], [START_REF] Zdancewic | Programming languages for information security[END_REF] an assignment to a variable is allowed only if the program counter level pc is lower than the level of the assigned variable l. Otherwise, the execution is stopped.

Figure 4 presents an inlining transformation for NSU. The inlining technique uses the transformation judgement G, S c c, where S : vars(c) → Var maps each variable of c into its shadow variable S(x) which contains the current security level of x; and G is a finite list of variables that store the current pc. S e e means that e is an expression for the level join of shadow variables of the variables in e (see [START_REF] Chudnov | Information Flow Monitor Inlining[END_REF]Fig. 9]).

NSU enforces termination-insensitive noninterference [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF], so the proposed transformation indeed satisfies Assumption 1. The only difference in our presentation of inlining is that we do not write an explicit divergence operation (such as while (true) skip), but rather assign the highest security level B to all the variables (see t-assign rule); and still allow the computation x := e.

The following short example demonstrates in a concise manner how the knowledge-based hybrid monitor that reuses NSU is more permissive than NSU.

Program 9 1 l = 1; if h then l = 0; 2 output h Example 7.
All the executions of Program 9 are blocked by NSU since the program tries to output a high variable h on a low channel. However our knowledge-based hybrid monitor combined with NSU accepts its execution when h = false. Following the idea of NSU, the monitor transforms an information channel into a termination channel. When h = false, the hybrid monitor is able to compute that the other initial environment ρ , where h = true will get a B label (κ( h)(ρ ) = B) and therefore will not be output (unless the rule outNI holds). Therefore, the output is accepted by the outH rule because the single predicate ensures that all the executions not blocked by the monitor (where h = false) will compute the same value.

C. Soundness and Permissiveness

We now prove the main soundness result for the hybrid monitor that executes a program with an inlined security monitor. In the following, we write HM (Output) for our hybrid monitor using a set of output rules Output ⊆ {outNI, outL, outH}. Theorem 3. All the executions of a program P = ( c; output x), monitored by a knowledge-based hybrid monitor HM ({outNI, outL, outH}) are secure for all environments ρ.

Remark that a hybrid monitor using a smaller set of output rules is also sound. This fact will be useful to prove the relative precision of hybrid monitors.

A monitor A is more permissive than a monitor B if it stops less monitored executions (suppresses less outputs). Following Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF], a productive environment for a monitor M and a program P , written E M (P ) is a set of environments for which the monitor does not stop, i.e., E M (P ) = {ρ | ∃v.(P, ρ) ⇓ M v}. Thus, E M is a family of productive sets indexed by programs for the monitor M . Definition 6. A monitor A is at least as permissive as a monitor

B if E B ⊆ E A .
Theorem 4 (Hierarchy of hybrid monitors). Consider a program P = c; output x and a program P = c; output x that is instrumented by a sound dynamic monitor for noninterference. The following precision results hold:

E HM({outNI}) (P ) = E HM({outNI}) ( P ) E HM({outNI}) ( P ) ⊆ E HM({outNI,outL}) ( P ) E HM({outL}) ( P )
⊆ E HM({outNI,outL}) ( P ) E HM({outNI,outL}) ( P ) ⊆ E HM({outNI,outL,outH}) ( P ) Theorem 4 shows that the combination of our hybrid monitor with a dynamic monitor is more precise than each of them taken separately. Moreover, as the output rule outH requires a cooperation between both, our best hybrid monitor HM ({outNI, outL, outH}) is more precise than a direct parallel composition of both, which can be obtained as HM ({outNI, outL}).

Example 8. Consider again a Program 9. When h = false, the knowledge-based hybrid monitor (E HM({outNI}) ) is not able to prove noninterference and the level of h is H, and hence the output is blocked. However, the more precise monitor E HM({outNI, outL, outH}) ensures that h is output since the single predicate ensures that the monitor always produces the same output.

VII. Implementation

The knowledge-based hybrid monitor has been implemented and proved correct [START_REF]Formalisation of the Hybrid Monitor in Coq[END_REF] using the Coq proof assistant. Here, we describe the main data structures and algorithms used for computing knowledge.

Knowledge about initial environments is formalized using knowledge functions K ∈ K. One algorithmic challenge is to find an efficient algorithm for extracting the knowledge from such a function K i.e. computing K -1 (v) for some v. We present a concrete representation for a class of knowledge functions that is closed under all the operations needed by the hybrid monitor. With this representation, a logical formula representing the knowledge of an output v is computed in linear time.

A. Concrete domain of knowledge functions

The domain of the monitor K = Env → V is encoded with the symbolic domain K ⊂ P(F × E) × F where E is the set of program expressions and F is the following set of boolean formulae:

F φ ::= φ ∧ φ | φ ∨ φ | ¬φ | e | tt | ff (here e ∈ E

is a program expression seen as a boolean, see Section III-A).

A pair (f, e) ∈ F × E denotes a knowledge which returns the value of the expression e when the formula f holds in the initial environment and otherwise. The last element φ ∈ F of K specifies when the knowledge is ⊥. Given an element K = (S, φ) ∈ K , we write K S for the set of pairs S and K φ for the formula φ. The denotation of K ∈ K in the knowledge domain K is then obtained by:

{|K|} = ( (f,e)∈K S f → e) K φ → ⊥ where ψ → e = λρ.if ψ ρ then e ρ else true[K] = (f,e)∈K S (f ∧ e) false[K] = (f,e)∈K S (f ∧ ē) top[K] = ¬(true[K] ∨ false[K] ∨ K φ ) K@ψ = ({(ψ ∧ f, e) | (f, e) ∈ K S }, K φ ∨ ¬ψ) K 1 K 2 = (K = ∪ K 12 ∪ K 21 , K φ 1 ∧ K φ 2 )
, where

K = = (f 1 ∧ f 2 ∧ e 1 = e 2 , e 1 ) (f 1 , e 1 ) ∈ K S 1 (f 2 , e 2 ) ∈ K S 2 K ij = {(f i ∧ K φ j , e i ) | (f i , e i ) ∈ K S i }
Fig. 5: Implementation of the conditional operator.

Our domain K also requires well-formedness conditions. Given (S, φ) ∈ K , we add the constraint that any two pairs (f, e) and (f , e ) from S must satisfy that if both f and f hold then the expressions e and e evaluate to the same value. Moreover, for any (f, e) ∈ S, the conjunction of f and φ does not hold. All the operators needed by the hybrid monitor preserve this property.

Example 9. We illustrate below the symbolic encoding of basic knowledge functions.

{|(∅, ff )|} = λρ. {|(∅, tt)|} = λρ.⊥ {|{(true, n)}, ff )|} = λρ.n
For Program 3, we get the following knowledge in l in the end of the program:

({(h, 1); (¬h, x); (x = 1, x)}, ff )
The knowledge is well-formed since if any two formulae among h, ¬h or x = 1 hold at the same time, the corresponding expressions evaluate to the same value.

B. Implementation of operators

The assignment rules assinDyn and assignStat compute the knowledge of an expression using a function _ κ . We show how to implement this function for a new domain of knowledge K below:

x κ = κ(x) n κ = ({(tt, n)}, ff ) k 1 ⊕ k 2 κ = (S, k 1 φ κ ∨ k 2 φ κ ) where S = (f 1 ∧ f 2 , e 1 ⊕ e 2 ) (f 1 , e 1 ) ∈ k 1 S κ (f 2 , e 2 ) ∈ k 2 S κ
One key operator is the conditional operator IF which combines the knowledge from different execution paths. The IF and assume operators can be rewritten using more basic operators, defined in Figure 5:

Assume(c, l) = l@true[c] l@top[c] IF (c, l, r) = l@true[c] r@f alse[c] (l r)@top[c]

C. Static analysis of loops

The only place where the specification of the hybrid monitor is not directly executable is the rule WhileStat. The implementation of this rule requires an iterative fixpoint computation in order to infer an invariant of the loop body. The domain K does not satisfy the finite ascending chain condition. Therefore, a widening operator is needed to ensure convergence and speed up computations. Our widening limits the number of distinct expressions which can occur in formulae. To remove an expression e from a formula f , we compute the formula f + ∧ f -where f + is obtained by substituting e for tt and f -is obtained by substituting e for ff . The obtained formula is by construction stronger which ensures the soundness of the transformation. Remember that (f → e) returns when f does not hold. By bounding the number of expressions to some fixed constant k, and because formulae have a normal, our fixpoint iteration operates over a finite domain of boolean formulae. This ensures convergence.

D. Effective proof of non-interference

To get an effective enforcement and implement the rules outNI and outH, we need a decision procedure for the predicates NI and single. These predicates can be encoded as logic formulae f ∈ F. To get a decidable enforcement, the logic needs to be decidable. As propositional logic is decidable, the decidability depends only on the language of expressions E. It will hold, for instance, for decidable fragment of arithmetic such as linear integer arithmetics or bit-vector arithmetics.

The logic translation is syntax-directed and defined by the function • :

K -1 (v) = (f,e)∈K S f ∧ e = v K -1 (⊥) = K φ [ρ] L = {x|Γ(x) L} x = ρ(x)
The inverse function K -1 (v) represents the knowledge of the output v. Given the output value v and a symbolic knowledge K ∈ K , K -1 (v) builds a disjunction where all the expressions are constrained to be equal to v. The equivalence class [ρ] L of a initial environment ρ is obtained by a conjunction of equality constraints stating that a low variable x, should have the value of ρ(x). Set operations ∪, ∩ and \ have a standard encoding and set inclusion can be done by checking entailment. Theorem 6 states that the security predicates NI and single can be checked by checking that their logic encoding is a tautology. Theorem 6. The logic translation of security predicates is sound and complete.

NI (ρ, K , v) iff [ρ] L ⇒ K -1 (v) ∨ K -1 (⊥) single(ρ, K, K, v) iff [ρ] L ∧ NotB( K) ⇒ K -1 (v)

E. Experiments

From our Coq development, we have extracted an Ocaml proof-of-concept implementation [START_REF]Formalisation of the Hybrid Monitor in Coq[END_REF]. We have extracted five programs from this paper and used our implementation to compute the approximated knowledge. These programs were selected to demonstrate the difference in monitors with respect to the attacker knowledge approximation and permissiveness. For these five programs, we provide the actual knowledge gained by an attacker by observing an output and the approximation computed by different monitors, including the best hybrid monitor of Besson et al. [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF], called HM(Val+Comb). For enforcement of noninterference, we compare the permissiveness of a knowledge-based hybrid monitor HM (Section IV), the standard NSU and their combination (Section VI).

For each program, we analyse an execution for a given initial environment presented in column 2 of Figure 6a. The actual knowledge of the attacker is a formula over the high variables, that we present in column K(P i , v, ρ). For columns HM(Val+Comb) and HM, we highlight in light grey the knowledge that was not computed precisely.

For the majority of programs the hybrid monitor HM is able to compute the exact knowledge of the attacker. Only for Program P 7 , our monitor approximates the knowledge of the attacker due to the its static analysis limitation. For Programs P 4 and P 5 , our hybrid monitor is strictly more precise than the hybrid monitor of Besson et al.

Figure 6b gives an insight into permissiveness of the monitors, where HM stands for HM ({outNI}), NSU stands for HM ({outL}) and HM+NSU stands for HM ({outNI, outL, outH}). Given a program execution described in the second column of Figure 6a, we write a if the value is output and a if the monitor blocks the execution. All the presented program executions are rejected by NSU except for P 1 and P 7 . The execution of P 5 is proved noninterferent by the hybrid monitor HM, while rejected by NSU. Program P 9 illustrates the case where neither HM nor NSU alone is able to ensure termination-insensitive noninterference whereas their combination HM+NSU does. As explained in Section VI-B, the key insight is to exploit the knowledge that other interfering executions would be blocked.

VIII. Discussion 1) Scalability:

The formal development and implementation of our hybrid monitor are given for a minimalist imperative language. A relevant question is whether our core monitor could be efficiently implemented for a fullfledged language. Core dynamic monitors have already been adapted to very dynamic languages. For instance, the JSFlow project [START_REF] Hedin | JSFlow: tracking information flow in javascript and its apis[END_REF] implements a dynamic information flow monitor for JavaScript. Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF] also proposed a hybrid monitor that covers a large subset of JavaScript. For hybrid monitors, the main challenge is to mitigate the overhead incurred by the static analysis. Note that it is always possible to trade precision for efficiency -for instance by making an aggressive use of widening operators (see Section VII-C). At the extreme, static analysis can even be momentarily switched off if it is deemed too costly or unfeasible. In that case, the computed knowledge for the non-executed branch would be λρ. i.e. the absence of knowledge which is sound but imprecise. Regarding functions, a reasonable trade-off could be to limit the static analysis to the current function boundaries i.e intra-procedural analysis. Yet, getting the desired trade-off between precision and efficiency requires more investigation.

2) Extension to programs with I/O and strategies: The proposed approach can be extended to programs with I/O and strategies [START_REF] Chong | Required information release[END_REF]. We could define a special global variable that contains all the knowledge of the previous outputs and each new input would immediately contain that knowledge. Like this, we could track the knowledge that would be an upper bound for any possible strategy. The current representation would not change in this case.

IX. Related work

Zdancewic [START_REF] Zdancewic | Programming languages for information security[END_REF] proposed the no-sensitive-upgrade principle for dynamic information flow control that halts execution if a program assigns to low variables under secret control. Austin and Flanagan [START_REF] Austin | Efficient purely-dynamic information flow analysis[END_REF], [START_REF] Austin | Permissive dynamic information flow analysis[END_REF] extended this to permissive upgrade which takes the future use of the assigned variable into account before halting the execution. Hybrid monitors for information flow control combine static and dynamic program analysis [START_REF] Guernic | Precise Dynamic Verification of Confidentiality[END_REF], [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF], [START_REF] Moore | Static analysis for efficient hybrid information-flow control[END_REF], [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF]. One of the first techniques was proposed by Le Guernic et al. [START_REF] Le Guernic | Automata-based Confidentiality Monitoring[END_REF] where the static analysis only performs syntactic checks on non-executed branches. Russo and Sabelfeld [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF] introduced a generic framework of hybrid monitors, where nonexecuted branches are analysed syntactically and formally proved that the permissiveness of such monitors is incomparable with the purely dynamic monitors. In a follow-up work, Le Guernic [START_REF] Guernic | Precise Dynamic Verification of Confidentiality[END_REF] presented a more permissive static analysis, that ignores possible branches that depend only on public variables. Besson et al. [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF] enhance a dynamic monitor with static constant propagation and dependency analysis, and show how this leads to a hierarchy of increasingly more permissive hybrid monitors. Their knowledge is represented by the domain F×V. As explained in Section I, the present work improves permissiveness of the hybrid monitor from [START_REF] Besson | Hybrid information flow monitoring against web tracking[END_REF]: 1) we have a strictly more expressive domain: an element (f, v) ∈ F × V is exactly modelled in our domain by the knowledge ({(f, v)}, ff ); 2) we have the advantage of capturing certain forms of non-termination. With respect to dynamic monitors, permissiveness of the proposed monitor is incomparable (see Fig. 6b), however it has the power to achieve a strictly higher level of permissiveness by combination with the dynamic monitors.

Chudnov et al. [START_REF] Chudnov | Information flow monitoring as abstract interpretation for relational logic[END_REF] propose a hybrid monitor for relational logic. An interesting feature of the work is that the monitor is obtained from a constructive soundness proof. In this work, we consider a specific property (namely termination insensitive non-interference). Yet, our knowledge analysis is not geared to noninterference and could help discharging more general assertions of relational logic. In a recent paper, Hedin et al. [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF] extend a dynamic information flow monitor for core JavaScript with a static points-to analysis that can approximate the potential write targets in regions with a high security context. The dynamic monitor is based on NSU and prevents implicit flows by forbidding all side effects with targets that are below the security context. The static analysis is used to raise the security labels of the potential write targets to the level of the context before entering this context. This prevents the monitor from stopping when writing to a low target. Interestingly, the static analysis need not be sound or complete, as the dynamic monitor ensures that the hybrid monitor is sound. Precision only affects the permissiveness of the monitor. Their hybrid monitor is more precise than a static information flow analysis such as that of Hunt and Sands [START_REF] Hunt | On flow-sensitive security types[END_REF]. However, they also make the observation that "with the above definition of relative permissiveness, a hybrid monitor cannot subsume a purely dynamic monitor" [START_REF] Hedin | Value-sensitive Hybrid Information Flow Control for a JavaScript-like Language[END_REF]Thm. 3]. This is not contradictory with our findings because they only consider a particular static analysis. We conjecture that their "NSU + pointsto" monitor can benefit from our extension with knowledge computation in order to obtain a monitor that subsumes their dynamic monitor.

The notion of attacker knowledge was first proposed by Askarov and Sabelfeld [START_REF] Askarov | Gradual release: Unifying declassification, encryption and key release policies[END_REF] and then used by Askarov and Chong [START_REF] Askarov | Learning is change in knowledge: Knowledge-based security for dynamic policies[END_REF] to study enforcement of noninterference when the security policy changes over time, and for different kind of attackers. The notion of knowledge here is used to state the security conditions but the enforcement mechanism does not compute the knowledge explicitly.

In the area of purely static information flow analysis, Hunt ans Sands [START_REF] Hunt | On flow-sensitive security types[END_REF] proposed a flow-sensitive type system for non-interference that was later proven to be less permissive than a standard hybrid monitor [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF]Thm. 3]. Müller et al. [START_REF] Müller | An analysis of Universal Information Flow based on Self-composition[END_REF] generalize the type system of Hunt and Sands using the technique of self-composition. They define an abstract weakest precondition calculus for selfcomposed program that computes logical formulae describing dependencies and equalities between variables.

X. Conclusions

We propose a hybrid monitor to compute the knowledge that an attacker obtains by observing a program output. The monitor is hybrid since it statically analyses non-executed branches. Our symbolic representation of attacker knowledge is powerful and subsumes existing hybrid monitoring approaches. We show that a knowledge-based monitor can be combined with any dynamic monitor for noninterference resulting in an enforcement mechanism that is more permissive than each mechanism taken separately. Therefore, our monitor is able to reach a level of permissiveness that was deemed impossible for the previous hybrid monitors [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF].

In this paper we have laid the foundations for designing knowledge-based hybrid monitors. There are several ways in which this work can be further expanded.

The language studied here is voluntarily kept minimalistic and there is interesting semantic questions linked to how to monitor knowledge for more advanced programming languages with features such as objects, arrays and higher-order functions.

Our monitor statically analyses non-executed branches and the theory explains how this integration is designed. However, the current development can go much further and integrate traditional static analyses. In particular, more precise numeric analyses, ranging from constant propagation to polyhedral analysis, would allow the monitor to prove more equalities between variables and, hence, improve permissiveness. Other analyses such as pointsto analysis would be required for the extension to the language features mentioned above.

Program 4 1

 1 x = 0; y = 0; 2 if (h1) then y = 1; 3 if (h2) then x = 1 else x = y; 4 output x When Program 4 outputs 1, the attacker learns that either h1 or h2 was true: Attacker knowledge: h1 ∨ h2

Fig. 3 :

 3 Fig. 3: Hybrid knowledge analysis semantics.

  Said otherwise, any non-terminating execution from initial environment ρ can soundly approximated by κ(x)(ρ) = v.Example 4 (Non-detection of loop non-termination).Consider the program obtained as the sequential composition of Program 7 followed by Program 8. This new composed program is noninterferent (TINI) since it either outputs 1 or does not terminate. Program 8 1 x = 1; 2 while y = 0 do x = 1; 3 output x After an execution of the Program 7 in the initial environment where h = true, the computed knowledge in variable y is κ

Fig. 4 :

 4 Fig. 4: NSU inlining transformation

Theorem 5 .

 5 The operators over K exactly model the operators over K. In particular, we have {| e κ |} = e λx.{|κ(x)|} {|K 1 K 2 |} = {|K 1 |} {|K 2 |} {|IF (c, e 1 , e 2 )|} = IF ({|c|}, {|e 1 |}, {|e 2 |})

Fig. 6 :

 6 Fig. 6: Experimental results

In all examples, variables with names starting with "h" are secret, and all the other variables are public.

Notice that the permissiveness result with respect to static analysis is achieved by transitivity of permissiveness: a knowledge-based hybrid monitor is provably more permissive than a standard hybrid monitor, and a standard hybrid monitor is more permissive than a static analysis of Hunt and Sands[START_REF] Hunt | On flow-sensitive security types[END_REF] (see Thm

. 3 of[START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF]).

Usually, this condition is pc Γ(x) L, however the program counter pc is at the lowest level L because our programs only produce output outside conditionals and while-loops.

Acknowledgement

This research has been partially supported by the French ANR projects AJACS ANR-14-CE28-0008 and ANR-10-LABX-07-01 Laboratoire d'excellence Comin-Labs.


Wafa Bouaziz

Johanna Sigaux

Dominique Modrowski

Claire-Sophie Devignes

Thomas Funck-Brentano

Pascal Richette

Hang-Korng Ea

Sylvain Provot

Martine Cohen-Solal
email: martine.cohen-solal@inserm.fr

Eric Haÿ

Martine Cohen- Solal

Eric Hay

Martine Pr

Cohen-Solal

Interaction of HIF1α and β-catenin inhibits matrix metalloproteinase 13 expression and prevents cartilage damage in mice

Keywords: Hypoxia-Inducible factor 1α, β-catenin, matrix metalloproteinase 13, cartilage, osteoarthritis, chondrocyte

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

\Body

Introduction

Low oxygen tension (hypoxia) orchestrates several cell functions and is critical in health and disease [START_REF] Maes | Hypoxia-driven pathways in bone development, regeneration and disease[END_REF][START_REF] Maes | VEGF-independent cell-autonomous functions of HIF-1alpha regulating oxygen consumption in fetal cartilage are critical for chondrocyte survival[END_REF][START_REF] Semenza | HIF-1 mediates metabolic responses to intratumoral hypoxia and oncogenic mutations[END_REF][START_REF] Gezer | Concise review: genetic dissection of hypoxia signaling pathways in normal and leukemic stem cells[END_REF]. Hypoxia-inducible factor 1α (HIF1α) is an essential factor to maintain chondrocyte homeostasis and allow cell differentiation [START_REF] Gelse | Role of hypoxia-inducible factor 1 alpha in the integrity of articular cartilage in murine knee joints[END_REF][START_REF] Dunwoodie | The role of hypoxia in development of the Mammalian embryo[END_REF]. HIF1 is a heterodimeric DNA-binding complex containing a constitutive HIF1β subunit and HIF1α subunit. In hypoxia, HIF1 binds to the hypoxia response elements of target genes, whereas in normoxia, HIF1α is hydroxylated, thereby leading to its degradation. Indeed, HIF1α hydroxylation is recognised by the von Hippel-Lindau tumor suppressor protein (pVHL), an E3 ubiquitin ligase that targets HIFα for proteolysis in the proteasome [START_REF] Weidemann | Biology of HIF-1alpha[END_REF]. The HIF1α pathway interacts with different cell signaling pathways, among them Wnt signaling. Indeed, HIF1α interacts with β-catenin in regulating cell growth and survival. In embryonic stem cells, HIF1α-β-catenin complexes upregulate lymphoid enhancerbinding factor 1 and transcription factor 1 (TCF1), which activates Wnt signaling [START_REF] Mazumdar | O2 regulates stem cells through Wnt/beta-catenin signalling[END_REF], whereas in colorectal cancer cells, HIF1α blocks the TCF4-β-catenin interaction and transcriptional activity, thus inhibiting canonical Wnt signaling [START_REF] Kaidi | Interaction between beta-catenin and HIF-1 promotes cellular adaptation to hypoxia[END_REF].

Cartilage loss characterizes osteoarthritis (OA), one of the most frequent joint disorders, but available treatments are poorly efficient to prevent joint destruction [START_REF] Arden | Osteoarthritis: epidemiology[END_REF][START_REF] Murray | Disability-adjusted life years (DALYs) for 291 diseases and injuries in 21 regions, 1990-2010: a systematic analysis for the Global Burden of Disease Study 2010[END_REF]. Therefore, the need for novel drug targets to treat OA is paramount. Matrix metalloproteinase 13 (MMP13) triggers the degradation of articular cartilage. Indeed, chondrocyte-specific deletion of MMP13 alleviated OA in mice; the Wnt family members were candidates for the regulation of MMP13 expression in chondrocytes because its expression was increased in chondrocytes from mice with conditional activation of β-catenin [START_REF] Wang | Recent progress in understanding molecular mechanisms of cartilage degeneration during osteoarthritis[END_REF]. Cumulative data showed that Wnt activity is low under physiological conditions, and activation of Wnt signalling contributes to cartilage breakdown in OA [START_REF] Zhu | Activation of beta-catenin signaling in articular chondrocytes leads to osteoarthritis-like phenotype in adult beta-catenin conditional activation mice[END_REF][START_REF] Funck-Brentano | Dkk-1-mediated inhibition of Wnt signaling in bone ameliorates osteoarthritis in mice[END_REF]. The modulation of Wnt inhibitors had significant effects on chondrocyte catabolism of mice. Indeed, loss of sclerostin enhanced cartilage degradation [START_REF] Bouaziz | Loss of sclerostin promotes osteoarthritis in mice via betacatenin-dependent and -independent Wnt pathways[END_REF] and the overexpression of Dkk-1 alleviated OA [START_REF] Funck-Brentano | Dkk-1-mediated inhibition of Wnt signaling in bone ameliorates osteoarthritis in mice[END_REF]. Despite the hypoxic status of cartilage [START_REF] Yuasa | Wnt/beta-catenin signaling stimulates matrix catabolic genes and activity in articular chondrocytes: its possible role in joint degeneration[END_REF], the involvement of hypoxia in regulating Wnt signalling and MMP13 expression in cartilage is still unclear.

We studied the role of HIF1α in regulating Wnt signaling in cartilage of mice with conditional knockout of HIF1α (∆HIF1α chon ) and induced OA. Hypoxia maintained low Wnt/β-catenin signaling via HIF1α, which lowered MMP13 expression, then prevented chondrocyte catabolism and cartilage loss. We here therefore highlight the role of HIF1α in cartilage remodeling and loss during OA and provide a novel mechanism of microenvironmental regulation of Wnt signaling.

Results

HIF1α deletion in chondrocytes enhanced OA development and MMP13 expression in mice.

Articular chondrocytes are physiologically in a hypoxic state that might be altered in OA [START_REF] Gelse | Role of hypoxia-inducible factor 1 alpha in the integrity of articular cartilage in murine knee joints[END_REF]. To monitor oxygen tensions in OA chondrocytes, we administered a hypoxyprobe (pimonidazole hydrochloride) to control and OA mice. Hypoxia levels were markedly decreased in all layers of the OA articular cartilage, as shown by immunohistochemistry and by the decreased number of hypoxic cells (Fig. 1A). HIF1α was expressed in undamaged articular cartilage at baseline but its level decreased significantly in OA joints along with the increased cartilage damage (Fig. 1B).

Noteworthy, the number of Hif1 expressing cells was steadily downregulated after destabilization of the medial meniscus (4 and 6 weeks) whereas OA damage increased in a time dependent manner.

To determine the role of HIF1α in OA development, we generated mice with inducible conditional knockout of HIF1α by mating COL2-Cre ERT mice with HIF1α fl/fl mice in which the recombination was induced by tamoxifen. We first verified that the Cre-lox recombination occurred correctly in cartilage; COL2-Cre ERT ; R26R and R26R mice were injected with tamoxifen as controls. β-galactosidase was expressed in the articular cartilage of COL2-Cre ERT ;R26R mice, thus tamoxifen induced Cre-lox recombination in chondrocytes (Supplementary Fig. S1). OA was induced in ∆HIF1α Chon mice 1 week after tamoxifen injections. OA cartilage lesions were increased in ∆HIF1α Chon mice as showed by the OARSI score (Fig. 1C). As HIF1α is a survival factor, we assessed chondrocyte apoptosis in OA in the absence of HIF1α. The number of apoptotic cells was increased in ∆HIF1α Chon mice although the OA score remained unchanged (Fig. 1D). TUNEL positive cells were further increased in ∆HIF1α Chon mice with DMM. As previously described, the expression of MMP13 was induced in OA mice. This increase is enhanced in ∆HIF1α Chon mice along with the exacerbated cartilage loss (Fig. 1E). Thus, OA is associated with loss of hypoxia in articular cartilage, decreased HIF1α protein levels and increased MMP13 expression and cartilage loss in mice. To rule out the hypothesis that ∆HIF1α Chon could induce EPAS-1 (Hif2α) expression and therefore contribute to the phenotype, we found that EPAS-1 was expressed at the same level in HIF1α fl/fl mice and ∆HIF1α Chon mice suggesting the absence of compensatory increase of EPAS1 (Figure S2A).

HIF1α inhibits MMP13 expression and the transcription of Wnt targets.

HIF1α is a major HIF that regulates chondrocyte metabolism [START_REF] Wu | Insights on biology and pathology of HIF-1alpha/-2alpha, TGFbeta/BMP, Wnt/beta-catenin, and NF-kappaB pathways in osteoarthritis[END_REF]. We first assessed the role of hypoxia in the metabolic effects of Wnt signaling in primary chondrocytes. As expected in normoxia, Wnt3a reduced proteoglycan release and Col2A expression while increasing Mmp13 expression (Fig. 2A and 2B). In contrast, under hypoxic conditions, Wnt3a failed to modulate the proteoglycan release as well as the expression of catabolic markers. Furthermore target genes such as Axin and Wisp1 were not regulated by Wnt3a in hypoxia (Fig 2C). To investigate whether HIF1α modulate MMP13 expression induced by Wnt, we first deleted HIF1α chondrocytes and analyzed the expression of MMP13 and Wnt target genes under Wnt stimulation. Using siRNA silencing, there was no effect of HIF1α knock-down in COL2A and Mmp13 in normoxia (Fig. 2D). Furthermore, HIF1α knockdown has no effect on the nuclear translocation of EPAS1 (Fig. S2B).

Loss of HIF1α promoted the Wnt-induced Mmp13 expression and the transcriptional Wnt targets (Fig 2E) and confirmed by Cre-Lox recombination (fig. 2F and2G). This was not observed when EPAS1 was knocked-down (Fig. S2C).

To confirm that HIF1α inhibits MMP13 expression by blocking transcription of Wnt targets, we stabilized HIF1α in normoxic chondrocytes upon VHL deletion using Cre-Lox recombination.

HIF1α increase with VHL deletion was confirmed by Western blot analysis (Fig. 2H) and led to increased MMP1,3 Axin, and Wisp1 expression in normoxia (Fig. 2I). Moreover, stabilization of HIF1α did not affect the transcription of the anabolic marker COL2A1 (Fig. 2I). Thus the regulation of anabolic markers is independent of the HIF1α pathway. Because loss of VHL stabilizes both HIF1 and Epas1, we used an overexpression of constitutive stabilized HIF1 in chondrocytes [START_REF] Yan | The hypoxia-inducible factor 2alpha N-terminal and C-terminal transactivation domains cooperate to promote renal tumorigenesis in vivo[END_REF]. We found that HIF1α abolished Mmp13 expression induced by Wnt (Fig. 2J).

Thus, HIF1α alone is able to inhibit Wnt-induced MMP13 expression.

HIF1α-β-catenin interaction reduced TCF4 binding to the MMP13 regulatory region. Upon

Wnt pathway activation, β-catenin accumulates in the cytoplasm, translocates into the nucleus, binds to TCF transcription factor and activates the transcription of target genes [START_REF] Clevers | Wnt/beta-catenin signaling and disease[END_REF]. Wnt activation increases the levels of catabolic markers under normoxia [START_REF] Yuasa | Wnt/beta-catenin signaling stimulates matrix catabolic genes and activity in articular chondrocytes: its possible role in joint degeneration[END_REF]. We then investigated whether the translocation of β-catenin is reduced in hypoxia. Wnt3a promoted β-catenin translocation into the nucleus and its protein expression regardless of O 2 level (Fig. 3A, Fig. 3B).

Thus, hypoxia reduced transcriptional activity of β-catenin independently of nuclear β-catenin translocation.

We investigated whether HIF1α inhibits Wnt activity by direct interaction between HIF1α and βcatenin. In hypoxia, HIF1α and β-catenin co-localized in the nucleus of Wnt3a-induced chondrocytes (fig 4A), suggesting a possible interaction within nuclear complexes. Indeed, coimmunoprecipitation in nuclear extracts assay revealed HIF1α-β-catenin interaction complexes in hypoxia (Fig. 4B). However, EPAS1 failed to co-immunoprecipitate with β-catenin in normoxia and hypoxia (Fig. S2D). We next assessed the impact of HIF1α-β-catenin interaction on the transcriptional activity of TCF4-β-catenin complexes. In chondrocyte stimulated by Wnt3a, the formation of TCF4-β-catenin nuclear complexes was decreased in hypoxia compared to normoxia (Fig. 4B). These data suggest that under hypoxia, β-catenin may bind preferentially to HIF1α rather than TCF4, thus reducing Wnt/β-catenin signaling.

MMP13 is targeted by both HIF and Wnt signaling [START_REF] Leeman | The structure, regulation, and function of human matrix metalloproteinase-13[END_REF][START_REF] Leeman | Matrix metalloproteinase 13 activity is associated with poor prognosis in colorectal cancer[END_REF][START_REF] Saito | Transcriptional regulation of endochondral ossification by HIF-2alpha during skeletal growth and osteoarthritis development[END_REF][START_REF] Saito | HIF-2alpha as a possible therapeutic target of osteoarthritis[END_REF][START_REF] Yun | Transcriptional regulation of MMP13 by Lef1 in chondrocytes[END_REF]. To better characterize the role of HIF1α-β-catenin interaction in inhibiting Wnt/β-catenin signaling and MMP13 expression under hypoxia, we assessed TCF4 binding to the MMP13 regulatory region by CHIP assay (Fig. 4C). We used a MMP13 regulatory 3' region downstream of coding area that includes Wnt responsive elements (WREs) (24) (Fig. 4C). TCF4 binding to WREs was decreased in hypoxia compared to normoxia (Fig. 4C). To confirm the role of HIF1α in inhibiting TCF4 binding to WREs, we overexpress the stabilized form of HIF1α in normoxic chondrocytes and found that TCF4 binding to WREs was abolished (Fig. 4C). Therefore, TCF4 binding to the MMP13 regulatory region was reduced by HIF1α. We further investigated the transcriptional activity of MMP13 under hypoxia.

The regulatory region was cloned downstream of a luciferase reporter gene and the plasmid was transfected in C3H10 cells. This assay revealed downregulation of Wnt3a-induced luciferase activity when cultured under hypoxia (Fig. 4D), and confirmed the functional regulation of this sequence by hypoxia and Wnt3a.

PKF118-310 reduced OA progression in ∆HIF1α

Chon mice. Given the sequestration of β-catenin by HIF1α, we hypothesized that HIF1α deletion may increase TCF4-β-catenin complex level, thereby leading to chondrocyte catabolism. To verify this hypothesis, we deleted HIF1α in chondrocytes by siRNA silencing and blocked TCF4-β-catenin complexes by using PKF118-310 which blocks the interaction between TCF4 and β-catenin. In normoxia, PKF118-310 totally suppressed Wnt-induced Mmp13 and target genes expression (Fig. 4E). Loss of HIF1α increased the expression of MMP13 and that of the bona fide Wnt target genes Axin and Wisp1. Hence, the PKF118-310 addition inhibited the increased expression of the canonical Wnt targets MMP13, Axin and Wisp1 induced by loss of HIF1α. Thus, HIF1α prevented Wnt to induce MMP13 expression by blocking TCF4-β-catenin complexes.

In OA mice, conditional loss of HIF1α increased MMP13 expression and cartilage lesions (Fig. 5A). Increased TCF4-β-catenin complex level may promote the phenotype observed in ∆HIF1α Chon mice. Articular injection of the β-catenin inhibitor PKF118-310 in ∆HIF1α Chon mice prevented cartilage lesions and reduced MMP-13 expression as compared with PBS treatment. Thus, PKF118-310 administration in ∆HIF1α Chon mice blocked the increased MMP13 expression and cartilage damage (Fig. 5A and5B). Moreover, PKF118-310 resulted in a reduced number of apoptotic cells in OA mice (Fig. 5C). Loss of HIF1α enhanced cartilage damage by increasing TCF4-β-catenin complexes, which activated MMP13 expression.

Discussion

Hypoxia is a characteristic of physiological articular cartilage [START_REF] Gelse | Role of hypoxia-inducible factor 1 alpha in the integrity of articular cartilage in murine knee joints[END_REF][START_REF] Thoms | Hypoxia promotes the production and inhibits the destruction of human articular cartilage[END_REF]. We addressed the specific function of HIF1α in chondrocytes and in OA in mice. With inducible conditional knockout of HIF1α in mice, we showed that HIF1α alleviated OA development by downregulating MMP13 through inhibition of β-catenin transcriptional activity in chondrocytes. The hypoxic avascular nature of the articular cartilage maintains the chondrocyte phenotype and homeostasis. Indeed, we observed that hypoxia and HIF1α were downregulated in OA cartilage. Our findings are consistent with lower chondrocyte hypertrophy during hypoxia, which may contribute to the maintenance of cartilage homeostasis [START_REF] Leijten | Hypoxia inhibits hypertrophic differentiation and endochondral ossification in explanted tibiae[END_REF][START_REF] Provot | Hif-1alpha regulates differentiation of limb bud mesenchyme and joint development[END_REF][START_REF] Portron | Inverse regulation of early and late chondrogenic differentiation by oxygen tension provides cues for stem cell-based cartilage tissue engineering[END_REF]. Moreover, we show that HIF1α is necessary to maintain a physiologic chondrocyte microenvironment and function. Consistent with our data, the inhibition of HIF1α by 2-methoxyestradiol induced an OA phenotype in mice [START_REF] Gelse | Role of hypoxia-inducible factor 1 alpha in the integrity of articular cartilage in murine knee joints[END_REF], which suggests that HIF1α modulation is an important event that triggers chondrocyte differentiation in OA. With our conditional HIF1α-knockout mouse model, we show that chondrogenic HIF1α directly maintains cartilage metabolism. Moreover, we show that HIF1α is also a physiological anti-apoptotic factor in articular cartilage as its loss enhanced chondrocyte apoptosis. Six weeks after HIF1α deletion, the increase of apoptotic chondrocyte did not induce cartilage lesion as chondrocyte apoptosis alone is not sufficient to induce to induce cartilage lesion [START_REF] Bouaziz | Loss of sclerostin promotes osteoarthritis in mice via betacatenin-dependent and -independent Wnt pathways[END_REF]. Here, the increase in procatabolic enzymes in addition with increased apoptosis can exacerbate the cartilage lesion during OA. Finally the cartilage erosion observed in OA ∆HIF1α Chon mice results of the double function of HIF1α in articular cartilage as a Wnt inhibitor and an anti-apoptotic protein. However, we cannot discard that Epas1 could be involved in cartilage erosion, since it was described as an inhibitor of survival and catabolic activator [START_REF] Saito | Transcriptional regulation of endochondral ossification by HIF-2alpha during skeletal growth and osteoarthritis development[END_REF][START_REF] Ryu | Hypoxia-inducible factor-2alpha regulates Fas-mediated chondrocyte apoptosis during osteoarthritic cartilage destruction[END_REF].

Wnt/β-catenin signaling is one of the key pathways involved in OA [START_REF] Loeser | Osteoarthritis year in review 2013: biology[END_REF]. Its activation triggers the osteoarthritic differentiation of chondrocytes and OA in mice [START_REF] Yuasa | Wnt/beta-catenin signaling stimulates matrix catabolic genes and activity in articular chondrocytes: its possible role in joint degeneration[END_REF][START_REF] Nalesso | WNT-3A modulates articular chondrocyte phenotype by activating both canonical and noncanonical pathways[END_REF]. Thus, understanding the molecular regulators of Wnt signaling is of great therapeutic interest. Oxygen level is an important regulator of Wnt activity [START_REF] Kaidi | Interaction between beta-catenin and HIF-1 promotes cellular adaptation to hypoxia[END_REF][START_REF] Mitani | Coordinated action of hypoxiainducible factor-1alpha and beta-catenin in androgen receptor signaling[END_REF]. Indeed, high oxygen level promotes Wnt signaling and the differentiation of stem cells [START_REF] Hakim | High oxygen condition facilitates the differentiation of mouse and human pluripotent stem cells into pancreatic progenitors and insulin-producing cells[END_REF]. Hypoxia inhibited the destruction of human cartilage explants by reducing MMP13 production in a HIF1α-dependent manner [START_REF] Thoms | Hypoxia promotes the production and inhibits the destruction of human articular cartilage[END_REF]. Because MMP13 is an important target of both HIF signaling and canonical Wnt pathways [START_REF] Leeman | The structure, regulation, and function of human matrix metalloproteinase-13[END_REF][START_REF] Leeman | Matrix metalloproteinase 13 activity is associated with poor prognosis in colorectal cancer[END_REF][START_REF] Saito | Transcriptional regulation of endochondral ossification by HIF-2alpha during skeletal growth and osteoarthritis development[END_REF][START_REF] Saito | HIF-2alpha as a possible therapeutic target of osteoarthritis[END_REF][START_REF] Yun | Transcriptional regulation of MMP13 by Lef1 in chondrocytes[END_REF], we assessed whether HIF1α regulates MMP13 and Wnt signaling to prevent OA. Here we demonstrated that hypoxia downregulated canonical Wnt signaling, thereby preventing chondrocyte catabolism.

HIF1α deficiency exacerbated cartilage catabolism, thus HIF1α is necessary to prevent OA development. We show that Wnt-induced MMP13 expression was promoted in ∆HIF1α chondrocytes but was blunted by stabilized HIF1α in chondrocytes. Taken together, we demonstrate that HIF1α downregulates the transcription of MMP13 driven by canonical Wnt signaling.

Given the critical role of β-catenin to drive Wnt signaling, understanding the role of HIF1α-βcatenin interaction may reveal novel mechanisms in regulating Wnt signaling. Because HIF1α inhibits TCF4-β-catenin interaction and transcriptional activity (9), we investigated whether HIF1α modulates MMP13 through a Wnt/β-catenin pathway. Hypoxia promoted the translocation of β-catenin and binding to HIF1α but not MMP13 expression. These results are consistent with transcriptional blockade of β-catenin activity despite the stabilization of βcatenin in the nucleus. Our study brings new insights into the protein regulation of HIF1α and βcatenin interaction (9) and its impact on MMP13 transcription. Under hypoxia, HIF1α-β-catenin complexes are preferentially formed, which results in a lower TCF4-β-catenin complex level and therefore markedly reduced TCF4 binding to the MMP13 regulatory region. Interestingly, when stabilized in normoxic chondrocytes, HIF1α blocked TCF4 binding to the MMP13 regulatory region. Furthermore, the inhibition of TCF4-β-catenin complexes by PKF118-310 abolished Wnt3a-induced MMP13 expression in ΔHIF1α chondrocytes. These results confirm the role of TCF4-β-catenin complexes triggering MMP13 expression in ΔHIF1α chondrocytes. Thus, HIF1α is a nuclear negative regulator of TCF4-β-catenin complexes that inhibits the shift toward a catabolic phenotype in chondrocytes.

We further demonstrated that HIF1α signaling protected against cartilage damage by blocking TCF4-β-catenin. Indeed, PKF118-310 administration reduced cartilage breakdown and the expression of MMP13 observed in ∆HIF1α Chon mice. Our findings support a pro-catabolic role of Wnt/β-catenin signaling in OA and bring new insights in the modulation of Wnt/β-catenin signaling by hypoxia. Furthermore, we provide evidence that HIF1α is a potent inhibitor of β-catenin and Wnt signaling and is required to block cartilage degradation. The use of HIF1α agonists might be a useful strategy for treating cartilage lesions in OA.

Methods

Harvesting, expansion and transfection of primary chondrocytes. HIF1α fl/fl and VHL fl/fl mice (Jackson Laboratory) were used for in vitro experiments involving chondrocyte cultures.

Chondrocytes were harvested from 6-day-old mice and cultured with 10% fetal bovine serum (50% confluence). Recombination, transient overexpression and plasmid [START_REF] Yan | The hypoxia-inducible factor 2alpha N-terminal and C-terminal transactivation domains cooperate to promote renal tumorigenesis in vivo[END_REF] Primer sequences are detailed in supplemental data. Immunocytochemistry. Cells were cultured in 24-well plates containing cover glasses, fixed for 15 min with 4% formaldehyde (w/v). Cultures were saturated with 3% BSA for 60 min at room temperature, then incubated with the antibodies rabbit primary anti-HIF1α, mouse primary anti-β-catenin and anti-EPAS1 (All Santa Cruz Biotechnology) for 1 h. Cultures were incubated for 60 min with Alexa dye 488-conjugated rabbit secondary antibody or Cy3 dye-conjugated mouse secondary antibody. Cells were observed with Axio Observer Z1 (Zeiss).

Quantification of proteoglycan release, western blots analysis and immunoprecipitation.

Proteoglycan release was measured in the supernatant by colorimetric method. Whole cell lysates and nuclear extracts were prepared and proteins were extracted (n = 3 independent experiments). Immunoprecipitation, cloning and reporter gene assay are described in the supporting file.

Mice. To evaluate the expression of HIF1α during OA, we induced joint instability in 10-week-old male C57BL6 mice (Janvier, France) by destabilization of the medial meniscus (DMM) of the right knee, with sham operation performed on the left knee as described [START_REF] Kadri | Osteoprotegerin inhibits cartilage degradation through an effect on trabecular bone in murine experimental osteoarthritis[END_REF]. Mice were killed at weeks 0 (n=3), 4 (n=5) and 6 (n=5) after OA induction. fl/fl HIF1α, R26R and COL2Cre ERT mice were supplied by the Jackson Laboratory. At 9 weeks of age, COL2Cre ERT ;fl/fl HIF1α and COL2-Cre ERT ;R26R, fl/fl HIF1α and R26R mice were injected with tamoxifen (1 mg/10 g weight) (Sigma) daily for 5 days. Joint instability was induced in 10-week-old male ∆HIF1α chon mice (n = 8-10 per group) and fl/fl HIF1α littermates (n = 9-12 per group) in the right knee, with sham operation performed in the left knee. ∆HIF1α chon and fl/fl HIF1α were injected intra-articularly once a week with PKF118-310 or phosphate buffered saline (PBS; n=8 per group). Mice were killed 6 weeks after surgery. This time point is suitable to quantify the expression of MMP13 in the remaining cartilage. To monitor hypoxia level in healthy and OA cartilage, we injected the hypoxia marker pimonidazole hydrochloride (Hypoxyprobe, USA) in mice. Male FVB mice (Jackson laboratory) at 16 weeks old were intraperitoneally injected with 0.6 mg pimonidazole/10 g weight and killed 17 h later. Mice were treated in accordance with the Guidelines for Animal Experimentation issued by the local Committee (Ethics Committee Lariboisière-Villemin no. CEEALV/2012-02-01, Paris).

Histology. Knees were fixed in 4% PFA for 24 h at 4°C and decalcified in Osteosoft at room temperature for 4 days, tissue was embedded in paraffin. Serial 5-µm-thick sagittal sections of medial femorotibial joints were collected at 3 depths at 70-µm intervals. Sections of tibias and femurs were stained with Safranin-O. The OARSI scoring method was used for both tibias and femurs, with a total severity score ranging from 0 to 12 [START_REF] Glasson | The OARSI histopathology initiativerecommendations for histological assessments of osteoarthritis in the mouse[END_REF]. Immunohistochemistry methods are described in the supporting file.

  information are detailed in the supporting file. Real-time PCR. Real-time PCR involved use of SYBR green (Applied Biosystems) in (5 to 8) independent experiments. Averaged Ct values were normalized to the averaged Ct value of RPL13A. Adjusted average Ct values were used to calculate relative expression versus control.

Statistical analysis .

 analysis Data are reported as mean  SEM. Statistical analyses involved ANOVA and the Mann-Whitney test with Statview (SAS Inst., Cary, NC). P<0.05 was the threshold of statistical significance.

Figure legends : Figure 1 :

 :1 Figure legends:

Figure 2 :

 2 Figure 2: HIF1α inhibits the transcription of Wnt targets in Wnt3a-induced chondrocytes.

Figure 3 :

 3 Figure 3: Wnt3a promotes β-catenin translocation into the nucleus in hypoxia and normoxia.

Figure 4 :

 4 Figure 4: HIF1α binds β-catenin and inhibits transcription factor 4 (TCF4) binding to MMP13

Figure 5 :

 5 Figure 5: Loss of HIF1α increases TCF4-β-catenin complexes and cartilage lesions in OA mice

Figure S1 :

 S1 Figure S1: β-galactosidase immunostaining in COL2-Cre ERT ;R26R and R26R mice with injection of

Figure S2 A.

 S2 Figure S2A. EPAS1 expression in HIF1α fl/fl and ∆HIF1α Chon mice at Week 6 (immunohistochemistry) in

Significance statement:

Hypoxia-Inducible factor 1α (HIF1α) is an important factor for cell growth and survival. It modulates Wnt signaling regulating cell differentiation and fate. Osteoarthritis (OA) is an increasingly frequent joint disorder characterized by progressive cartilage breakdown in which Wnt/β-catenin signaling triggers matrix metalloproteinase 13 (MMP13) expression and chondrocyte catabolism. Here we demonstrate HIF1α inhibits β-catenin signaling by blocking tcf4-β-cat interaction and downregulates MMP13 expression, thereby alleviating cartilage lesions, whereas the transcription factor 4 (TCF4)-β-catenin signaling induces an OA phenotype in mice. In OA joints, PKF-118-310, a small molecule that blocked TCF4-β-catenin interaction, significantly reduced the progression of OA cartilage lesions. Thus, blockade of TCF4-β-catenin signaling by HIF1α represents a promising strategy to prevent articular cartilage loss in OA.