[IsThisObvious]

I help write microcontroller code for pressure equipment management. If something goes sufficiently wrong in heating/fails to properly vent, an explosion can occur, endangering everyone in the area.

Even unrelated code is heavily audited to make sure that it can't somehow impact the main control loop and cause an invalid state.

Cryptography software should be much the same.

[jlgreco]

With normal software you can load up on the unit and integration tests to make yourself more confident with your software. When the concern is with the integrity of a cryptographic system, things are not quite so simple. You can write tests, sure, but your overall confidence afterwards is going to be much different.

[IsThisObvious]

We go beyond unit tests to verify that the algorithms can't create certain states by any execution path, etc.

Formal verification of software properties is an interesting field.

[DanBC]

A blog post about the process would be fascinating, and probably something that many on HN would be interested in.

[foobarqux]

The problem is no one would volunteer to write crypto code under those constraints.

[IsThisObvious]

I know people who write crypto software that must conform to formal verification of the algorithm, requires detailed design documentation before a single line of code, etc.

[z-factor]

Funny thing is that code is then compiled with a compiler was not formally verified, so it's still a 'fingers crossed' situation.

[IsThisObvious]

The code generator we use (at my job; not crypto) was written in Coq and formally verified to generate code with certain properties, given properties of the input.

I assume that the crypto group I know, who developed most of the code generator I use, takes similar measures to make sure that their verified "theorems" translate correctly to code.

The unverified stage is actually the hardware, which is an open problem.

[foobarqux]

I think in many regulated industries Coq itself would also need to be certified.

What industry is this?

[IsThisObvious]

Pressure equipment, specifically sort of mid-scale items for laboratory and small-batch use.

Our low level code (ie, directly controlling machines) is written in the SPARK environment. This code tends not to get updated often, and has a high level of verification to it. It's what actually handles the pressure cut-offs (ie, hard limits on the machine), turning vales, etc.

Our middleware code is based on a specially developed VM that gets code generated for it in Coq, to ensure that it doesn't choke or become unresponsive. However, it's not directly responsible for safety control and has somewhat laxer restrictions.

Coq is useful for demonstrating that the middleware analytics will complete in a given time profile and not crash out the server on erroneous input.

[jdiez17]

Right, but it's much less of a leap of faith, IMHO. Besides, if you turn off optimisations you can be reasonably sure the compiler didn't do something unintended.

[foobarqux]

I meant volunteer to mean "not get paid".