--- license: apache-2.0 pretty_name: CVE Proof Corpus task_categories: - text-classification tags: - formal-verification - proof-carrying-code - security - vulnerability - cve - farkas - static-analysis - program-analysis - memory-safety - heartbleed - smt size_categories: - n<1K configs: - config_name: default data_files: - split: train path: cve-proof-corpus.jsonl --- # CVE Proof Corpus **Six real vulnerability classes, each with a machine-checkable proof that the shipped fix eliminates it — and a checker that shares no code with whatever produced the proof.** Every record carries the safety relation, the guard the upstream project shipped, the declared attacker domain, and the nonnegative multipliers that prove the guard implies safety. All six verify. ```bash pip install "certkit@git+https://github.com/nickharris808/certkit@main" python verify.py ``` ``` VERIFIED curl_ntlm_type3 CVE-2019-3822 2 obligation(s) VERIFIED libpng_rfc1123 CVE-2015-7981 2 obligation(s) VERIFIED libxml2_len_overflow CVE-2015-8317 1 obligation(s) VERIFIED openssl_heartbeat CVE-2014-0160 1 obligation(s) VERIFIED sudo_set_cmnd CVE-2021-3156 1 obligation(s) VERIFIED zlib_inflate_extra CVE-2022-37434 2 obligation(s) 6 of 6 records verified by certkit Every published certificate re-checks against its published spec. ``` That output is a real run. ## 30-second quickstart ```python from datasets import load_dataset corpus = load_dataset("nickh007/cve-proof-corpus", split="train") print(len(corpus), "records") print(corpus[0]["cve"], "-", corpus[0]["relation_in_words"]) ``` No `datasets` install needed either — it is one JSONL file: ```bash pip install "certkit@git+https://github.com/nickharris808/certkit@main" curl -sL https://huggingface.co/datasets/nickh007/cve-proof-corpus/resolve/main/cve-proof-corpus.jsonl -o corpus.jsonl python - <<'EOF' import json from certkit import check_certificate rows = [json.loads(line) for line in open("corpus.jsonl") if line.strip()] for r in rows: print(f"{r['cve']:<16} {check_certificate(r['spec'], r['certificate']).verdict}") EOF ``` ``` CVE-2019-3822 ACCEPTED CVE-2015-7981 ACCEPTED CVE-2015-8317 ACCEPTED CVE-2014-0160 ACCEPTED CVE-2021-3156 ACCEPTED CVE-2022-37434 ACCEPTED ``` Every certificate re-verifies from the published file, by a checker that shares no code with whatever produced it. That is the whole point of the corpus: you do not have to take the proofs on trust, and re-checking takes milliseconds. ## Honest scope **What each record proves:** that the relations transcribed from the fixed check imply the safety property, over the declared domain. The certificate is a Farkas refutation and it is exact. **What it does not prove:** - **Not that the project is secure.** The relations are a model a human wrote from reading the fix. A correct proof about a wrong model is still a wrong result, and nothing here reads source code. - **Not machine-word arithmetic.** The atoms are relations over the mathematical integers. A proof says nothing about a path where the real arithmetic wraps. - **Not a survey.** Six classes are six classes. This is not a statistical claim about real code. - **Nothing about current versions.** Every CVE here is historical and fixed. No record is a statement about any software you might be running today. ## Why this exists Proof-carrying security work usually publishes *conclusions* — "we verified it" — which a reader has no way to check. This corpus publishes the **proofs**, in a format small enough to re-verify with a checker you can read in an afternoon. The relations are the real ones. `openssl_heartbeat` is the CVE-2014-0160 length relation, not a paraphrase or a toy analogue. Six classes across six ecosystems and two weakness families. ## Contents | id | CVE | Project | CWE | Weakness | Safety conjuncts | |---|---|---|---|---|---| | `openssl_heartbeat` | CVE-2014-0160 (Heartbleed) | OpenSSL | CWE-125 | out-of-bounds read | 1 | | `libxml2_len_overflow` | CVE-2015-8317 | libxml2 | CWE-125 | out-of-bounds read | 1 | | `zlib_inflate_extra` | CVE-2022-37434 | zlib | CWE-787 | out-of-bounds write | 2 | | `libpng_rfc1123` | CVE-2015-7981 | libpng | CWE-125 | out-of-bounds read | 2 | | `sudo_set_cmnd` | CVE-2021-3156 (Baron Samedit) | sudo | CWE-787 | heap OOB write | 1 | | `curl_ntlm_type3` | CVE-2019-3822 | curl | CWE-787 | stack OOB write | 2 | ## Schema One JSON object per line. | Field | Type | Meaning | |---|---|---| | `schema` | string | `cve-proof-corpus/v1` | | `id` | string | stable class identifier | | `cve` | string | upstream CVE identifier | | `common_name` | string | the name people actually use (e.g. "Heartbleed") | | `project` | string | upstream project | | `cwe` | string | weakness classification | | `weakness` | string | plain-English weakness type | | `relation_in_words` | string | what the safety relation means, in one sentence | | `variables` | list[string] | the variables the relations range over | | `spec` | object | a `certkit/spec/v1` object: `domain`, `guard`, `safety`, `fingerprint` | | `certificate` | object | a `certkit/farkas/v1` object: multipliers per obligation | | `n_safety_conjuncts` | int | number of obligations | | `n_domain_atoms` | int | size of the declared domain | | `n_guard_atoms` | int | size of the shipped guard | | `has_certificate` | bool | whether every obligation carries multipliers | An **atom** is a linear relation in canonical form, with exact rational coefficients encoded as `[numerator, denominator]` pairs: ```json {"coeff": {"hb_payload": [1, 1], "hb_record_len": [-1, 1]}, "const": [19, 1], "strict": false} ``` meaning `hb_payload - hb_record_len + 19 <= 0`, i.e. `19 + payload <= record_len`. ## The obligation model The claim for each record is: **within `domain`, `guard` implies `safety`.** `safety` is a conjunction, so its negation is a disjunction — which is not a single atom list. So there is **one obligation per safety conjunct**, and obligation `i` is the atom list ``` domain ++ guard ++ [negate(safety[i])] ``` in exactly that order. Multiplier indices refer to positions in *that reconstructed list*, not to anything the certificate carries. The property holds only if every obligation is refuted. ## Usage ```python from loader import load_corpus, to_certkit from certkit import check_certificate for rec in load_corpus(): spec, cert = to_certkit(rec) report = check_certificate(spec, cert) print(rec["cve"], "->", "VERIFIED" if report.ok else "FAILED") ``` With `datasets`: ```python from datasets import load_dataset ds = load_dataset("json", data_files="cve-proof-corpus.jsonl", split="train") print(ds[0]["cve"], ds[0]["relation_in_words"]) ``` ## Integrity — the file, by hash ``` cve-proof-corpus.jsonl sha256 522992a91026ff08b33356c5641fa21eeef23f7ee148f209f491cea347261e47 6 records, one JSON object per line ``` Recompute it with `shasum -a 256 cve-proof-corpus.jsonl`. If it differs from the line above, you are not looking at the corpus this card describes, and nothing else on this page applies to what you have. ## The negative control — watch the checker refuse A corpus of things that pass tells you nothing about whether the checker can fail. This one ships with the control beside it: ```bash python verify.py # 6 of 6 verified, exit 0 ``` Now break one and watch it refuse. Change any single multiplier in any record — the proof is the multiplier set, so this is the smallest possible tamper: ```bash python - <<'EOF' import json recs = [json.loads(l) for l in open("cve-proof-corpus.jsonl") if l.strip()] ob = recs[0]["certificate"]["obligations"][0]["multipliers"] k = next(iter(ob)); ob[k] = [int(ob[k][0]) + 1, ob[k][1]] # one multiplier, off by one open("tampered.jsonl", "w").write("\n".join(json.dumps(r) for r in recs) + "\n") EOF python verify.py --data tampered.jsonl # FAILS, exit 1 ``` That second run is a real one, not an illustration. It prints: ``` FAILED: curl_ntlm_type3 FAILED curl_ntlm_type3 CVE-2019-3822 2 obligation(s) obligation 0: variables did not cancel: cu_ntresplen, cu_size VERIFIED libpng_rfc1123 CVE-2015-7981 2 obligation(s) ... 5 of 6 records verified by certkit ``` Note what the failure says: the multipliers no longer make the variables cancel. That is the whole check — nonnegative multipliers that combine the guard with the negated safety property so every variable disappears and an impossible constant remains. Move one and the arithmetic stops closing. The checker rebuilds each obligation from the published spec and ignores whatever atoms the certificate carries, so a certificate that proves some easier unrelated system cannot pass either. A checker that accepted the tampered file would be worth nothing, and you should not take that on trust from a card — the two commands above are the whole argument, and they run in ten seconds. ## Provenance Exported by `export.py` from a specification manifest and its Farkas certificates. The manifest encodes each CVE's bounds relation as small integer inequalities; the certificates were produced by a solver-free decision procedure that is **not** part of this release. That asymmetry is deliberate and is the reason the corpus is publishable at all: **producing** these certificates is the hard part, and **checking** them is cheap enough that you need not trust us. Re-run `export.py --repo-root ` to regenerate, and `verify.py` to re-check. ## Limitations - **Six classes is a small corpus.** It is a demonstration that the format carries real relations, not a statistical sample of anything. - **Quantifier-free linear integer arithmetic only.** These are bounds and length relations. Nothing here involves the heap shape, aliasing, or nonlinear arithmetic. - **A proof about a relation, not about a program.** Each record proves the guard implies the stated bounds relation over the declared domain. It does **not** prove the upstream project is free of other defects, nor that the relation captures every safety requirement of that code path. The relation is stated explicitly so you can judge that yourself. - **The domain is declared, not inferred.** A conclusion holds over the domain in the record and says nothing outside it. - **Fingerprints detect drift, not forgery.** The `spec.fingerprint` binds a certificate to a spec and catches accidental mismatch. A deliberate forger would edit the spec and recompute it — soundness rests on a human reading the relations, which is why they are kept small. ## The rest of the toolkit | | | |---|---| | **[certkit](https://github.com/nickharris808/certkit)** | the checker that verifies this corpus | | **[exploit-counter](https://github.com/nickharris808/exploit-counter)** | how many states an unsound guard admits | | **[crs-mcp](https://github.com/nickharris808/crs-mcp)** | the verdict surface AI agents call | | **[soundnessbench](https://github.com/nickharris808/soundnessbench)** | the benchmark that grades soundness tools | | **[Try it in your browser](https://huggingface.co/spaces/nickh007/certkit-demo)** | re-verify all six live, no install | ## Citation `CITATION.cff` ships beside this card. In text: ```bibtex @misc{cve_proof_corpus, title = {CVE Proof Corpus: six vulnerability classes with machine-checkable soundness proofs}, author = {Harris, Nick}, year = {2026}, note = {Apache-2.0. sha256 of cve-proof-corpus.jsonl: 522992a91026ff08b33356c5641fa21eeef23f7ee148f209f491cea347261e47}, url = {https://huggingface.co/datasets/nickh007/cve-proof-corpus} } ``` ## License Apache-2.0. The CVE identifiers and upstream relations are public facts; the encoding and certificates are released for copying and re-verification. --- Part of **[certified discovery](https://nickharris808.github.io/certified-discovery/)** — ten artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted.