SymDiff is useful in ensuring that a method isn't called with secret data. However, it doesn't, by default, ensure that the decision to call a method is based only on public data. If you have a method that requires this, you need to use an artificial event counter.

For instance,
ghost var {:readonly} event_counter:int;

ghost method MethodThatShouldntBeCalledBasedOnSecretData ()
    requires public(event_counter);
    ensures event_counter == old(event_counter) + 1;

Currently, we use two such event counters, one for reading from the network and one for writing to the network. One perspective is that this is one too many, and that we should use a single event counter for all such methods. So if you have such a method you use the network output counter, and eventually we'll change the network input method to also use that counter.

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


No comments yet.