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

Phillip Hallam-Baker phill at hallambaker.com
Thu Jun 5 08:35:07 EDT 2014


On Wed, Jun 4, 2014 at 5:20 PM, Judson Lester <nyarly at gmail.com> wrote:
> On Wed, Jun 4, 2014 at 10:46 AM, Phillip Hallam-Baker
> <phill at hallambaker.com> wrote:
>> 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.
>
> Sincerely curious: How do you demonstrate that the proof and the code
> are both accurate representations of the specification? I'm thinking
> back to a subverted GCC that was able to protect itself by modifying
> programs as they were built. In other words, how do we know that the
> proof of the specification applies to the proof of the code?

Its easy to show that the proof applies to the code, the validator
will check that.

The hard part is whether the code matches the actual problem which is
the real problem that proving the code matches the specification is
meant to check.

In practice I have not found a proof that the code matches the
specification to be the show stopper, its showing that the
specification actually describes the real world problem.

For example the problem I was given during my interview for a DPhil
place at Oxford: How do you write a specification for a sort. Most
people get that it has to be a monotonically increasing series but
only about 50% remember to specify that the output is a permutation of
the input. Now I had read Tony Hoare's Turing award address so I knew
about that one. But 50% were still failing.

What made me rather disillusioned about formal methods was that
problem, it is much harder for the average programmer to describe
their problem in Z or VDM than in the programming language they are
using.

But that does not mean they don't work. Prof Hoare used to say that
waterfall development methods 'dont work', meaning that you can't
expect to write a perfect specification, implement it perfectly and
then test to see that it solves the problem. The understanding of what
the problem is will change during development. But as I wrote to him a
few months ago, that just means that the waterfall methods don't work
for the customer. They work brilliantly for the consultant looking to
extract the maximum rent from their victim.


More information about the cryptography mailing list