Noninterference

As explained in Noninterference and RelHoare, data confidentiality is most often expressed formally as a property called noninterference. To formalize this for Imp programs, we divide the variables as either public or secret by assuming a total map P : pub_vars between variables and Boolean labels:

A noninterference attacker can only observe the values of public variables, not of secret ones. We formalize this as a notion of publicly equivalent states that agree on the values of all public variables, which are thus indistinguishable to an attacker:

For some total map P from variables to Boolean labels, pub_equiv P is an equivalence relation on states, so reflexive, symmetric, and transitive.

Program c is noninterferent if whenever it has two terminating runs from two publicly equivalent initial states s₁ and s₂, the obtained final states s₁' and s₂' are also publicly equivalent.

Intuitively, c is noninterferent when the value of the public variables in the final state can only depend on the value of public variables in the initial state, and do not depend on the initial value of secret variables. For instance, consider the following command (taken from Noninterference):

If we assume that variable X is public and variable Y is secret, we can state noninterference for secure_com as follows:

We have already proved that secure_com is indeed noninterferent both directly using the semantics (in Noninterference) and using RHL (in RelHoare). Both these proofs were manual though, while in this chapter we will show how this proof can be done more syntactically using several information flow control (IFC) type systems that enforce noninterference for all well-typed programs. Not all programs are noninterferent though. For instance, a program that reads the contents of a secret variable and uses that to change the value of a public variable is unlikely to be noninterferent. We call this an explicit flow and all our type systems will prevent all explicit flows. Here is a program that has an explicit flow, which breaks noninterference, as we already proved in Noninterference.

Not all explicit flows break noninterference though. For instance, the following variant of insecure_com1 is noninterferent even if it has an explicit flow. The reason for this is that the variable X is overwritten with public information in a subsequent assignment.

Since our IFC type systems will prevent all explicit flows, they will also reject secure_com1', even if it is secure with respect to our attacker model for noninterference, in which the attacker only observes the final values of public variables. As usual, our type systems will only provide sound syntactic overapproximations of the semantic property of noninterference. Explicit flows are not the only way to leak secrets: one can also leak secrets using the control flow of the program, by branching on secrets and then assigning to public variables. We call these leaks implicit flows.

Here the expression X+1 we are assigning to X is public information, but we are doing this assignment after we branched on a secret condition Y = 0, so we are indirectly leaking information about the value of Y. In this case we can infer that if X gets incremented the value of Y is not 0. We have proved in Noninterference that this program is insecure, so it will be rejected by our type systems, which enforce noninterference by preventing all implicit flows. Not all implicit flows break noninterference though. For instance, in RelHoare we saw a program that we proved to be noninterferent, even though it contains both an explicit and an implicit flow:

Intuitively, even if this program branches on the secret Y, it always assigns the value 0 to X, so no secret is leaked. Still, our type systems will reject programs containing any explicit or implicit flows, this one included. C'est la vie!

Type system for noninterference of expressions

We will build a type system that prevents all explicit and implicit flows. But first, let's start with something simpler, a type system for arithmetic expressions: our typing judgement P ⊢a- a \in l specifies the label l of an arithmetic expression a in terms of the labels of the variables read it reads. In particular, P ⊢a- a \in public says that expression a only reads public variables, so it computes a public value. P ⊢a- a \in secret says that expression a reads some secret variable, so it computes a value that may depend on secrets. Here are some examples:

• For a variable X we just look up its label in P, so P ⊢a- X \in P X.
• For a constant n the label is public, so P ⊢a n \in public.
• Given variable X₁ with label l₁ and variable X₂ with label l₂, what should be the label of X₁ + X₂ though?

Combining labels

We need a way to combine the labels of two sub-expressions, which we call the join (or least upper bound) of the two labels:

	(T_Num)
P ⊢a- n ∈ public

	(T_Id)
P ⊢a- X ∈ P X

P ⊢a- a1 ∈ l1    P ⊢a- a2 ∈ l2	(T_Plus)
P ⊢a- a1+a2 ∈ join l1 l2

P ⊢a- a1 ∈ l1    P ⊢a- a2 ∈ l2	(T_Minus)
P ⊢a- a1-a2 ∈ join l1 l2

P ⊢a- a1 ∈ l1    P ⊢a- a2 ∈ l2	(T_Mult)
P ⊢a- a1*a2 ∈ join l1 l2

	(T_True)
P ⊢b- true ∈ public

	(T_False)
P ⊢b- false ∈ public

P ⊢a- a1 ∈ l1    P ⊢a- a2 ∈ l2	(T_Eq)
P ⊢b- a1=a2 ∈ join l1 l2

...
P ⊢b- b ∈ l	(T_Not)
P ⊢b- ~b ∈ l

P ⊢b- b1 ∈ l1    P ⊢b- b2 ∈ l2	(T_And)
P ⊢b- b1&&b2 ∈ join l1 l2

Restrictive type system prohibiting branching on secrets

For commands, we start with a simple type system that doesn't allow any branching on secrets, which prevents all implicit flows. For preventing explicit flows when typing assignments, we need to define when it is okay for information to flow from an expression with label l₁ to a variable with label l₁.

