Alleged "microkernel mathematically proven to be bug free"

[Troy Benjegerdes]

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 at 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.