Alleged "microkernel mathematically proven to be bug free"

Cathal (Phone) cathalgarvey at cathalgarvey.me
Mon Jul 28 10:26:53 PDT 2014


Theory-wise, a Turing-complete system can emulate any other turing complete system unless the emulatee has an ace up its sleeve; something unique to the hardware that canot be simulated without breaking authenticity.

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?

On 28 July 2014 18:04:05 GMT+01:00, "Lodewijk andré de la porte" <l at odewijk.nl> wrote:
>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!

-- 
Sent from my Android device with K-9 Mail. Please excuse my brevity.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/html
Size: 4330 bytes
Desc: not available
URL: <http://lists.cpunks.org/pipermail/cypherpunks/attachments/20140728/a3af5d33/attachment-0001.txt>


More information about the cypherpunks mailing list