Information flow control tries to prevent the leak of secret information to public outputs. But how does one formalize that a program doesn't leak secret information? We first investigate this question in the very simple setting of Coq functions taking two arguments, one we call the public input and the other one we call the secret input. Our functions return a pair containing one public output and one secret output. Say we have the following function working on natural numbers:

This function seems intuitively secure, since the first output pi+1, which we assume to be public, only depends on the public input pi, but not on the secret input si. The second output pi+si*2 depends on both the public input and the secret input, but that's okay, since we assume this second output to be secret. Still, what security notion does this function satisfy? Let's try it on a couple of inputs:

In the last two cases the value of the public output is equal to the value of secret input. But that's just a coincidence, and has nothing to do with the public output leaking the secret input, which wasn't used in computing the public output. So a naive security definition, which we'll only use as a strawman, is one that simply compares secret inputs with public outputs:

This definition would reject our secure function above as insecure:

Even worse, this broken definition of security would allow insecure functions, such as the following one whose public output is si+1:

This function's public output is never equal to its secret input, yet an attacker can easily compute one from the other by just subtracting 1. So the secret is entirely leaked, yet our broken definition accepts this:

This attempt at defining secure information flow by looking at how inputs and outputs are related for a single execution of the program has failed. In fact, it is well known in the formal security research community that secure information flow cannot be defined by looking at just one single program execution.

Noninterference for pure functions

The usual way to define secure information flow is a property called noninterference, which in its most standard form looks at two program executions: for two different secret inputs the public outputs should not change:

We defined this for arbitrary types of inputs and outputs, but we can still instantiate them to nat when looking at our example functions above:

The tactic specialize we used above instantiates a quantified hypothesis to the concrete arguments we specify. In the definition of noninterference we pass the same public inputs to the two executions, since this allows public outputs to depend on public inputs. To convince ourselves of this, let's look at the following too strong definition of security:

This basically says that the first output of f has to be constant, which is not the case for our secure_f.

Noninterference is still a very strong property. In particular, f being noninterferent is equivalent to f being splittable into two different functions, one of which doesn't get the secret at all.

Secure Multi-Execution (SME)

The previous proof also captures the key idea behind Secure Multi-Execution (SME), an enforcement mechanism that can make any function noninterferent. To achieve this SME runs the function twice, once passing a dummy secret as input to obtain the public output, and once using the real secrets to obtain the secret output.

Functions protected by sme are guaranteed to satisfy noninterference:

Moreover, if the function we pass to sme is already noninterferent, then its behavior will not change; so we say that sme is a transparent enforcement mechanism for noninterference:

It is interesting to look at what sme does for interferent functions, like insecure_f, whose public output was one plus its secret input:

Now the public output is one plus the dummy constant 0 we passed to the sme function, so always the constant 1.

This is a secure behavior, but a behavior that's different than that of the original insecure_f function. So we are giving up some correctness for security. There is no free lunch! The other downside of sme is that we have to run the function twice for our two security levels, public and secret. In general, we need to run the program as many times as we have security levels, which is often an exponential number, say if we take our security levels to be sets of principals. Other information flow control mechanisms overcome this downside, but have other downsides of their own, for instance:

• by requiring complex manual proofs for each individual program (e.g. Relational Hoare Logic), or
• by using static overapproximations that reject some secure programs (security type systems), or
• by using dynamic overapproximations that unnecessarily change program behavior, for instance forcefully terminating even some secure programs to prevent leaks, in which case they are not transparent (dynamic information flow control).

Again, there is no free lunch!

Noninterference for state transformers

This development is easy to adapt to functions that transform states (state→state), where we label each variable as either public or secret.

We can prove an equivalence between noninterferent_state and our original noninterferent definition. For this we need to split and merge states, and a few helper lemmas. The way we define split_state and merge_state is a good example of programming with higher-order functions, and there's more of this in Maps. The split_state function takes a state s and zeroes out the variables x for which pub x is different than an argument bit b. So split_state s pub true keeps the public variables, and zeroes out the secret ones. Dually, split_state s pub false keeps the secret variables, and zeroes out the public ones.

