#### Re: "Math is hard"

And how can you know that the code you just wrote is secure if you cannot produce a mathematical proof that it is secure?
It's not quite that hopeless. I expect that there are engineering practices which can be put in place that will allow secure code to be produced. Those practices must be developed by mathematicians (they will be called "computer scientists"), and strictly enforced to work, however.

I will just address a dangerous and incorrect inference that many will make from your statement: "the code you just wrote is secure if [you can] produce a mathematical proof that it is secure".

For many will assume that mathematically rigorous code is secure.

Mathematical correctness is a necessary condition, but not sufficient.

1) From a mathematical point of view, proven code is demonstrated to follow rigorously from a set of assumptions. The first challenge is making sure that *all* your assumptions are valid and apply to the 'real' world. This page on the formally proven seL4 microkernel goes into more depth: seL4 - What we prove...what we assume. There is a telling quotation there: "Mathematical proof is proof as long as it talks about formal concepts. *It is when assumptions connect to reality where things may still fail.* Albert Einstein is quoted as saying 'As far as the laws of mathematics refer to reality, they are not certain; and as far as they are certain, they do not refer to reality.'", which leads on to...

2) While the algorithm may be demonstrated to be secure under the chosen set of assumptions, it is implemented on real world hardware, which is subject to side-channel attack, e.g. timing attacks, power-fuzzing and a panoply of other techniques. AES is a pretty well proven encryption algorithm but difficult to implement in a secure manner *in silico* ( Cache Based Remote Timing Attack on the AES ). There are decades of work, some of which is either not classified, or now unclassified dealing with working with EAL/Common Criteria and equivalent security requirements and the hardware issues that have to be resolved.

3) The hardware your code is implemented on can be compromised in subtle ways, even at the gate level (Stealthy dopant-level hardware Trojans: Extended version : April 2014Journal of Cryptographic Engineering 4(1):19-31 : DOI: 10.1007/s13389-013-0068-0 ). Bullet-proof code can be compromised by tissue-paper hardware. If you cannot trust the hardware your code is running on, it makes it difficult to claim your system is secure, even if the code itself is formally proven.

There are indeed engineering practices that can mitigate many of the known security vulnerabilities. TEMPEST is one such set of practices which may or may not be over the top for most people.

A formally proven piece of code is only one step on the long path to secure information processing.

NN

Addendum

1a) One person's experience of use of formal verification is here.

Ray Wang: Formal Verification: The Gap Between Perfect Code and Reality

tl;dr Formal Verification is *hard*, and there are plenty of examples of it going wrong.

That said, from my point of view, formal verification is obviously useful, and is used in many areas (including chip design and cryptocurrency), but has not made inroads into general-purpose computing as yet. And formal verification is only part of the story: it is all well and good showing that the program correctly implements the specification; but humans write the specification, and there is a great deal of room for specifications to be incomplete and/or inaccurate.