The definition of security for a system is given by the security policy. A system is “secure” only insofar as it correctly implements the security policy. But flaws in a system’s design and implementation may create vulnerabilities that allow an attacker to violate that policy, and the complexity of computer systems make it difficult to verify that a system’s design and implementation are free of flaws. In fact, the current state-of-the-art in system development is incapable of “proving” that a system of mo
· A Specifier’s Introduction to Formal Methods, Jeannette M. Wing
http://www.cs.cmu.edu/~wing/publications/CMU-CS-90-136.pdf