Skip to content

Commit 4f5f118

Browse files
frawarefraware
committed
Close RC gaps with schema coverage, pilot metrics, and CBMC harness.
1 parent 0e6f44a commit 4f5f118

76 files changed

Lines changed: 2491 additions & 162 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/ci.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ jobs:
2424
run: pytest
2525
- name: Validate intent templates
2626
run: python scripts/validate_templates.py
27+
- name: Validate adapter capabilities
28+
run: python scripts/validate_capabilities.py
2729
- name: Score all benchmark cases
2830
run: python benchmarks/formal_pr_bench/score_all_lanes.py
2931
- name: Score expanded benchmark and publish leaderboard

‎.github/workflows/update-adoption-summary.yml‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
name: Update Adoption Summary
2+
3+
on:
4+
workflow_dispatch:
5+
6+
permissions:
7+
contents: write
8+
9+
env:
10+
OVK_PACKAGE_VERSION: "1.2.0"
11+
12+
jobs:
13+
refresh-adoption-summary:
14+
runs-on: ubuntu-latest
15+
steps:
16+
- uses: actions/checkout@v4
17+
- uses: actions/setup-python@v5
18+
with:
19+
python-version: "3.11"
20+
- name: Install package
21+
run: |
22+
python -m pip install --upgrade pip
23+
pip install -e '.[dev]'
24+
- name: Collect pilot metrics and render adoption summary
25+
run: |
26+
python scripts/collect_pilot_metrics.py \
27+
--pilot-report .verification/pilot-dogfood-report.json \
28+
--source pilot-dogfood \
29+
--ovk-version "${OVK_PACKAGE_VERSION}"
30+
python scripts/render_pilot_metrics.py \
31+
--metrics .verification/pilot-dogfood-report.json \
32+
--registry docs/benchmarks/external-pilots-registry.json
33+
- name: Commit adoption summary when changed
34+
run: |
35+
git config user.name "github-actions[bot]"
36+
git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
37+
git add docs/benchmarks/adoption-summary.json
38+
if git diff --staged --quiet; then
39+
echo "No adoption summary changes to commit"
40+
else
41+
git commit -m "chore: refresh adoption summary from pilot metrics"
42+
git push
43+
fi

‎benchmarks/formal_pr_bench/score_all_lanes.py‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,10 @@ def evaluate_lane_case(case: dict) -> tuple[str, str, str | None]:
5555
"verus-harness-check",
5656
"lean-proof-check",
5757
"cbmc-harness-check",
58+
"cbmc-buffer-bounds",
59+
"cbmc-no-integer-overflow-quota",
60+
"cbmc-no-unchecked-buffer-copy",
61+
"cbmc-no-use-after-free-auth-cache",
5862
"alloy-model-check",
5963
}:
6064
from ovk.core.backend_fixture import evaluate_backend_fixture

