Alleged "microkernel mathematically proven to be bug free"

[Troy Benjegerdes]

On Mon, Jul 28, 2014 at 06:05:47PM +0200, Lodewijk andré de la porte wrote:
> <3
> 
> I have a rough outline for a "cloud computing grid" that verifiably:
> 
> * Exists on many hardware nodes that can be run by untrusted third parties,
> as the hardware is "tamper evident" and the "cloud computing grid" is self
> healing and distributing.
> * Can run programs in a way that geographic location is unknowable - Onion
> routing, amongst other features, causes programs to seemingly run on every
> node in the network
> * Cannot inspect what runs on it - the microkernel programs cannot read
> what the programs are doing, nor can programs contact one another unless
> they are instances (that potentially run on another hardware node).
> * Is fault tolerant, automatically scaling, etc.
> * Can still be addressed from the Internet or other networks
> 
> You could run something like your Bitcoin wallet in it. It's really
> geodistributed, automatically fault tolerant, etc. There's no way to tamper
> with the programs running, except as specified before a cluster was created.
> 
> Right now you're always stuck with an insane amount of local law, hardware
> issues (and features), fault tolerance, accessibility, etc.
> 
> With this you could run a program in a nigh-perfect vacuum. Your program
> would be networked, but not in any specific place. Nobody can know what it
> does, but it can compute and it can communicate as it wishes. Depending on
> the grid (grids have to be manifactured in one go, checked by several third
> parties, distributed, set and forget) there's some pricing scheme or
> whatnot.
> 
> But it absolutely requires a verified microkernel. I'm *very *excited to
> see that we're making progress towards it.
> 
> 
> If you're a secure kernel developer, Onion routing expert, fantastic C
> coder or technology investor, and this triggered your interests, please
> contact me!

I would be very interested in contract work for running Linux on L4 microkernels.

You can see my experience here https://lkml.org/lkml/1999/3/7/59

But if you give me the code, and I can emulate the hardware with qemu,
I can extract keys/code/whatever from anything running inside the 'secure' 
microkernel. 

If you want the 'tamper evident' hardware it must be open-source hardware
and you will need on the order of at least a million USD to fabricate the 
silicon, and then another million to offer cash prizes at DEFCON for anyone
that can hack the silicon & microkernel.

So if you can secure 2 to 10 million, let's get it done.

Otherwise talking about the theory of a formal-methods 'microkernel' running
on today's buggy broken pre-trojaned hardware is unethical and dangerous.
Do you know what your network card firmware is doing? Neither do I, but I bet
the NSA and Chinese intelligence will have updates for you when the 'secure' 
kernel comes out.

-- 
----------------------------------------------------------------------------
Troy Benjegerdes                 'da hozer'                  hozer at hozed.org
7 elements      earth::water::air::fire::mind::spirit::soul        grid.coop

      Never pick a fight with someone who buys ink by the barrel,
         nor try buy a hacker who makes money by the megahash