From Fuzzing to Proof: Using Kani with the Bolero Property-Testing Framework
Today we’re going to talk about how you can use fuzzing and verification in a unified framework, which is enabled by the integration of the Kani Rust Verifier in Bolero. Bolero is a property-testing framework that makes it easy for users to test a piece of Rust code with multiple fuzzing engines, ...
Hasnain says:
Will definitely need to try this in the future.
“One question that might arise is: is there any point in using fuzzing alongside Kani? In other words, if we can prove a harness for all inputs with Kani, would we still want to use fuzzing? The answer is yes, because fuzzing and Kani provide complementary benefits.
Kani verifies a Rust program by symbolically analyzing its code. This allows Kani to make mathematical statements about the expected semantics of the Rust code being verified. Kani allows you to prove that, for all possible inputs, the code under verification follows its specification, assuming everything else functions correctly (e.g. the underlying hardware, the OS, etc.).
Fuzzing concretely executes the program under test. This gives you end-to-end confidence that for the set of inputs generated by the fuzzer, the code under verification follows its specification, under real-world conditions. Fuzzing and Kani fit together to give more assurance than either provides on its own.”
Posted on 2022-11-04T04:03:29+0000