‎benchmarks/formal_pr_bench/seed_cases.json‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -289,6 +289,42 @@
289289
"expected_merge_recommendation": "block",
290290
"expected_counterexample_class": "cbmc_assertion_failed"
291291
},
292+
{
293+
"case_id": "cbmc_native_buffer_bounds_pass",
294+
"input_fixture": "examples/backends/cbmc_native_buffer_bounds_pass.json",
295+
"expected_intent": "cbmc-buffer-bounds",
296+
"expected_backend_class": "model_checker",
297+
"expected_status": "pass",
298+
"expected_merge_recommendation": "allow",
299+
"expected_counterexample_class": null
300+
},
301+
{
302+
"case_id": "cbmc_native_integer_overflow_pass",
303+
"input_fixture": "examples/backends/cbmc_native_integer_overflow_pass.json",
304+
"expected_intent": "cbmc-no-integer-overflow-quota",
305+
"expected_backend_class": "model_checker",
306+
"expected_status": "pass",
307+
"expected_merge_recommendation": "allow",
308+
"expected_counterexample_class": null
309+
},
310+
{
311+
"case_id": "cbmc_native_unchecked_copy_pass",
312+
"input_fixture": "examples/backends/cbmc_native_unchecked_copy_pass.json",
313+
"expected_intent": "cbmc-no-unchecked-buffer-copy",
314+
"expected_backend_class": "model_checker",
315+
"expected_status": "pass",
316+
"expected_merge_recommendation": "allow",
317+
"expected_counterexample_class": null
318+
},
319+
{
320+
"case_id": "cbmc_native_uaf_pass",
321+
"input_fixture": "examples/backends/cbmc_native_uaf_pass.json",
322+
"expected_intent": "cbmc-no-use-after-free-auth-cache",
323+
"expected_backend_class": "model_checker",
324+
"expected_status": "pass",
325+
"expected_merge_recommendation": "allow",
326+
"expected_counterexample_class": null
327+
},
292328
{
293329
"case_id": "alloy_pass",
294330
"input_fixture": "examples/backends/alloy_pass.json",

‎benchmarks/formal_pr_bench/seed_cases_expanded.json‎

Lines changed: 72 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -289,6 +289,42 @@
289289
"expected_merge_recommendation": "block",
290290
"expected_counterexample_class": "cbmc_assertion_failed"
291291
},
292+
{
293+
"case_id": "cbmc_native_buffer_bounds_pass",
294+
"input_fixture": "examples/backends/cbmc_native_buffer_bounds_pass.json",
295+
"expected_intent": "cbmc-buffer-bounds",
296+
"expected_backend_class": "model_checker",
297+
"expected_status": "pass",
298+
"expected_merge_recommendation": "allow",
299+
"expected_counterexample_class": null
300+
},
301+
{
302+
"case_id": "cbmc_native_integer_overflow_pass",
303+
"input_fixture": "examples/backends/cbmc_native_integer_overflow_pass.json",
304+
"expected_intent": "cbmc-no-integer-overflow-quota",
305+
"expected_backend_class": "model_checker",
306+
"expected_status": "pass",
307+
"expected_merge_recommendation": "allow",
308+
"expected_counterexample_class": null
309+
},
310+
{
311+
"case_id": "cbmc_native_unchecked_copy_pass",
312+
"input_fixture": "examples/backends/cbmc_native_unchecked_copy_pass.json",
313+
"expected_intent": "cbmc-no-unchecked-buffer-copy",
314+
"expected_backend_class": "model_checker",
315+
"expected_status": "pass",
316+
"expected_merge_recommendation": "allow",
317+
"expected_counterexample_class": null
318+
},
319+
{
320+
"case_id": "cbmc_native_uaf_pass",
321+
"input_fixture": "examples/backends/cbmc_native_uaf_pass.json",
322+
"expected_intent": "cbmc-no-use-after-free-auth-cache",
323+
"expected_backend_class": "model_checker",
324+
"expected_status": "pass",
325+
"expected_merge_recommendation": "allow",
326+
"expected_counterexample_class": null
327+
},
292328
{
293329
"case_id": "alloy_pass",
294330
"input_fixture": "examples/backends/alloy_pass.json",
@@ -595,6 +631,42 @@
595631
"expected_merge_recommendation": "block",
596632
"expected_counterexample_class": "cbmc_assertion_failed"
597633
},
634+
{
635+
"case_id": "cbmc_native_buffer_bounds_pass_variant_1",
636+
"input_fixture": "examples/backends/cbmc_native_buffer_bounds_pass.json",
637+
"expected_intent": "cbmc-buffer-bounds",
638+
"expected_backend_class": "model_checker",
639+
"expected_status": "pass",
640+
"expected_merge_recommendation": "allow",
641+
"expected_counterexample_class": null
642+
},
643+
{
644+
"case_id": "cbmc_native_integer_overflow_pass_variant_1",
645+
"input_fixture": "examples/backends/cbmc_native_integer_overflow_pass.json",
646+
"expected_intent": "cbmc-no-integer-overflow-quota",
647+
"expected_backend_class": "model_checker",
648+
"expected_status": "pass",
649+
"expected_merge_recommendation": "allow",
650+
"expected_counterexample_class": null
651+
},
652+
{
653+
"case_id": "cbmc_native_unchecked_copy_pass_variant_1",
654+
"input_fixture": "examples/backends/cbmc_native_unchecked_copy_pass.json",
655+
"expected_intent": "cbmc-no-unchecked-buffer-copy",
656+
"expected_backend_class": "model_checker",
657+
"expected_status": "pass",
658+
"expected_merge_recommendation": "allow",
659+
"expected_counterexample_class": null
660+
},
661+
{
662+
"case_id": "cbmc_native_uaf_pass_variant_1",
663+
"input_fixture": "examples/backends/cbmc_native_uaf_pass.json",
664+
"expected_intent": "cbmc-no-use-after-free-auth-cache",
665+
"expected_backend_class": "model_checker",
666+
"expected_status": "pass",
667+
"expected_merge_recommendation": "allow",
668+
"expected_counterexample_class": null
669+
},
598670
{
599671
"case_id": "alloy_pass_variant_1",
600672
"input_fixture": "examples/backends/alloy_pass.json",
@@ -828,78 +900,6 @@
828900
"expected_status": "unknown",
829901
"expected_merge_recommendation": "require_human_review",
830902
"expected_counterexample_class": "malformed_input"
831-
},
832-
{
833-
"case_id": "dafny_pass_variant_2",
834-
"input_fixture": "examples/backends/dafny_pass.json",
835-
"expected_intent": "dafny-obligation-check",
836-
"expected_backend_class": "proof_assistant",
837-
"expected_status": "pass",
838-
"expected_merge_recommendation": "allow",
839-
"expected_counterexample_class": null
840-
},
841-
{
842-
"case_id": "dafny_fail_variant_2",
843-
"input_fixture": "examples/backends/dafny_fail.json",
844-
"expected_intent": "dafny-obligation-check",
845-
"expected_backend_class": "proof_assistant",
846-
"expected_status": "fail",
847-
"expected_merge_recommendation": "block",
848-
"expected_counterexample_class": "dafny_obligation_unproved"
849-
},
850-
{
851-
"case_id": "verus_pass_variant_2",
852-
"input_fixture": "examples/backends/verus_pass.json",
853-
"expected_intent": "verus-harness-check",
854-
"expected_backend_class": "proof_assistant",
855-
"expected_status": "pass",
856-
"expected_merge_recommendation": "allow",
857-
"expected_counterexample_class": null
858-
},
859-
{
860-
"case_id": "verus_fail_variant_2",
861-
"input_fixture": "examples/backends/verus_fail.json",
862-
"expected_intent": "verus-harness-check",
863-
"expected_backend_class": "proof_assistant",
864-
"expected_status": "fail",
865-
"expected_merge_recommendation": "block",
866-
"expected_counterexample_class": "verus_proof_failed"
867-
},
868-
{
869-
"case_id": "lean_pass_variant_2",
870-
"input_fixture": "examples/backends/lean_pass.json",
871-
"expected_intent": "lean-proof-check",
872-
"expected_backend_class": "proof_assistant",
873-
"expected_status": "pass",
874-
"expected_merge_recommendation": "allow",
875-
"expected_counterexample_class": null
876-
},
877-
{
878-
"case_id": "lean_fail_variant_2",
879-
"input_fixture": "examples/backends/lean_fail.json",
880-
"expected_intent": "lean-proof-check",
881-
"expected_backend_class": "proof_assistant",
882-
"expected_status": "fail",
883-
"expected_merge_recommendation": "block",
884-
"expected_counterexample_class": "lean_proof_failed"
885-
},
886-
{
887-
"case_id": "cbmc_pass_variant_2",
888-
"input_fixture": "examples/backends/cbmc_pass.json",
889-
"expected_intent": "cbmc-harness-check",
890-
"expected_backend_class": "model_checker",
891-
"expected_status": "pass",
892-
"expected_merge_recommendation": "allow",
893-
"expected_counterexample_class": null
894-
},
895-
{
896-
"case_id": "cbmc_fail_variant_2",
897-
"input_fixture": "examples/backends/cbmc_fail.json",
898-
"expected_intent": "cbmc-harness-check",
899-
"expected_backend_class": "model_checker",
900-
"expected_status": "fail",
901-
"expected_merge_recommendation": "block",
902-
"expected_counterexample_class": "cbmc_assertion_failed"
903903
}
904904
]
905905
}

