Proving code correct

Most of us spent some time in school studying program proofs in a way or another. Many techniques exist, but in most cases, their most important use it to make students understand that, sometimes, a computation does not end.

Proving programs is hard, but the hardness of the proof greatly depends on what you want to prove. We can split proofs in two groups:

  • Proving generic properties on programs. In that case, we are simply trying to prove that a given program (for instance, a Java Card program), satisfies a given property. This can be very simple. For instance, the property “The program does not use sharing” can be proven simply by ensuring that the program does not refer to any shareable interface. In such a case, a syntactical check (which does not look at all at what the program actually does) is sufficient. Sometimes, the proof is not as simple. For instance, the property “The program only sends SMS’s to French phone numbers” (on a MIDP program) is more complex to prove, because it requires an analysis of the data used by the program. In that case, the prover needs to simulate the way in which the program works in order to figure out all possible phone numbers that can be used to send SMS’s, and then analyze that. In that case, a semantic check (which somehow looks at what the program does) is required.
  • Proving that a program actually implements its specification. Now, this is the hard part. The first difficulty is actually to write the specification in a way that can be understood by a prover (i.e., a formal specification). Many languages exist to do that, and they are quite complicated. On Java Card, a famous result has been to prove that the verifier actually does its work and guarantees that programs run safely. Multos also had a similar result, in which they proved that running a program was safe(memory-wise). In both cases, it resulted to high-level security certifications (good for publicity and marketing).

Now, how useful are these results?

The first kind of proof is called static analysis. We actually think about using this technique in the deployment of certified NFC applications, because it allows us to prove that an application does not interfere with other applications. And we also have been using this technique in the security evaluation of applications for years. Its main advantage is that is works on binary code, which means that it integrates easily in a signature scheme (a program is signed only if static analysis succeeds).

For formal proofs, we are not as close to direct exploitation. In the case of Java Card, it resulted in the discovery of a few interesting bugs in the specification of the Java Card Virtual Machine and API, which have been fixed in subsequent releases. This often occurs, as the construction of a formal specification forces developers to look into minute details of the spec, which often happen to be the source of issues and bugs.

In quite recent news, an Australian team (NICTA) has announced that they have built a complete formal proof of an operating system kernel, which could be used in mobile devices. This piece of software represents 7500 lines of code, but the formal proof represents 200,000 lines, and it took 4 years to a team of 12 people to build it. Even if they didn’t work on this full time, this means that we are not going to see such proofs on a daily basis. However, this could become more common, because of the side results of this work, as explained by its leader in the press release:

“This work goes beyond the usual checks for the absence of certain specific errors. Instead, it verifies full compliance with the system specification. The project has yielded not only a verified microkernel but a body of techniques that can be used to develop other verified software.”

Hopefully, we will see more of it, since proving programs can definitely lead to more stable programs, and we need that.

Another good news is that the technology is apparently open source, and that it will be transferred to Open Kernel Labs, a well-known Australian company in the field of mobile hypervisors.

Once again, it reminds us that mobile security is a hot topic, and there is still hope that our mobile devices will not become our next PC platform, ridden with vulnerabilities and malware.

No Comments

Leave a Reply

Your email is never shared.Required fields are marked *