[Cryptography] Is it mathematically provably impossible to construct a mechanism to test for back doors in programs?

[Phillip Hallam-Baker]

On Wed, Jun 4, 2014 at 1:39 AM, Brian M. Waters <brian at brianmwaters.net> wrote:
> On Sat, 31 May 2014 13:51:43 -0700
> Tony Arcieri <bascule at gmail.com> wrote:
>> I think you should flip the question around and ask how you construct
>> a proof that an algorithm is backdoor free
>
> I think the point of Stephan's halting problem analogy is that you
> can't to this, in the general case.
>
> But I do agree with the following comments that, in the real world, for
> the special case of well-written code, it's possible to use tools (like
> static analysis) and code review arrive at a very high degree of
> confidence, if not an actual proof.
>
> I'm actually very interested in where techniques from the programming
> languages and functional programming communities can take security and
> cryptography in the future. HM-style static types (and dependent types)
> are in some sense a partial step toward formal verification.
>
> I don't think we'll ever live in a world where formal verification (or
> static analysis, or code audits) becomes commonplace in application
> development. However, we're already doing a lot for reusable
> systems-level components like crypto libraries. Will we ever see a day
> when we can *formally verify* these components, or at least parts of
> them?

I have managed to construct formal proofs for very large real world
systems. But my approach is not one that I was able to make generally
usable as I spent my post-doc at CERN working on a network hypertext
system for publishing pictures of cute cats instead.

The way I generated proofs for the ZEUS data acquisition system was to
design a very very high level language that was specific to a task and
then generate the code and the proof together from the specification.


What makes the system work is that these are not specifications in a
generic language, they are specifications in a language for writing
FSRs or Parsers or a routing harness on a parallel processor.

The halting problem is irrelevant to these applications because we
don't have to develop a tool that guarantees to produce a proof of
correctness for every possible or even every valid input. The only
proofs of correctness that matter are the proofs for the code that we
actually generate.


This is the tool for building code generating tools. It is the tool I
used to build the protocol compiler I mentioned in the previous post.

http://sourceforge.net/projects/goedel/