Add post: adversarial decodes broke a proven merge law - #59
Add post: adversarial decodes broke a proven merge law#59KyleClouthier wants to merge 3 commits into
Conversation
A Kani success story from bitrep, an order-invariant bit-identical float reduction crate. Covers the bug (two empty accumulator states differing only in fields the merge never reads, which serialise differently), why the Lean model-level proof could not have caught it, the measured cost split between harnesses CI runs and those gated behind cfg(kani_slow), and checking that passing harnesses are load-bearing.
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
Thank you so much for this contribution! It is a quite enjoyable reading specially for me seeing other folks using Kani and driving value from it in the wild. I made a few suggestion to improve the text but you can take any of them as you wish, it's approved on my side.
PS. I'd change the title to be a bit more catchy to a wider audience... only an intuition not a useful suggestion at this point but worth to make you reflect on it before we merge it.
Once again, thank you!! 🥳
| codec has to round-trip, and the state has to be independent of insertion order. Those laws are | ||
| proved at the model level in Lean 4. | ||
|
|
||
| The Lean proof was correct. The Rust still had a bug, and the bug was only reachable through byte |
There was a problem hiding this comment.
I felt it missed in the end of this intro the punch line that Kani was able to caught that bug. I'd also state upfront in very simple terms that this story highlights how important it's to have a model-level proof connected to the implementation, because if you don't even tho the model is proved correct, the implementation might be buggy and this story is walking on the right direction.
Of course you can make that point in a lever way while still engaging the reader as you do in this intro quite well.
| No accumulator built by adding numbers can be in that state, because `add` always writes canonical | ||
| zeros there. The only way to construct it is to decode it from bytes. So a test suite that builds | ||
| accumulators honestly, merges them in both orders, and compares, will never find this. Not because | ||
| the suite is weak, but because the state it needs is unreachable through the API it uses. |
There was a problem hiding this comment.
an image representing this here would be so great. something like what we have in this post: https://model-checking.github.io/kani-verifier-blog/2023/08/31/using-kani-to-validate-security-boundaries-in-aws-firecracker.html
of course not a blocker, it'd just be nice
| This is the part I found most instructive, and it is why the crate carries proofs at three levels | ||
| with explicitly different jobs. |
There was a problem hiding this comment.
THIS IS GOLD! This is what makes this worth publishing.
| **A differential fuzzer owns the numerical semantics.** `value()` performs f64 arithmetic that Kani | ||
| models slowly, so its correct rounding is checked against a BigInt oracle, NIST StRD datasets, and | ||
| golden cross-architecture vectors instead. The fuzzer has found real bugs of its own, including two | ||
| decoder defects in the crate's quantile sketch, and the changelog records which tool found which. |
There was a problem hiding this comment.
in which state of the development did you apply the fuzzer? do you use it in CI? I usually argue that we can use fuzzing in the beginning of the development when we start writing unit tests and regression tests... do you agree? was your experience different?
| and shift it across all 34 limbs. On CI runners **they did not close in roughly three hours.** They | ||
| are gated behind `cfg(kani_slow)` for local runs, with the reason recorded in the source. |
There was a problem hiding this comment.
Could you perhaps open a github issue on Kani pointing to one of these harnesses so we can see if there is anything that could be done to improve performance on these cases?
| None of this is a new observation. Vacuity detection goes back to Beer, Ben-David, Eisner and Rodeh | ||
| in 1997, and the Kani team shipped `kani::cover` and | ||
| [wrote about it](https://model-checking.github.io/kani-verifier-blog/2023/01/30/reachability-and-sanity-checking-with-kani-cover.html) | ||
| precisely because they know. The habit I would add is small: pair a `cover` with every `assume` and | ||
| treat an UNREACHABLE cover in CI as a failure, because otherwise the two outcomes are | ||
| indistinguishable where anybody actually looks. |
There was a problem hiding this comment.
We should be able to do that automatically somehow and your insight on how to handle vacuity here is truly on point...
|
@tautschnig @rahulku @adpaco @remi-delmas-3000 @celinval check this out 😉 |
- Retitle to 'The Lean proof was correct. The Rust still had a bug.' - State the model-vs-implementation point plainly in the intro, and say outright that Kani connected them and Kani caught it - Add fuzzing cadence (Kani per push, fuzz nightly and bounded) and note that two of five fuzz targets are not in the nightly matrix
|
Thank you, this is a genuinely useful review and I've taken most of it. Pushed the changes. Title. Changed to "The Lean proof was correct. The Rust still had a bug." Your instinct was right: the old title told Kani users what the post was about and told nobody else anything. This one states the thesis, and it should land with people who have never run a model checker. Happy to change it again if it reads as too blunt. The intro punch line. Agreed, and this was the best note in the review. I've made the point explicit up front: a proof about a model says nothing about the code underneath unless something connects the two, the model can be flawless while the implementation meant to realise it is wrong, and re-checking the model will never tell you because the model is not where the mistake is. Then plainly: Kani is what connected them, and Kani is what caught it, with a counterexample in seconds. On the fuzzer, and when it applies. Good question, and my experience differs a little from the pattern you describe. All three layers, Lean, Kani and the fuzzer, landed in the same commit here. The boundaries were drawn before any of them were written, which is what made it obvious which tool owed which property. So it wasn't fuzz-first with proofs bolted on afterwards. Where I do agree with you: the cadence has to match the cost. The six fast Kani harnesses run on every push because they close in seconds to minutes. The fuzz targets run nightly on a schedule, bounded, because a useful fuzz run is measured in hours. I've added that to the post. And one thing I noticed while answering you, which is now in the post too: five fuzz targets exist and the nightly matrix runs three. The two that are not scheduled are the two that historically found bugs. That is exactly the gap between what exists and what runs that the rest of the post is about, one layer down, in my own repo. I would not have spotted it if you hadn't asked. The performance issue on the slow harnesses. Yes, gladly, and thank you for offering. I'll open one against Kani pointing at Automating the cover-with-every-assume check. I'd be very interested in that. The shape that seems tractable: treat an The diagram. Agreed it would help, and the two-empty-states case is the right thing to draw. I'd like to add one before merge if that's alright; if it holds things up, I'm happy for the post to go without it and to follow up separately. Thanks again for the review, and for the tool. |
SVG so it stays crisp and is reviewable in the diff. Shows the two empty states differing only in min_bits, both merge orders short-circuiting on the empty check, and the two byte strings that result.
|
Both follow-ups are done. Diagram is in, showing the two empty states, both merge orders hitting Performance issue: model-checking/kani#4720. I dug into why The contrast that made it click: the merge and codec harnesses over the same 34-limb type close in seconds, and the only structural difference is that they start from I was explicit there that I gated these rather than tuning them exhaustively, since the properties are covered by Lean and by the fast harnesses, so nothing is blocked. I would just rather understand the wall than route around it. |
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
blocking so I can give a final read
|
Sounds great Felipe. I can only imagine how much you have on your plate. Kindly let me know you thoughts or if any further changes are needed for this. Regards, Kyle |
|
@KyleClouthier is there an email address I can contact you? |
|
Of course it is kyle@simgen.dev.
|
2 participants
Submitting this at @feliperodri's invitation in model-checking/kani#4635.
The post is a Kani story from bitrep, a crate for order-invariant, bit-identical float reductions. It covers four things:
The bug.
ExtremaF64::mergeshort-circuits on empty states. Two accumulators that are both empty, and that differ only in the min/max fields the merge never reads, keep whichever garbage the receiver held and therefore serialise to different bytes. Merge commutativity, stated over the encoded state, is false. No accumulator built by callingaddcan reach that state, so testing with honestly-built accumulators cannot find it.Reproducing it. The harness ranges over symbolic bytes rather than symbolic numbers, which is what makes adversarial decodes reachable. Comment out the three-line canonical check in
src/lattice.rsandextrema_merge_commutesfails;--concrete-playback=printhands back the two 25-byte states. Both are in the post, and I re-ran everything while writing it so the output quoted is real.Why the Lean proof could not have caught it. The merge algebra is proved at the model level and those proofs were correct throughout. An abstract lattice has no encoding, so it has no notion of two byte strings denoting one element. The bug is invisible at that level, not missed.
Where Kani stopped, measured. There are 11 harnesses and CI runs 6. Three add-path harnesses decompose a symbolic
f64across 34 limbs and did not close in ~3 hours on CI runners, so they are gated behindcfg(kani_slow). The post says plainly that a green badge on that repo warrants six properties and not eleven.The last section is about whether passing harnesses are load-bearing, using a small demo repo where four of five harness styles report SUCCESSFUL against a knowingly broken function. It credits Beer, Ben-David, Eisner and Rodeh (1997) and the team's own
kani::coverpost, and states outright that nothing in it is a new technique.Around 1,900 words. Happy to cut the adequacy section if you would prefer the post stay on the bitrep story, to change the title, or to restructure however suits the blog. Please tell me what to fix.