‎benchmarks/real_diffs/cbmc_integer_overflow_quota.diff‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
diff --git a/src/quota/rate_limit.c b/src/quota/rate_limit.c
2+
new file mode 100644
3+
index 0000000..2222222
4+
--- /dev/null
5+
+++ b/src/quota/rate_limit.c
6+
@@ -0,0 +1,10 @@
7+
+#include <stdint.h>
8+
+
9+
+unsigned int apply_quota(unsigned int used, unsigned int delta) {
10+
+ unsigned int next = used + delta;
11+
+ if (next < used) {
12+
+ return used;
13+
+ }
14+
+ return next;
15+
+}

‎benchmarks/real_diffs/cbmc_use_after_free_auth_cache.diff‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
diff --git a/src/auth/cache.c b/src/auth/cache.c
2+
new file mode 100644
3+
index 0000000..1111111
4+
--- /dev/null
5+
+++ b/src/auth/cache.c
6+
@@ -0,0 +1,12 @@
7+
+#include <stdlib.h>
8+
+
9+
+typedef struct {
10+
+ int *entry;
11+
+} auth_cache_t;
12+
+
13+
+void auth_cache_store(auth_cache_t *cache) {
14+
+ cache->entry = (int *)malloc(sizeof(int));
15+
+ free(cache->entry);
16+
+ *cache->entry = 1;
17+
+}

