Alleged "microkernel mathematically proven to be bug free"

[Lodewijk andré de la porte]

2014-07-28 18:35 GMT+02:00 Georgi Guninski <guninski at guninski.com>:

> > I have a rough outline for a "cloud computing grid" that verifiably:
>
> verifiably? _really_ provable stuff is a very scarce resource IMHO
> (especially in crypto. do you need crypto? Do you need P \ne NP?).
>

Yes, it needs crypto. I said verifably because "proving" an untamperable
hardware box (IOW: you can only plug it in, nothing else) is what the spec
says it is, is, well, impossible.

You'll depend on some observers, audits and where possibly physical
impossibilities, to show that indeed it is what it is. It's not proof, but
with trust you can verify it.

It's as good as it gets, but no better. I don't think that'd surprise
anyone.

Part of the design involves generations. Eventually you'll have a
generation for which something is questionable in a certain way, nothing to
do about it. Generations will slowly die as the hardware breaks and the
network becomes too small (has too few resources) to uphold anonymity and
fault-tolerance guarantees.

Perhaps a generation will be hybrid with blackbloxes mailed to people and
satellites in space. That generation would be expected to deteriorate fast
in the first 100 years, and then hardly deteriorate at all for many after
that.

All these different grids will have some sort of resource pricing scheme,
that may guarantee a certain runtime, or may be subject to monthly renewals
at new market prices or whatnot. It's a very interesting part of the design.

But yes, the anonymity profits /greatly/ from crypto. Interestingly I think
it could well work without crypto, whereas hardly any other designs could.
It'd lose a lot of convenience though! And P = NP doesn't mean crypto is
useless, just less nice. At the very least there'll be OTPs! Then there may
be (quantum) couple RNGs that can generate secure OTPs. I think there'll
always be ways the newer generations of this idea can continue to function.


> > But it absolutely requires a verified microkernel. I'm *very *excited to
> > see that we're making progress towards it.
>
> Is it really a progress?
> There are assumption free proofs of False
> in most formal proof systems.
>
> Design flaws like \lor instead of \land
> pass the verification process and later are
> considered design flaws, not bugs in proof IMHO.
>
> Knuth quote:
> "Beware of bugs in the above code; I have only proved
> it correct, not tried it."


It's progress, because now all we need is to specify safely, or find a way
to prove specifications. The rest is somewhat, maybe, experimentally
operational. It'll depend on how well we use it, but it is a step in the
right direction!
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/html
Size: 3465 bytes
Desc: not available
URL: <http://lists.cpunks.org/pipermail/cypherpunks/attachments/20140728/e7368d40/attachment-0001.txt>