The merge_state function takes in two states s₁ and s₂ and produces a new state that contains the public variables from s₁ and the private variables from s₂.

The technical development needed for the equivalence proof between noninterferent_state and our original noninterferent definition is not that interesting though, and can be skipped on first read.

Now we can finally state our theorem about the equivalence between non_interferent_state and noninterferent:

SME for state transformers

One thing to note in this proof is that we used the lemma Bool.eqb_spec to do case analysis on whether the pub x' is equal to true. For more details on how this works, please check out the explanations about the reflect inductive predicate in IndProp.

Noninterference and SME for Imp programs without loops

For programs without loops the "failed attempt" evaluation function from Imp works well and allows us to easily define a state transformer function for each command.

For proving secure_com noninterferent we first prove a few helper lemmas.

Here we are using the t_update_neq and t_apply_empty lemmas that were proved in Maps

Using these lemmas the noninterference proof for secure_com is easy:

Now let's look at a couple of insecure commands:

An explicit flow is when a command directly assigns an expression depending on secret variables to a public variable, like the X := Y+1 assignment above. We can prove that this is insecure:

Noninterference can be violated not only by explicit flows, but also by implicit flows, which leak secret information via the control-flow of the program. Here is a simple example:

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 can use sme_state to execute such programs to obtain a noninterferent state transformer, by running them 2 times, once on a state without secrets and once on the original input state and then merging the final states.

The result of applying sme_cmd to a program is no longer a program, but a state transformer. We can prove them noninterferent as state transformers using our noninterference theorem about sme_state.

Noninterference and SME for Imp programs with loops

In the presence of loops, we need to define noninterference using the evaluation relation (ceval) of Imp:

Now to define SME we also need to use a relation, of a similar type to ceval:

To state that sme_eval is secure, we need to generalize our noninterference definition, so that it works not only with ceval, but with any evaluation relation, including sme_while pub.

The proof that while_sme is noninterferent is as before, but now it relies on the determinism of ceval, which was obvious for state transformer functions, but is not obvious for evaluation relations.

Turns out we can only prove a weak version of transparency, and this has to do with nontermination (more later). But first we need a few lemmas:

More specifically, we can only prove that sme_while execution implies ceval. But we cannot prove the reverse implication, since a command terminating when starting in state s, does not necessarily still terminates when starting in state split_state s pub true, as would be needed for proving sme_while.

Still, it seems we can still do the same things as in the setting without while loops, including SME (just not fully transparent). So is there anything special about loops and nontermination? Yes, there is! Let's look at our noninterference definition again:
Definition noninterferent_while pub c := ∀ s₁ s₂ s₁' s₂',
  pub_equiv pub s₁ s₂ →
  s₁ =[ c ]=> s₁' →
  s₂ =[ c ]=> s₂' →
  pub_equiv pub s₁' s₂'. It says that for any two terminating executions, if the initial states agree on their public variables, then so do the final states. This is traditionally called termination-insensitive noninterference (TINI), since it doesn't consider nontermination to be observable to an attacker. In particular, the following program is considered secure wrt TINI:

And we can prove it ...

Termination-Sensitive Noninterference

We can give a stronger definition of security that prevents such nontermination leaks. It is traditionally called termination-sensitive noninterference (TSNI) and it is defined as follows:

We can prove that termination_leak doesn't satisfy TSNI:

More generally, we can prove that TSNI is strictly stronger than TINI (noninterferent_while)

The reverse direction of the implication only works for programs that always terminate (such as most of our simple examples above).

Now for a more interesting use of TSNI: it turns out that sme_while is transparent for programs satisfying TSNI.

Unfortunately sme_while does not imply TSNI, and this is hard to fix in our current setting, where programs only return a result in the end, a final state, so we had to merge the public and secret inputs into a single final state. Instead, SME is commonly defined in a setting with interactive IO, in which public outputs and secret outputs can be performed independently, during the execution. In that setting, it does transparently enforce TSNI.