On Tue, Jul 29, 2014 at 06:36:19PM +0200, Lodewijk andré de la porte wrote:
On Jul 29, 2014 6:14 PM, "Georgi Guninski" <guninski@guninski.com> wrote:
These proofs tie a meta-specification to the actual code. Look into the sort of proofs they use. Basically they're saying "the code does what we said it has to. Only if we accidentally told it to go skynet on us, it
will
work perfectly". Things like segfaults would be pretty clearly not as specified.
By browsing the proofs, I have the impression they don't depend on the C code (and Isabelle parsing C appears not very trivial, though possible).
If I backdoor the C code of the kernel, will the proof fail?
Isn't that the whole idea? It would really change the thing up if there's a backdoor!
/* * Copyright 2014 under AGPLv3, Troy Benjegerdes, <add your name> * as a derivative work of http://q3u.be/patent/q3ube * claim 9, A process for producing a new physical computer hardware design * utilizing a software program running on an existing design that contains all * software and specifications to produce a derivative physical design. * (recursive hardware) */ Well, technically, I suspect the proof would never complete running because the hash signature(s) of the backdoored kernel will not match the signature etched in silicon on the open-source hardware, and it will immediately wipe any crypto keys when there is a kernel hash check failure. Of course, if you fix any of the backdoors that existed when the silicon mask was generated the hash check will fail too. C'est la vie /* * end copyright notice */ You'll need to hurry up and get your backdoors in kernels, compilers, and EDA tools before we get this implemented. I think you've got 5-15 years yet before that window closes. Eventually I predict various intelligence agencies will eventually work together to validate the trusted open-source hardware, either because they actually understand the value, or because activist hacker groups rewrite their legislative funding mandates using existing backdoors. Lodewijk, please write this stuff down (preferably as patent claims) so we have the original open-source hardware prior art documented and protected before some corporate IP pirates find it.