An implementation of a verification condition generator for foundational proof-carrying code
Bibliographic record
Abstract
Proof-carrying code (PCC) is a technique that addresses the problem of mobile code safety. It is a mechanism in which a code producer provides both code and a proof certifying that the code will run safely on a code consumer's machine. The code consumer or the host system will validate the proof against a safety policy before executing the source code. Foundational proof-carrying code (FPCC) aims to minimize the amount of code that must be trusted (the “trusted computing base” or TCB) with the goal of providing more flexibility and increased security. In both PCC and FPCC, the verification-condition generator (VCG) constructs the statement of the safety theorem from the source code, and is an important part of the TCB. This paper presents an implementation of a VCG based on a sound set of Hoare-style rules for machine instructions in the context of FPCC. The implementation in OCaml is described and examples illustrating the approach are given. The output of our VCG is a list of verification conditions that are directly inserted into a proof script that serves as input to the Coq proof assistant, and represents an important part of the safety proofs of our programs. We also present examples showing how these verification conditions are used to complete the proofs of safety. This work represents an important step in automating proofs for PCC.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.004 | 0.016 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.002 |
| Scholarly communication | 0.002 | 0.003 |
| Open science | 0.003 | 0.002 |
| Research integrity | 0.002 | 0.003 |
| Insufficient payload (model declined to judge) | 0.015 | 0.005 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".