In Ironclad, we have a new way of specifying information-flow properties that takes some explaining. These information-flow properties are checked by a tool called SymDiff, which generally runs after DafnyCC has compiled and verified functional-correctness properties.

If any device may leak information outside of the trusted part of the platform, its specification ensures that only public data may be leaked out that interface. Thus, if you ever try to output anything to, say, the network card, SymDiff is going to raise an alarm if you don't prove that it's public.

The specification also says that data you read from untrusted parts of the platform is public. So you can prove data is public if you read it from, say, the network. But, most of the time, you'll want to do something to that data before you output it. If you can prove that your output derives only from public data, you'll be allowed to output it. But how do you prove such "derivation"?

Suppose we have a set of expressions S that are known to be public, and we want to prove that another expression D is also public. We can do this by proving that, for any two program runs L and R in which each expression S takes on the same value in both runs, D also takes on the same value in both runs.

We call these two runs L and R the "left" run and the "right" run. We use left(E) as the value that E takes on in the left run, and right(E) as the value that E takes on in the right run. So the axiom SymDiff applies is:
public(S) && (left(S) == right(S) ==> left(D) == right(D)) ==> public(D)

Indeed, viewed this way, you can think of public(X) as a synonym for left(X) == right(X). If this appears in a pre-condition, then SymDiff considers only pairs of runs in which X takes on the same value in both runs. If this appears in a post-condition, then SymDiff tries to prove that in any pair of runs considered, X takes on the same value.

Unfortunately, SymDiff can only look at these relational invariants when they're pre-conditions, post-conditions, or loop invariants. So you can't, for instance, assert(public(X)).

Sometimes you'll need to output data that can't be proven to be public. For instance, if you encrypt secret data using your private key, that encryption derives from the private key, which derives from randomness read from the trusted platform, which is obviously not public. However, you and I and the remote verifier know that the encryption scheme doesn't actually reveal anything about the key. So you'll need to convey that in an axiom that essentially forces SymDiff to accept something as public. For instance, you can write:
method {:axiom} DeclassifyEncryption (m:seq<int>, k:RSAKey, e:seq<int>)
    requires e == RSAEncrypt(m, k);
    ensures public(e);

so you can encrypt something, call DeclassifyEncryption, then output the encryption on the network.

Note the {:axiom} and the lack of a body. The lack of a body means that Dafny and DafnyCC will take all the post-conditions on faith. If this sounds dangerous, that's because it is, and for this reason the build system won't build an executable if there are any body-less methods. However, the :axiom directive tells the system it's OK to build an executable even though there's no body on this method.

Event counters

Last edited Oct 14, 2014 at 11:14 PM by howell, version 2


No comments yet.