Going through the list of SIGOPS Hall-of-Famers, I came across this paper about proof-carrying codes. However, I don't see these techniques used in practice, and they seem unusable when building at scale?

Is there any reason PCC is not more widely used? Were there security limitations, as this seems like a very attractive idea (code proves that it does not access resources it should not, kind of a more fine-grained Android permission system)? What justifies its inclusion in the Hall-of-Fame in that case?

  • 1
    the paper seems to indicate a 90% performance loss, which was a big deal in 1996. the idea is good, and the link synopis answers your last question: PCC turns out to be a general approach for relocating trust in a system; trust is gained in a component by trusting a proof checker ... rather than trusting the component per se. PCC has become one of the cornerstones of language-based security.
    – dandavis
    Commented Dec 8, 2016 at 21:58
  • That's not quite true. The PCC-program had a higher startup time, but was shown to significantly outperform the alternatives in terms of runtime latency.
    – Jedi
    Commented Dec 8, 2016 at 22:55

1 Answer 1


Ok, so trust is relocated from the component to the proof checker. On what basis can the proof checker's certificate process be trusted?

The proof checker's certification process can be trusted because:

  1. the proof checker defines the safety policy;
  2. the proof checker employs its axioms to validate the safety predicate, and so knows whether the safety predicate meets the conditions of the safety policy, or not;
  3. The proof checker establishes the VC-generation rules, proof rules, and preconditions, (essentially the 'calling convention') that defines how the code consumer invokes the binaries.

Seems all good right? Before any of this happens though, the code consumer defines and publicizes its safety policy.

  1. Do safety policies remains static?
  2. Are safety policies, at any point in time, sufficient with their VC-generation rules, proof rules, and preconditions to certify that safety predicates truly establishes compliant non-malicious code?
  3. Can code producers really certify a safety predicate using first-order logic in polynomial time?

To the first point, if the safety policy is found to be too simplistic, or ineffective lacking the proper axioms, it will change, which means it must be rewritten and republished, which means the code producer must redevelop a safety predicate and safety proof for re-certification.

What code-producer (hoping to have their code re-used in different environments) is going to constantly be recreating safety predicates and redeveloping safety proofs every time someone's safety policy changes, for every possible scenario? The issue of trust is a constraint on the code consumer, not the code producer who may not care if their binaries are trusted.

To the second point, To formulate safety policy, code consumers must make assumptions about what constitutes sufficient conditions to certify a safety predicate. Simply because a safety predicate receives certification, does not mean it is truly safe. Rather, it only means that it has meet the minimal necessary conditions imposed by the code consumers; so some minimal threshold for sufficiency which may not be enough to ensure real safety.

If a code consumer constructs and publishes an ineffective safety policy, the certification process is not providing a sufficient control against malicious code execution. In fact, this model has the code producer abrogating their responsibility for writing trustworthy code, in favour of writing code that merely passes the minimal conditions for certification (i.e. one that produces a minimally acceptable safety predicate).

Finally, to the third point, The author notes "In order to create a safety proof, the code producer must prove a predicate in first-order logic. In general, this problem is undecidable."

If creating a safety proof requires proving a predicate in first-order logic which is 'in general' undecidable this implies the code producer cannot in general create a safety proof - so what good is certification in the first place? Isn't it all merely academic?

There are other problems the authors reference noting in the Introduction that "... there are many difficult problems that remain to be solved." Truly!


You ask Is there any reason PCC is not more widely used?

It sounds like there's very little incentive on the part of code producers to be more widely using this model, given the apparently impossible battle they face in creating a safety proof for their predicate and in having their safety predicate meet conditions of some particular certification process.

  • Great answer. Couldn't "safe" policy creation be template driven, possibly similar to the Android permissions system, where a broad list of actions could be allowed/disallowed? Do you know if PCC has been influential in research on security through formal verification?
    – Jedi
    Commented Dec 28, 2016 at 14:03
  • 'In general' just means 'in the general case'. 'In the general case' 'totality' for an arbitrary function cannot be proven or disproven. But there are a huge number of non-trivial functions that can be proven to be total. Similarly, if code is written to provably conform to a standard (within first order logic) then the proof will fall within a tractable fragment of first order logic. This requires the producer of the code to do the proof. However, this is what money is for. So it sounds doable.
    – JMW
    Commented Jun 9, 2021 at 6:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .