[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

Christian Huitema huitema at huitema.net
Thu Mar 17 01:07:33 EDT 2016


On Wednesday, March 16, 2016 7:01 PM, Perry wrote:
> ...
> Most, no, but I've become a convert to formal methods in the last few
> years. Until quite recently it was impossible to do real formal
> verification work on programs of significant size, but that has
> completely changed.

I am not sure that formal method are such a break from the current state of the art.

Formal methods end up declaring what the code should do, using pre-conditions for the input variables and statements of invariants for the outcome. That's good, but at some level it is comparable to what can be done with the combination of static code analyzers and real time assertions. 

C/C++ extensions like SAL Annotations make static code analyzers really powerful. If developers use SAL honestly, the code analyzers will definitely catch have Heart Bleed or Go To Fail bugs. Adding ASSERT statements liberally expresses a lot about code intent, and will catch potential issues during a debug break.

Of course, true formal development if applicable will be somewhat better than C + SAL + ASSERT. ASSERT are too costly to be compiled in the production code. They are only activated in special debug builds, and thus can only detect issues encountered during debug runs. There are classes of bugs that are not found by static analysis. They tend to be arcane, something like "use after free during a race condition." Formal development and "annotated analysis" are different. But there are enough similarities. It is probably a continuum.

-- Christian Huitema





More information about the cryptography mailing list