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" <[email protected]> wrote: >2014-07-28 18:35 GMT+02:00 Georgi Guninski <[email protected]>: > >> > 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.
