Security is not like paint: it can’t just be applied after a system has been completed. Instead, security has to be built into the system design. But how can we know that a system design is secure against a particular attack? And how can we know that the system implements that design correctly?

The key problem, on one hand, is that system design specifications are often ambiguous and incomplete, with specifications (if they exist at all) intended for human consumption and reasoning. On the other hand, system implementations are often highly complex, evolving over time, and often diverging from design specifications as they evolve.