[Cryptography] Security proofs prove non-failproof

Phillip Hallam-Baker phill at hallambaker.com
Thu Feb 23 18:41:39 EST 2017


On Thu, Feb 23, 2017 at 10:33 AM, Patrick Chkoreff <patrick at rayservers.net>
wrote:

> Perry E. Metzger wrote on 02/22/2017 10:07 AM:
>
> >> In addition to empirical testing, I often think in terms of pre- and
> >> post-conditions and loop invariants, which in conjunction with
> >> correctness-preserving code transformations, are in effect a
> >> quasi-formal proof.
> >
> > One popular technique in formal verification is the use of Hoare logic
> > and its descendants, which is where the notion of pre and
> > postconditions comes from.
>
> Yes, I learned the technique by reading Tony Hoare back in the 80s.
>

​Prof Hoare was my college tutor.​



> Basically what I've done is, instead of maintaining a *separate* entity
> called a "proof", I have aimed to make my code itself an ongoing sort of
> proof.  By that I mean whenever I transform the code, I do it in a
> systematic way which, if applied correctly, is guaranteed either to (1)
> maintain the original correct behavior of the code, or (2) alter the
> behavior of the code in a way which is also correct.
>

​Most of it can be automated, the main issue is providing invariants for
loops and arriving at the specification in the first place. Getting a
specification correct is as hard as getting a program correct.

The biggest value I think there is to formal methods is actually in forcing
people to design systems that are simple enough to be tractable. I have
removed about 10,000 lines of code from the Mesh code over the past year by
refining the design.

The tools I use do allow me to code at a very high level, which is very
close to a specification language. My goal is to take the language in which
I specify the problem as close as I can to the structure of the problem
domain.
​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170223/58a002a5/attachment.html>


More information about the cryptography mailing list