[kani] Validate complete proof result inventory - #3662
Conversation
|
You have reached your Codex usage limits for security reviews. Please try again later. |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
Reviewer guide: exact scopeThis follow-up checks one fresh, unfiltered Kani 0.67 run. Before trusting its inventory, it requires Kani’s exact six-field metadata root, The result parser accepts only the complete-run property-class vocabulary observed in the authentic Kani 0.67 zerocopy corpus (23 classes), rejects duplicate full property identifiers, and rejects C0/DEL controls in harness names. It also rejects malformed, stale, duplicate, symlinked, non-finite, or otherwise ambiguous artifacts. Non-goals: This is not an independent source manifest. If source code deletes a harness—or deletes one cover while another remains—both emitted inventories can agree while the obligation disappears. The parser is deliberately pinned to the audited Kani 0.67 corpus and requires a complete-corpus re-audit on upgrades or newly observed property classes. It does not strengthen Kani’s Rust/UB model, and the canonical CI invocation supplies no harness/test-selection options. Evidence: 51 checker tests pass, including adversarial cases; each new exploit case passed the pre-fix checker and now fails closed. The full pinned run verified 332/332 harnesses and found all 896 emitted cover properties Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
@codex review Please review exact current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7509f06e31
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| expected = {} | ||
| for key in ("proof_harnesses", "test_harnesses"): | ||
| harnesses = data.get(key) | ||
| if not isinstance(harnesses, list): |
There was a problem hiding this comment.
If the sole metadata artifact is partial or belongs to the wrong crate but still contains proof_harnesses and test_harnesses, the checker accepts it because only those two fields are inspected; even crate_name may be missing or malformed. Matching result files can therefore produce a successful validation without establishing that this is complete Kani 0.67 metadata for zerocopy. Require the pinned schema’s mandatory root fields and the expected crate identity before trusting the harness inventory.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 16c135c0c726de6f4937550c12ef9404aff27a64. _validate_metadata_root now requires the exact six-field Kani 0.67 root, zerocopy root and nested proof-harness crate identities, a nonempty proof list, an empty test list, null autoharness metadata, and array types for the remaining list fields. The adversarial partial/wrong-crate artifacts passed the pre-fix checker and now fail closed; all 51 checker tests pass.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| while cursor < len(lines): | ||
| if lines[cursor].startswith("Check "): | ||
| check, cursor = _parse_check(lines, cursor, len(checks) + 1, path) | ||
| checks.append(check) |
There was a problem hiding this comment.
When a malformed result repeats the same property name, each copy is appended independently and counted in the reconstructed summaries. For example, two SATISFIED records named harness.cover.1 with a 2 of 2 cover summary pass validation, even though Kani property identifiers represent distinct inventory entries; such duplication can replace an omitted record while preserving all checked counts. Track parsed property names per harness and reject repeats.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 16c135c0c726de6f4937550c12ef9404aff27a64. The result parser now tracks complete property names per harness and rejects a duplicate before accepting reconstructed summaries. The replacement-by-duplicate exploit passed the pre-fix checker and now fails closed; all 51 checker tests pass.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| expected = {} | ||
| for key in ("proof_harnesses", "test_harnesses"): | ||
| harnesses = data.get(key) |
There was a problem hiding this comment.
When proof_harnesses is empty but test_harnesses contains a covered entry, this loop populates expected and the checker reports success. The canonical runner rejects --tests and the documentation says test harnesses are not enabled, so a malformed or wrongly selected artifact can lose the entire proof inventory yet pass by supplying only test results. Require a nonempty proof-harness list and an empty test-harness list separately for this protocol.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 16c135c0c726de6f4937550c12ef9404aff27a64. Proof and test inventories are now validated independently: proof harnesses must be a nonempty array, test harnesses must be an empty array, and expected results are built only from proof harnesses. The test-only artifact passed the pre-fix checker and now fails closed; all 51 checker tests pass.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| if PROPERTY_CLASS_RE.fullmatch(property_class) is None: | ||
| raise ValidationError( | ||
| f"{path}:{line_number}: malformed Kani property class {property_class!r}" | ||
| ) | ||
| _canonical_uint(property_id, U32_MAX, "Kani property id", path, line_number) | ||
| return property_class |
There was a problem hiding this comment.
The class parser accepts any lowercase, underscore, or hyphen sequence rather than the property classes emitted by the pinned Kani 0.67 toolchain. Consequently, a result containing a fabricated record such as harness.not_a_kani_class.1 with SUCCESS and a matching normal summary passes whenever the run also has a valid cover, even though the artifact is outside the audited grammar. Enumerate the pinned class vocabulary or otherwise reject unrecognized classes so format drift and corruption fail closed.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 16c135c0c726de6f4937550c12ef9404aff27a64. Property classes must now belong to the exact 23-class vocabulary observed in the authentic complete zerocopy Kani 0.67 corpus. Even known but unobserved variants remain rejected until a complete-corpus re-audit. The fabricated-class artifact passed the pre-fix checker and now fails closed; all 51 checker tests pass.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| name = harness.get("pretty_name") | ||
| if not isinstance(name, str) or not name: | ||
| raise ValidationError( | ||
| f"{metadata_path}: {key}[{index}].pretty_name is not a nonempty string" | ||
| ) | ||
| parsed_name = PurePosixPath(name) |
There was a problem hiding this comment.
A metadata pretty_name containing a newline, tab, or DEL character passes these checks, and a correspondingly named regular result file is accepted as an inventory entry. Rust/Kani harness names cannot canonically contain such controls, so this permits malformed metadata and ambiguous filenames or diagnostics to pass the supposedly version-pinned parser. Apply the same control-character rejection used for property names before converting the harness name into a path.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 16c135c0c726de6f4937550c12ef9404aff27a64. Metadata harness names now reject every C0 control and DEL before path conversion. New newline, tab, and DEL cases passed the pre-fix checker and now fail closed; all 51 checker tests pass.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
7509f06 to
4d90a86
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gwnposbjq4xdjjy5mrhghubvvni5syc2m #3662 +/- ##
====================================================================
Coverage ? 91.89%
====================================================================
Files ? 20
Lines ? 6118
Branches ? 0
====================================================================
Hits ? 5622
Misses ? 496
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
4d90a86 to
16c135c
Compare
|
@codex review Please review exact current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 16c135c0c7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
|
|
||
| def _contains_control_characters(value): | ||
| return any(ord(character) < 0x20 or ord(character) == 0x7F for character in value) |
There was a problem hiding this comment.
When a malformed metadata pretty_name or result property identifier contains a C1 control such as U+0085, this helper returns false because it checks only C0 and DEL; a matching filename/result then passes the complete validator even though that character cannot occur in a canonical Rust/Kani identifier. Fresh evidence in the current head is that the new helper still permits the entire U+0080–U+009F range, so extend it with 0x80 <= ord(character) <= 0x9F (and add a fixture for one of these controls).
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Addressed on exact head 16ec4d06b0b1a4f7208a5b29e54ec5c7f74fc8f3. The raw-result and decoded-name checks now reject C1 controls in addition to C0/DEL; only the structural tab and line-feed characters are admitted in raw output. Regression tests cover controls in property names, descriptions, locations, and harness names. The complete parser suite passes all 54 tests.
| FAILURE_LOCATION_RE = re.compile(r' File: "(.*)", line (0|[1-9][0-9]*), in (.*)') | ||
| # `Duration::as_secs_f32()` is rendered with Rust's ordinary `Display`, not | ||
| # exponential formatting. `Display` omits redundant leading/trailing zeroes. | ||
| TIME_RE = re.compile(r"Verification Time: (?:0|[1-9][0-9]*)(?:\.[0-9]*[1-9])?s") |
There was a problem hiding this comment.
If a forged or corrupted footer contains an arbitrarily large canonical-looking decimal, such as Verification Time: 999999999999999999999999999999999999999999s, this regex accepts it and the complete checker reports success. Kani renders Duration::as_secs_f32(), so values above the rendered Duration::MAX cannot be produced by Kani 0.67; parse and bound the token (and add an above-maximum fixture) rather than validating only its decimal shape.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Addressed on exact head 16ec4d06b0b1a4f7208a5b29e54ec5c7f74fc8f3. The verification-time field now has Decimal-based necessary bounds: zero or at least one nanosecond, no greater than 2^64 seconds, and at most nine significant decimal digits. Boundary and rejection tests were added. The documentation deliberately calls this a numeric envelope for the informational field, not an exact inverse of the binary32 shortest-decimal renderer; values inside the envelope are not claimed to authenticate the renderer.
| CHECK_RE = re.compile(r"Check ([1-9][0-9]*): (.+)") | ||
| THREAD_RE = re.compile(r"Thread (0|[1-9][0-9]*):") | ||
| STATUS_RE = re.compile(r"\t - Status: ([A-Z]+)") | ||
| LOCATION_RE = re.compile(r"\t - Location: (.+)") |
There was a problem hiding this comment.
When a corrupted check record uses any nonempty location payload, for example \t - Location: definitely not a Kani location, this regex accepts it and the full artifact validates successfully. Kani 0.67's regular renderer emits a structured source location containing the file, canonical line and column, and function, so parse that pinned shape instead of treating arbitrary text as a valid optional location.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Addressed on exact head 16ec4d06b0b1a4f7208a5b29e54ec5c7f74fc8f3. I retained an opaque nonempty location payload rather than imposing a Rust file:line:column grammar: the pinned Kani SourceLocation representation permits optional string components, including a file-only value. The matcher is now named LOCATION_ENVELOPE_RE, its limited claim is documented, and tests cover file-only, partial, full, unknown-file/function, and generated-file forms. Framing and control-character rejection remain enforced; the location is not consumed as proof evidence.
301fcf7 to
39312f0
Compare
Kani 0.67 excludes cover properties from its overall success result. Run the unfiltered suite once into a fresh target, then validate the exact metadata/result inventory and every cover-class record with a version-pinned, fail-closed parser. Keep the parser auditable with adversarial fixtures and document both its output-format premises and its source-coverage non-goals. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G868f72aa79c4e2c0240a06b3f1151fc9
39312f0 to
2eb935e
Compare
16c135c to
16ec4d0
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Something went wrong. Try again later by commenting “@codex review”. ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
2 participants
Kani 0.67 excludes cover properties from its overall success result. Run the unfiltered suite once into a fresh target, then validate the exact metadata/result inventory and every cover-class record with a version-pinned, fail-closed parser.
Keep the parser auditable with adversarial fixtures and document both its output-format premises and its source-coverage non-goals.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G868f72aa79c4e2c0240a06b3f1151fc9 && git checkout -b pr-G868f72aa79c4e2c0240a06b3f1151fc9 FETCH_HEADCheckout
git fetch origin refs/heads/G868f72aa79c4e2c0240a06b3f1151fc9 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G868f72aa79c4e2c0240a06b3f1151fc9 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.