2014-07-28 18:35 GMT+02:00 Georgi Guninski <guninski@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!