Formal methods in security engineering
John McLean · 2007
Starting with the Trusted Computer System Evaluation Criteria (aka the "Orange Book"), the information security community within the US Department of Defense has been advocating formal methods for decades. Others have followed suit, culminating in the appearance of the Common Criteria. The advantages of formal analysis seem self-evident. First, of the three things that are subject to certification -- people, process, and product -- product seems to be the most immediately relevant. Second, if we focus on product, testing seems insufficient; as Dijkstra famously noted, testing can reveal the presence flaws, but not their absence. This is especially true of security, where flaws may be intentionally constructed not to reveal themselves during normal testing. Despite this, the acceptance of formal methods has been less than universal.