The idea of having code accompanied by a proof of tameness usually goes by the name of "proof carrying code". https://en.m.wikipedia.org/wiki/Proof-carrying_code
On October 27, 2019 8:28:04 AM PDT, Giovanni Mascellani <[email protected]> wrote: >Il 27/10/19 10:01, Mario Carneiro ha scritto: >> Of course my programme proposes to prove correctness of "all the >code", >> but as long as there is *any* unverified code on the system you have >to >> be able to protect yourself from it, and that means sandboxing. > >Yes, my (admittedly, somehow tongue-in-cheek) idea is that the whole >ecosystem evolves so that any code is always shipped together with a >proof-of-tameness, that says that that code is going to behave nicely >when you jump in it. So you run your Tor client and download some >program from the worst darknet website, but it comes with a bundled >proof that guarantees that it is going to only access allowed memory >space and only do authorized syscalls through well defined gates >(possibly, provided that there is some way to formalize this in a >trusted way, also that it is not going to take advantage of >microarchitectural attacks like Spectre and co). > >Then, since you trust the specification of "being nice" that such >program proved to be conforming to, you happily run it in ring 0. No >worries even if the code is self-modifying: the "being nice" >specification took this into consideration as well (it is probably not >a >big problem in the specification; if anything, the additional burden is >put on the prover). > >Again, I fully agree that this is an enormous over-engineering: it is >much easier (as we do) to build a processor that enforces privilege >separation. It is just a way to picture in a funny way what extreme >program correctness proving might one day deliver us. > >> I mention this briefly in the paper, but that's actually why the >> verifier is in a separate process; the "small trusted kernel" >approach >> doesn't work unless the language is sufficiently "safe" and >restrictive >> (and verified) that we can prove that "arbitrary" code doesn't >trample >> on the part of the code about which properties of interest are proved >> (the trusted kernel). If it's in a separate process, then the >unverified >> part of the code can throw whatever tantrums it likes but it won't be >> able to influence the verified checker without the OS's say-so. (The >OS >> still has to be trusted in this scenario, though.) > >I agree from the viewpoint of MM0. In my scenario the verification >would >be made by the kernel before the program is even jumped in the first >time. > >Giovanni. >-- >Giovanni Mascellani <[email protected]> >Postdoc researcher - Université Libre de Bruxelles > >-- >You received this message because you are subscribed to the Google >Groups "Metamath" group. >To unsubscribe from this group and stop receiving emails from it, send >an email to [email protected]. >To view this discussion on the web visit >https://groups.google.com/d/msgid/metamath/33bdea08-d5b4-6b60-c495-b71195102725%40gmail.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7B64EEE9-C0D0-4988-8C23-7CC3E640A284%40panix.com.
