I think proof-carrying code is most valuable when it comes to things like firmware updates, where the possible damage that can be done is large, but you also can't sandbox the program and you can't afford to watch it do its thing. I wonder if it's possible to have a closed source PCC? o.O I guess it's not much different from the executable itself - you can have a proof without making it any easier to understand what is going on in the program...
On Sun, Oct 27, 2019 at 11:45 AM Jim Kingdon <[email protected]> wrote: > 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. >> >> -- > 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 > <https://groups.google.com/d/msgid/metamath/7B64EEE9-C0D0-4988-8C23-7CC3E640A284%40panix.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSt6UCVwWq52%2BHKEs%2BRgxB7hdoDdSdEPhPBykNUyzsA3RA%40mail.gmail.com.
