Programmers have to be very careful about how information flows in the software they develop to prevent leaking secret data. For instance in Moodle students shouldn't be able to obtain information about other student's grades. Or in crypto protocols the crypto keys should be kept secret and not sent over the network in clear. Information flow control tries to prevent leaking secret information. But how does one formalize that a program doesn't leak any information about the secret inputs to public outputs? 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 where the first element is the public output and the second one the 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, how can we mathematically define that this function is secure? 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 at all in computing the public output.

Naive attempt at defining secrecy

So a naive security definition, which we'll only use as a strawman, is one that simply compares secret inputs with public outputs:

As discussed above, 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 was a complete failure. 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 simplest correct 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:

This defines noninterference for arbitrary types of inputs and outputs, so we can instantiate them to nat when looking at our example functions above:

A too strong secrecy definition

In the definition of noninterference above we pass the same public inputs to the two executions and 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 public output of f can depend neither on the public input not on the secret input, so it has to be constant, which is not the case for our secure_f.

Noninterferent implies splittable

Noninterference is still a very strong property though. 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 secret input 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 of sme insecure_f 0 is one plus the dummy constant 0, so always the constant 1.

This is a secure behavior, but it is different from 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. This is inefficient! Other information flow control mechanisms overcome this downside, but have other downsides of their own, for instance:

• by requiring nontrivial 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; an extension of dynamic taint tracking to also handle implicit flows).

Again, there is no free lunch!

Noninterference for state transformers

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

Instead of requiring that the first elements of two pairs are equal, we require that the two states have equal values on the variables labeled public by the pub map.

This makes the definition more symmetric, since we can use pub_equiv both for the input states and the output states:

We can prove an equivalence between noninterferent_state and our original noninterferent definition. For this we need to split and merge states. We also need 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 one can skip directly to the noninterferent_state_ni statement on first read.

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

SME for state transformers

We can use the split_state and merge_states functions above to also define SME for state transformers.

We can prove the same two theorems as for sme above:

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 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.

SME for Imp programs without loops

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 all the state transformers obtained by sme_cmd noninterferent using our noninterference theorem about sme_state.

Noninterference for Imp programs with loops

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

SME for Imp programs with loops

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 for noninterferent programs, and this has to do with nontermination (more later).

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. Yet it seems we can still do most of the 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 secure wrt TINI:

And we can prove it ...

Termination-Sensitive Noninterference

We can give a stronger definition of security that disallows 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 enforce 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 a version of TSNI.