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

Brian M. Waters brian at brianmwaters.net
Wed Jun 4 01:39:18 EDT 2014


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?

BW


-- 
Brian M. Waters
Burlington, Vermont, USA
+1 (908) 380-8214
brian at brianmwaters.net
https://brianmwaters.net/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: not available
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20140604/e240c014/attachment.sig>


More information about the cryptography mailing list