Last Christmas, I gave you my HeartBleed

With HeartBleed well and truly behind us, and entered into the history books, I want to tackle the idea that HeartBleed would've definitely been prevented with the application of formal methods -- specifically those that culminate in a proof of correctness regarding the system.

Despite sounding really good, this is actually a false statement, and the reasoning isn't actually all that subtle.

To demonstrate, I'm going to use a common example, the Bell and LaPaulda model for mandatory access control.

The model is, roughly, that everything is a resource or a subject. Both resources and subjects have classifications (we'll just limit ourselves to two), for example, "low" and "high". Subjects with low classification can only read low resources. Subjects with high classification may read both high and low resources.

The specification of the write operations is not currently relevant.

So, let's try and specify this in (something like) the Z notation; we need two operations, ReadOk and ReadError. ReadOp is a combination of both of them.

I apologise in advance, this is the bastardisation of Z that I could work into a blog post without inclining images.

ReadOk:

Variables:
SubjectClassification?
ResourceId?
Result!

Predicates:
(SubjectClassification? = high) || (classificationOfResource(resourceFromId(resourceId?)) = low)
Result! = resourceFromId(resourceId?)

What this can be read as is, given inputs SubjectClassification and ResourceId, and an Result output; and the predicate (SubjectClassification? = high) || (classificationOfResource(resourceFromId(resourceId?)) = low), then the Result output is the resource.

This embodies the "Read down" property of Bell & LaPaulda. If a subject has high classification, then they can read, otherwise, the resource must have a low classification.

The ReadError operation is similarly designed;

ReadError:

Variables:
SubjectClassification?
ResourceId?
Result!

Predicates:
(SubjectClassification? = low) && (classificationOfResource(resourceFromId(resourceId?)) = high)
Result! = error

This basically, roughly, very poorly, states that if you're a low classification subject, and you try to read a high classification resource, you'll get an error.

We now know that, for our specification, we're done.

This looks really good! A decent specification that we can really work to! Let's implement it!

public class BLPFileSystem {

  public enum Classification { LOW, HIGH }

  private final Map<ResourceId, Resource> resourceMap;

  public Resource readById(final ResourceId id, Classification subjectClassification) {

    assert id != null;

    assert resourceMap.contains(id);



    Resource r = resourceMap.get(id);

    Classification resClass = r.getClassification();

    r.setClassification(LOW);



    if (subjectClassification == HIGH) {

      return r;

    } else if (resClass == LOW) {

      return r;

    } else {

      throw new IllegalAccessException();

    }

  }

}
 

Also, imagine the rest of the infrastructure is available and correct...

Well, this is obviously broken. If you've skipped the code, the offending line is "r.setClassification(LOW);"

That's right, this method declassifies everything as it goes along!

Interestingly, this completely meets our specification. Now, if this was an automatically verified (engage hand-waving/voodoo), I could push this to production with no hassle.

This isn't just a contrived example, but a demonstration of a general issue with these sorts of things.

A specification is usually a minimum of what your software must do -- it usually does not declare a maximum. In OpenSSL's case, the software did the minimum that it was supposed to, it also went above and beyond it's specification to work in new and interesting ways; which turned out to be really bad.

Even with our file system, we can add predicates to ensure that the state of the read file is not changed by reading it; but then the state of other files could be modified. A bad service could declassify every other file when reading any file.

It's not easy to just put "must not" into the spec. Many cryptography systems must run in adversarial situations, for example, sharing virtual machines sharing hardware with adversaries. These systems must protect their key material despite a threat model in which the adversary can measure the time, power and cache effect of the system.

In our example, the system can still violate the "spirit" of the specification by leaking information based on timing-dependant operations.

In part, this exists because the specification is a "higher level" of abstraction, and the abstraction is not perfect.

Now, that is not to say that we should abandon formal methods. Far from it, these, and related formalisms are the kinds of things which save lives, day in, day out. The overall quality of most projects would be vastly improved if some degree of formal methods had been applied from the start. Doubly so if it's something as unequivocally bad as the OpenSSL source. It's just that, in the face of security, our tools need some refinement.