In particular, we disallow the value of secret expressions to be assigned to public variables.

We allow public information to flow everywhere, and secret information to flow to secret variables:

	(PCWT_Skip)
P ⊢pc- skip

P ⊢a- a ∈ l    can_flow l (P X) = true	(PCWT_Asgn)
P ⊢pc- X := a

P ⊢pc- c1    P ⊢pc- c2	(PCWT_Seq)
P ⊢pc- c1;c2

P ⊢b- b ∈ public    P ⊢pc- c1    P ⊢pc- c2	(PCWT_If)
P ⊢pc- if b then c1 else c2

P ⊢b- b ∈ public    P ⊢pc- c	(PCWT_While)
P ⊢pc- while b then c end

Secure program that is pc_well_typed:

Explicit flow prevented by pc_well_typed:

Implicit flow prevented by pc_well_typed:

We show that pc_well_typed commands are noninterferent.

Remember the definition of noninterferent is as follows:

forall s1 s2 s1' s2',
  pub_equiv P s1 s2 ->
  s1 =[ c ]=> s1' ->
  s2 =[ c ]=> s2' ->
  pub_equiv P s1' s2'.

The main intuition is that the two executions will proceed "in lockstep", because all the branch conditions are enforced to be public, so they will execute to the same Boolean in both executions. The proof is by induction on s₁ =[ c ]=> s₁' and inversion on s₂ =[ c ]=> s₂' and P ⊢pc- c. Here is a sketch of the two most interesting cases:

• In the conditional case we have that c is if b then c₁ else c₂, P ⊢pc- c₁, P ⊢pc- c₂, and P ⊢b- b \in public. Given this last fact we can apply noninterference of boolean expressions to show that beval st₁ b = beval st₂ b. If they are both true, we use the induction hypothesis for c₁, and if they are both false we use the induction hypothesis for c₂ to conclude.
• In the assignment case we have that c is X := a, P ⊢a- a \in l, and can_flow l (P X) = true, which expands out to l == public ∨ P X == secret.
  If l == public then by noninterference of arithmetic expressions then aeval st₁ a = aeval s₂ a, so we are assigning the same value to X, which leads to public equivalent final states (since the initial states were public equivalent).
  If P X == secret then the value of X doesn't matter for determining whether the final states are pub_equiv.

pc_well_typed too strong for noninterference

While we have just proved that pc_well_typed implies noninterference, this is too strong a restriction for just noninterference. For instance, the following program contains no explicit flows and no implicit flows, so it is intuitively noninterferent, yet it is still rejected by the type system just because it branches on a secret:

We will later show that pc_well_typed enforces a security notion called program counter security, which prevents some side-channel attacks and which also serves as the base for cryptographic constant-time.

IFC type system allowing branching on secrets

We now instead extend this to a more permissive type system for noninterference in which we do allow branching on secrets. Now to prevent implicit flows we need to track whether we have branched on secrets. We do this with a program counter (pc) label, which records the labels of the branches we have taken at the current point in the execution (joined together).

	(WT_Skip)
P ;; pc |-- skip

P ⊢a- a ∈ l   can_flow (join pc l) (P X) = true	(WT_Asgn)
P ;; pc |-- X := a

P ;; pc |-- c1    P ;; pc |-- c2	(WT_Seq)
P ;; pc |-- c1;c2

P ⊢b- b ∈ l    P ;; join pc l |-- c1
P ;; join pc l |-- c2	(WT_If)
P ;; pc |-- if b then c1 else c2

P ⊢b- b ∈ l    P ;; join pc l |-- c	(WT_While)
P ;; pc |-- while b then c end

With this more permissive type system we can accept more noninterferent programs that were rejected by pc_well_typed.

And we still prevent implicit flows:

Dealing with unsynchronized executions running different code

We show that well_typed commands are noninterferent.

The noninterference proof is still relatively simple, since the cases in which we take different branches based on secret information are all handled by the different_code lemma. Another key ingredient for having a simple noninterference proof is working with a big-step semantics.

Type system for termination-sensitive noninterference

The noninterference notion we used above was "termination insensitive". If we prevent loop conditions depending on secrets we can actually enforce termination-sensitive noninterference (TSNI), which we defined in Noninterference as follows:

We could prove that pc_well_typed enforces TSNI, but that typing relation is too restrictive, since for TSNI we can allow if-then-else conditions to depend on secrets. So we define a new type system that only prevents loop conditions to depend on secrets.

We just need to update the while rule of well_typed:

Old rule for noninterference:

P ⊢b- b ∈ l    P ;; join pc l |-- c	(WT_While)
P ;; pc |-- while b then c end

New rule for termination-sensitive noninterference:

P ⊢b- b ∈ public    P ;; public ⊢ts- c	(TS_While)
P ;; public ⊢ts- while b then c end

Beyond requiring the label of b to be public, we also require that once one branches on secrets with if-then-else (i.e. pc=secret) no while loops are allowed.

We prove that ts_well_typed enforces TSNI.

For this we show that ts_well_typed implies well_typed, so by our previous theorem also noninterference. Then we show that P;; secret ⊢ts- c implies termination. Then we show that ts_well_typed implies equitermination, which together with noninterference implies termination-sensitive noninterference.