Proof Carrying Code

PeterLee?'s "An Overview of Proof-Carrying Code" (http://www-2.cs.cmu.edu/~petel/papers/pcc/pcc.html) defines Proof-Carrying Code (PCC) as

: "a technique by which a code consumer (e.g., host) can verify that code provided by an untrusted code producer adheres to a predefined set of safety rules. These rules, also referred to as the safety policy, are chosen by the code consumer in such a way that they are sufficient guarantees for safe behavior of programs. ... The key idea behind proof-carrying code is that the code producer is required to create a formal safety proof that attests to the fact that the code respects the defined safety policy. Then, the code consumer is able to use a simple and fast proof validator to check, with certainty, that the proof is valid and hence the foreign code is safe to execute.

Also see AutomatedTheoremProving.

Contrast with more traditional security concepts which rely on supervision of all accesses to the code consumer's resources during the execution of the code.

Also see JonathanRees?' dissertation "A Security Kernel Based on the LambdaCalculus" (http://mumble.net/jar/pubs/secureos/).

Once an esoteric concept found only in research labs, now ProofCarryingCode is commonplace in the industry

Where?

JavaByteCode is a textbook example of ProofCarryingCode (see SafeVirtualMachine).

No, it is not. Assuring (well, attempting) safe execution in a sandbox is not identical to ProofCarryingCode by any means. Unless the point is supposed to be that Java's sandbox has ProofCarryingCode -- but that would obviously be implementation dependent, and then of course we'd want a pointer to some interesting documentation of such an implementation. I don't see such in the above referenced pages.

Hmm, it may not be ProofCarryingCode in some strict sense, but at least it is a TypedAssemblyLanguage. And isn't the point of ProofCarryingCode, that it can be automatically verified? The JavaByteCodeVerifier? does exactly this.

Automatic verification certainly is the general topic, but there are many kinds of "verification" other than literal proof. There's no need to stretch the terms "proof" and "ProofCarryingCode", you can just say "verification". I don't think this is a nitpick, I think "ProofCarryingCode" means something very, very specific, something that is an excellent idea, but not in wide use yet, whereas some forms of automatic verification are now in wide use. Retaining that important distinction helps keep clear what is, and what is not, current practice versus a laudible future practice.

As I said last year, below, "the state of the art of incorporating proof into programming is far too primitive to be helpful in day to day work, despite how critical it is for people like Knuth, who develop the algorithms the rest of us use. Proof steps aren't even supported in any widely used software environments." Yet it would be nice if they were.

Agreed. ProofCarryingCode really means something like e.g. ProofAnnotationsForBubbleSort. But it is often used in the sense of SelfCertifyingCode. I should probably move those comments there.

"The extreme case of `unbridled' programming arises when we omit all proof steps ". I guess if you fall into that vice you are a CowboyCoder.

If you interview 1000 programmers in Silicon Valley about how often they do any proof steps at all, ever, in their programming, I think the odds are about 95% that all 1000 will say "never". (That is, if you keep repeating such an experiment with randomly chosen programmers, eventually you'll find some positive hits, but they'll be quite rare and certainly non-representative.)

Does that mean that all 1000 are CowboyCoders? It shouldn't, because that devalues the phrase to the point where it means nothing. More likely, it means that, in most areas of pragmatic programming, the state of the art of incorporating proof into programming is far too primitive to be helpful in day to day work, despite how critical it is for people like Knuth, who develop the algorithms the rest of us use. Proof steps aren't even supported in any widely used software environments; that alone should tell you something.

Also see CapabilitySecurityModel, TypedAssemblyLanguage