Here a present an idea for a simple tool for information flow control. As usually, the idea is language-parametric.
The goal
We want to verify that a program satisfies a termination-insensitive non-interference property. The property basically says that a change of values of secret variables should not influence publicly observable outputs. That is, if everything except “high” variables is the same at the beginning of the execution, then everything except “high” variables will be the same at the (assumed) termination. By transitivity, the problem can be reduced to having a single “high” input variable and a single “high” output variable. Also, even if the semantics of the chosen programming language is effectfull (that is, the induced transition system has non-trivial edge labeling), I will work in an effect-less / unlabeled setting, as one can always transform the language definition to accumulate effects in the configurations.
The approach
We first transform the language definition D into some D’ such that the following holds. (1) there exists a projection P of D’-configurations into D-configurations such that (1.1) x’ ~> y’ if and only if P(x’) ~> P(y") (for any D’-configurations x’,y’), and (2) there exists a predicate H on D’-configurations for all D’-configurations x'1, x'2, y'1, y'2, if P(x'1)=P(x'2) and x'1 ~> y'1 and x'2 ~> y'2, then (2.1) P(y'1) = P(y'2) and (2.2) if H(x'1) <-> H(x'2) then y'1 = y'2. The property (1) can be called “conservativeness” (the new language definition behaves essentially the same way as the old one), the property (2) “tracking” (the new language definition keeps track of whether the behavior depends on a “high” input - hence the name H).'
How does this help us proving non-interference? Consider a family of configurations c(I), where I represents the “high” input, and a family of terminal configurations d(O), where O represents the “high” output. We want to prove that a change in the input does not move the system outside d(O); that is: for every i1,i2, if c(i1) ~>* d(o1) for some o1 ∈ O, then c(i2) ~>* d(o2) for some o2 ∈ O. But the translation allows us to reduce this goal to something like: for every D’-configuration c’ such that P(c’) = c(i) for some i ∈ I and ¬H(c’), c’ reaches on all paths to some configuration d’ such that P(d’) = d(o) for some o ∈ O and ¬H(d’). And we can use the standard all-path reachability logic / symbolic execution to verify this. (That the reduction works is only a conjecture of mine.)
Transforming the language definition
First, we transform the FOL model over which the language definition is built, such that its every value has in addition a “tainted”-ness flag, and so that there is a bool-valued function is_tainted in the model, and that there is a function make_tainted : bool -> M -> M that keeps the value but makes it tainted, and so that taintedness “reasonably” propagates through the operations of the model (to account for the data-flow dependency). Then, every semantics rule l => r if p(e1,...,en), where p(e1,...,en) is a predicate , needs to be updated such that expressions on the right-hand side become tainted whenever expressions used in the side-condition are. This will account for the control-flow dependency.
Transforming the model of values
But how do we transform the potentially large model of values without resorting to a lot of manual work? What if it is composed of multiple smaller models of values (for ints, bools, lists, etc)? And what if we want to have more fine-grained control over the propagation of tainted-ness - for example, what if it is only the parity of a natural number that is tainted, and division by two then clears the tainted-ness? These are the questions for the next time. Maybe.