[kani] Prove zero-only pointer validation - #3652
Conversation
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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G56sp4dsuukjpe3trlzhqbkuvl6f53jkg #3652 +/- ##
==================================================================
Coverage 91.89% 91.89%
==================================================================
Files 20 20
Lines 6118 6118
==================================================================
Hits 5622 5622
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
e8753b0 to
88a28f5
Compare
3a882af to
0e35235
Compare
88a28f5 to
82d27ac
Compare
0e35235 to
61ff28d
Compare
82d27ac to
c0a2e4c
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
![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: c0a2e4c68c
ℹ️ 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".
| // produces `Option::<T>::None`. | ||
| macro_rules! zero_only_pointer_proof { | ||
| ($proof:ident, $ty:ty, $value:ident => $assertion:expr) => { | ||
| #[kani::proof] |
There was a problem hiding this comment.
On the 64-bit Kani CI target, each generated harness reaches pointer::is_zeroed, which iterates over all eight pointer bytes, but these proofs have no #[kani::unwind(...)] bound. Kani's default bound is insufficient for the all-zero path to complete, so the unwinding assertion fails instead of establishing the documented domain; the existing four-byte array proof above uses #[kani::unwind(5)] for this reason. Add a bound sufficient for the pointer-size loop (nine on the current target) to the generated harnesses.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Every generated pointer harness now has #[kani::unwind(9)], which covers the eight-byte pointer scan on the verified 64-bit target, and the focused pointer proof passes with unwinding assertions enabled.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| // Excludes: This does not claim that rejected nonzero bytes are invalid | ||
| // Rust pointers. It also excludes provenance, fat pointers, other pointees, | ||
| // function signatures and ABIs, and non-Kani targets. |
There was a problem hiding this comment.
The exclusions mention provenance but omit Kani's incomplete checking of invalid Rust values, which is material here because the public read path materializes raw-pointer and niche-pointer values before the safe observations run. If that path regresses and constructs an invalid Option<&mut _>, function pointer, or Box representation, Kani is not a complete oracle for the resulting immediate UB, so this proof cannot establish that obligation even though it starts from initialized bytes. Add invalid-value checking to the stated soundness boundary rather than presenting the listed exclusions as complete.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The exclusions now call out incomplete invalid-value checking in Kani. In addition, arbitrary bytes are passed only to the raw non-materializing validator; the public read is invoked solely for independently safe null/None witnesses, so these harnesses no longer materialize public values based on the validator under test.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
2d90423 to
cc19271
Compare
c0a2e4c to
48967ac
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 48967acdf5
ℹ️ 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".
| // Domain: Every initialized eight-byte source sequence for the thin | ||
| // pointer-bearing monomorphizations below. Eight bytes is the pointer size | ||
| // of the common 64-bit Kani CI target documented above. |
There was a problem hiding this comment.
When this harness is audited or its Kani configuration changes, the stated domain does not disclose its allocation or assumption bounds, and it leaves readers to infer the eight-iteration scan and why unwind 9 is sufficient from the implementation. The repository’s formal-verification guidance requires each of those dimensions to be documented independently; add an explicit statement such as Assumptions: none; allocation: no dynamic allocation; loop: eight byte checks with unwind bound 9 so the claimed proof scope is reproducible rather than implementation-inferred.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The pointer-family scope now states that every harness uses fixed eight-byte stack inputs, performs no dynamic allocation, contains no explicit proof loop, and uses no kani::assume; every initialized eight-byte input is unconstrained. #[kani::unwind(9)] bounds the modeled eight-byte scans with unwinding assertions enabled.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
48967ac to
53ae6e6
Compare
|
@codex review Please review 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. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ 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". |
3879072 to
ed4cbd6
Compare
8ed9170 to
95247f7
Compare
|
@codex review 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. |
|
Codex Review: Didn't find any major issues. You're on a roll. Reviewed commit: ℹ️ 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". |
95247f7 to
b643033
Compare
ed4cbd6 to
bdccd1c
Compare
|
@codex review Please review exact 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. |
|
Codex Review: Didn't find any major issues. What shall we delve into next? Reviewed commit: ℹ️ 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". |
b643033 to
9509491
Compare
bdccd1c to
269250c
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ 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". |
9509491 to
98be607
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ 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". |
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Gzi6kdmiqx3hi24gccqw5f6pebmv47idc
|
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
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v52 — Compare vs v51
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gzi6kdmiqx3hi24gccqw5f6pebmv47idc && git checkout -b pr-Gzi6kdmiqx3hi24gccqw5f6pebmv47idc FETCH_HEADCheckout
git fetch origin refs/heads/Gzi6kdmiqx3hi24gccqw5f6pebmv47idc && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gzi6kdmiqx3hi24gccqw5f6pebmv47idc && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.