If it's Provably Secure, It Probably Isn't: Why Learning from Proof Failure is Hard

Abstract

In this paper we're going to explore the ways in which security proofs can fail, and their broader lessons for security engineering. To mention just one example, Larry Paulson proved the security of SSL/TLS using his theorem prover Isabelle in 1999, yet it's sprung multiple leaks since then, from timing attacks to Heartbleed. We will go through a number of other examples in the hope of elucidating general principles. Proofs can be irrelevant, they can be opaque, they can be misleading and they can even be wrong. So we can look to the philosophy of mathematics for illumination. But the problem is more general. What happens, for example, when we have a choice between relying on mathematics and on physics? The security proofs claimed for quantum cryptosystems based on entanglement raise some pointed questions and may engage the philosophy of physics. And then there's the other varieties of assurance; we will recall the reliance placed on FIPS-140 evaluations, which API attacks suggested may have been overblown. Where the defenders focus their assurance effort on a subsystem or a model that cannot capture the whole attack surface they may just tell the attacker where to focus their effort. However, we think it's deeper and broader than that. The models of proof and assurance on which we try to rely have a social aspect, which we can try to understand from other perspectives ranging from the philosophy or sociology of science to the psychology of shared attention. These perspectives suggest, in various ways, how the management of errors and exceptions may be particularly poor. They do not merely relate to failure modes that the designers failed to consider properly or at all; they also relate to failure modes that the designers (or perhaps the verifiers) did not want to consider for institutional and cultural reasons.