How does formal verification guarantee secure, error-free code?

It doesn't guarantee that the code is free of vulnerability. However, if verification is used appropriately, it can increase assurance (confidence) that the application is secure.

Speaking from a very broad perspective, there are two aspects of this problem:

• Verification. Given a mathematical model of the system and a mathematical specification of the requirements, does the system meet the specs?

• Validation. Do we have the right set of requirements? Does the mathematical spec accurately reflect the true requirements? Does the mathematical model accurately and completely correspond to the code?

Sometimes people focus only on verification, but both matter.

In your situation, if the specification incorporates all relevant security requirements, and if the mathematical model correctly corresponds to the code, and if the verification is done appropriately and is successful, then we may have a basis for significantly increased assurance that the system will meet our security requirements.

In the best case, verification can be a powerful tool to help assure security, one of the most powerful that we have. However, as with anything, it is possible to misuse the technology or get a false sense of security if it is not used appropriately. One of the most common failure modes is that the verification process does not verify all relevant security requirements (some are overlooked or omitted).

To say much more might require delving into the details of the system, the security requirements, and the nature of the verification that was done, but hopefully this gives you an overview.

Formal verification does not guarantee a secure system. Nothing guarantees a secure system. What formal verification can do is provide a very high assurance that some parts of the system are secure.

Formal verification gives a mathematical proof that under certain assumptions, a model of the system has certain properties. Thus, if part of the system has been formally verified, there still remains several conditions for the system to be secure:

• Are the assumptions underlying the verification met?
• Does the system match the model that has been verified?
• Is the proof given by the verification system correct?
• Are the proven properties sufficient to ensure the security of the system?

The extent of the formal verification can vary a lot. For example, buffer overflows — a common kind of vulnerability — can be spotted pretty easily: most languages that are higher-level than C or C++ guarantee the absence of buffer overflows in the compiled program. It can nonetheless happen that the compiler allows broken code to get through — while compiler bugs are a lot rarer than program bugs, they are not impossible. Buffer overflows are only one kind, however; most systems' security depend on far more than knowing that there are no buffer overflows. (Related reading: Why don't computers check whether there are memory contents in some memory space?)

To illustrate the limitations above, let me take a concrete example. Some smart cards run a Java Card virtual machine, and execute only bytecode that has been verified. The bytecode verifier, in principle, guarantees that the code cannot peek or poke outside its alloted memory space. This avoids some vulnerabilities but not all:

• The verification only guarantees its properties if the bytecode interpreter behaves according to its specification. Furthermore, if hardware does not execute the interpreter correctly, all bets are off (for example, one way to attack a smartcard is to cause a power glitches which results in some instructions being skipped).
• If there is a bug that allows code to be uploaded without going through the verifier, then it is possible that the code on the card will not have the properties guaranteed by verification.
• The verifier itself may be buggy and allow incorrect code to be uploaded.
• Even if the code of the applications on the card does not directly access the memory of other applications, it may still spy or perturbate them in other ways. For example, it may exploit a side channel such as timing to deduce properties of other code running on the same device.
  Furthermore, the security of the system may depend on things other than the isolation between applications on the card. For example, the authentication system may allow an attacker to take control of the card, there may be a protocol-level vulnerability that allows the attacker to disrupt communications, etc.

In a high-assurance system, formal verification can help in two ways:

• Proving that the code matches its specification. This requires a formal model of the execution environment (hardware, compiler or interpreter, standard library, …) and a lot of work.
• Proving that the specification has certain desirable properties. This requires a formalization of the specification, a judicious choice of properties and a lot of work.

The Common Criteria for security evaluations define several assurance levels. Only the highest assurance level (EAL7) requires formal verification. This is not the only requirement: formal verification does not preclude the evaluation of other aspects of the system, including documentation, penetration testing, etc.

Formal verification really only works in extremely constrained cases where a system can be modeled as a series of transforms with clearly defined domains, ranges, and clearly understood rules that define the behavior of a function - in many cases this means that you're dealing with a system that is the software realization of a mathematical model, or that it's (relatively :-) ) easy to derive a model from the systems behavior (digital circuits of significantly less complexity than a general purpose CPU)

I worked in some forerunners to this in the '80s, where the effort was in generating 'provably correct code' - One system I recall was named Adele, and operated on programs written in (uggh) Ada. Anecdotally, we used to joke that using Adele meant that it took 10 times as long to write, it ran 10 times more slowly, and it only crashed 10% as much - You might want to look at Bertrand Meyer's writings on Eiffel, he put significant thought and effort into how a language could provide internal verification checks via preconditions, postconditions, invariants, and a bunch of other stuff I have since forgotten.....