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

[Jerry Leichter]

On Jun 5, 2014, at 8:35 AM, Phillip Hallam-Baker <phill at hallambaker.com> wrote:
> 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.
I've used the same problem (in the form "here's an alleged sorting routine; how do you write a test for it that convinces you it's correct") as a interview question for QA people.  Very few get it right without significant prompting.  (In the testing scenario, I can also follow up with questions about performance testing.)

BTW, "monotonically increasing" and "permutation" get tricky if you allow duplicate values in the input - another thing people often forget about.

> 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.
Back in the 1970's, someone wrote an article in SIGPLAN Notices proposing an abstract datatype called a "traversable stack" - details long forgotten, but it was a stack which you could also "walk down".  The datatype wasn't interesting in and of itself; the point was to develop a formal spec from the English description.  The original article had bugs, which were pointed out in a response article - which also had bugs.  There were a whole series of correction articles, one of which I recall had the amusingly honest title "Traversable Stack With Fewer Errors".

> But that does not mean they don't work. Prof Hoare used to say that
> waterfall development methods 'dont work' ... [but t]hey work brilliantly for the consultant looking to extract the maximum rent from their victim.
Indeed.

But when the formal, mathematical world meets the messiness of the real physical world, you have to decide whose standards to use in defining "works".  If you use the standards of the formal, mathematical world - there's no hope.  But if you use the standards of the real world - where we live by "good enough/cheap enough" approximations because nothing else is available - your conclusion might be very different.
                                                        -- Jerry