Alleged "microkernel mathematically proven to be bug free"

[Lodewijk andré de la porte]

>
> This is probably only *theoretically* possible with quantum computation,
> but it's *practically* possible with tamperproof hardware: TCMs used for
> good instead of evil, maybe?


What I'm planning doesn't have much in the way of uniqueness of hardware.
The only unique thing is.. wait.. shouldn't I patent this first?

The whole hardware device will be as trusted as any TPM would be. And
probably be more trustworthy than any TPM that exists now. 't Is a tricky
thing. The programs run in a vacuum, even they can't know where they run.
That changes the purpose of a "TPM" significantly.

2014-07-28 19:53 GMT+02:00 Troy Benjegerdes <hozer at hozed.org>:

> On Mon, Jul 28, 2014 at 06:05:47PM +0200, Lodewijk andré de la porte wrote:
> > <3
> >
> > 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.
>

There will be need for running software on the secure platform, but I
suspect resources will be so pricy that Linux will be too fat. I'm not
really sure about that left or right, so don't pin me down on it. In tone
with microkernels it would be nice to make wrappers for portions of Linux
APIs, also to ease porting.


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

I'm not entirely sure what you mean by this. At least in my design there is
absolutely no unique (platform) information available, that includes
platform/application keys. If you need them you'll have to make them in
your own userspace.


> 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,


>From what I heard from those that make mining hardware about half a million
is enough. But I'm afraid trustable silicon is only part of the problem.
The trustable silicon will already require some sort of minimalism to allow
for validation, but it gets worse. To prevent data observation the rest of
the casing will have to be able to self-destruct (think harddrives coated
in thermite), and therefore self-observe in known an unknown ways. It also
musn't radiate patterns, which will be exceedingly hard to prove. It will
involve Faraday's cages and the like. Such hardware design is has been
attempted before, but is probably still less effort than the software.


> and then another million to offer cash prizes at DEFCON for anyone
> that can hack the silicon & microkernel.
>

I was thinking of a few millions thrown at companies banks could trust, to
validate proofs, check circuits, observe fabrication, etc. and eventually
undersign responsibility for the validity of the end result.


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

I don't think that'd be enough. It requires a small horde of experts and a
significant support infrastructure. On top of that the idea is exceedingly
hard to convey. The idea that the cloud can be more secure then an in-house
dedicated server is very foreign. It was to me, when I thought it up.

The upside is that the income model is very simple. Just charge for
resources on the computing grids.


> Otherwise talking about the theory of a formal-methods 'microkernel'
> running
> on today's buggy broken pre-trojaned hardware is unethical and dangerous.
>

It's not *that *unethical and dangerous, it just wouldn't work! How can you
claim to stay afloat when you're underwater? The hardware that makes op the
grid will probably be a collection of simplistic components bought in
VHDL-form. These simple, trusted, components will likely be in a shroud of
not-vital components that do some practical stuff, like connecting to the
Internet. Fresh ground to find those stupid patents, too.


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

Are you really prepared to see how deep the rabbit hole goes
<http://www.intel.com/content/www/us/en/intelligent-systems/intel-technology/intel-amt-design-remote-management-even-when-systems-powered-off.html>
?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/html
Size: 6289 bytes
Desc: not available
URL: <https://lists.cpunks.org/pipermail/cypherpunks/attachments/20140728/8e6ad40c/attachment-0001.txt>