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:
- the proof checker defines the safety policy;
- 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;
- 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.
- Do safety policies remains static?
- 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?
- 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.