‎benchmarks/real_diffs/manifest.json‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,28 @@
118118
"expected_lanes": [],
119119
"expected_recommendation": "require_human_review",
120120
"expected_intents": []
121+
},
122+
{
123+
"case_id": "rd_cbmc_use_after_free_auth_cache",
124+
"diff": "cbmc_use_after_free_auth_cache.diff",
125+
"expected_lanes": ["backend"],
126+
"expected_recommendation": "block",
127+
"expected_intents": [
128+
"cbmc-no-use-after-free-auth-cache",
129+
"cbmc-buffer-bounds",
130+
"cbmc-no-unchecked-buffer-copy"
131+
]
132+
},
133+
{
134+
"case_id": "rd_cbmc_integer_overflow_quota",
135+
"diff": "cbmc_integer_overflow_quota.diff",
136+
"expected_lanes": ["backend"],
137+
"expected_recommendation": "block",
138+
"expected_intents": [
139+
"cbmc-no-integer-overflow-quota",
140+
"cbmc-buffer-bounds",
141+
"cbmc-no-unchecked-buffer-copy"
142+
]
121143
}
122144
]
123145
}

‎docs/ARTIFACTS.md‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,15 @@ ovk validate-outputs ovk-bundle
4040

4141
Set `OVK_SIGNING_KEY` for HMAC-SHA256 envelope signing.
4242

43+
## Attestation statement
44+
45+
Schema: in-toto Statement shell with OVK verification predicate — see `schemas/attestation.statement.schema.json`.
46+
47+
Unsigned attestation produced by `bundle_to_statement()`. Validated at write time and by `ovk validate-outputs`.
48+
4349
## Artifact manifest
4450

45-
Schema: `ovk.artifact_manifest.v1`
51+
Schema: `ovk.artifact_manifest.v1` — see `schemas/artifact.manifest.schema.json`.
4652

4753
```json
4854
{
@@ -123,6 +129,6 @@ Use `--root` for portable relative paths in the manifest.
123129

124130
## Validation
125131

126-
`ovk validate-outputs <directory>` schema-checks evidence, quality, provenance, and attestation envelope files. Write-time Pydantic validation applies when runners emit evidence bundles.
132+
`ovk validate-outputs <directory>` schema-checks evidence, attestation statement, artifact manifest, quality, provenance, and attestation envelope files. Write-time Pydantic validation applies when runners emit evidence bundles. `write_release_bundle()` validates the release layout schema before writing artifacts. Release layout schema coverage and adapter capability manifests are required `ovk release-preflight` checks.
127133

128134
Schema index: [SCHEMA_INDEX.md](SCHEMA_INDEX.md).

‎docs/BACKENDS.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Workflow: [`.github/workflows/native-backends-tier1.yml`](../.github/workflows/n
1414
|---------|---------|------------------|
1515
| `opa` | OPA `v0.67.0` static release | Yes |
1616
| `z3` | `z3-solver` Python package `4.13.4.0` | Yes |
17-
| `cbmc` | CBMC Debian `6.4.1` | Binary probe + contract check today; full harness execution planned |
17+
| `cbmc` | CBMC Debian `6.4.1` | Yes — native harness execution for all four data-boundary templates |
1818
| `cedar` | `cedar-policy-cli` `4.8.2` | Yes |
1919

2020
Installer: [`scripts/ci/install_backend.sh`](../scripts/ci/install_backend.sh)
@@ -41,7 +41,7 @@ These use built-in evaluators when binaries are missing. Verification still runs
4141
| `dafny` | `dafny` | Proof obligations | `examples/backends/dafny_*.json` |
4242
| `verus` | `verus` | Verified Rust | `examples/backends/verus_*.json` |
4343
| `lean` | `lean` | Theorem proving | `examples/backends/lean_*.json` |
44-
| `cbmc` | `cbmc` | Bounded C verification | `examples/backends/cbmc_*.json` |
44+
| `cbmc` | `cbmc` | Bounded C verification (native harness) | `examples/backends/cbmc_*.json`, `examples/backends/cbmc_harness/*.c` |
4545
| `alloy` | `alloy` | Relational models | `examples/backends/alloy_*.json` |
4646

4747
## Built-in fallback behavior

0 commit comments

Comments
 (0)