List view
A milestone to capture pending issues for the new coverage reports feature, discussed in https://github.com/model-checking/kani/pull/2612 and first implemented in https://github.com/model-checking/kani/pull/2609
No due date•0/7 issues closed- No due date•54/74 issues closed
- No due date•3/14 issues closed
Make Kani execution more responsive by reusing artifacts from previous execution that don't require any modification.
No due date•9/11 issues closed- Overdue by 2 year(s)•Due by July 1, 2023
Bolero is a property-testing framework that allows users to test Rust code with multiple fuzzing engines. In 2022, Kani was integrated in Bolero (https://model-checking.github.io/kani-verifier-blog/2022/10/27/using-kani-with-the-bolero-property-testing-framework.html) so users could run Kani as a verification engine in Bolero without requiring any changes in existing harnesses. One advantage of Bolero against verification tools like Kani is that is much closer to other testing tools, which makes it easier to use by developers without any background on formal methods. Therefore, Bolero is a great candidate for filling the gap that users face when they need more assurance for their code. Thanks to Kani’s integration, property-based harnesses written for Bolero can now be used as Kani harnesses, providing even more assurance. Moreover, there is a high number of projects which already depend on property-based testing tools like proptest (95 in brazil (https://code.amazon.com/search?term=f%3ACargo.toml+proptest), 708 in crates.io (https://crates.io/crates/proptest/reverse_dependencies)) or quickcheck (132 in brazil (https://code.amazon.com/search?term=f%3ACargo.toml+quickcheck), 899 in crates.io (https://crates.io/crates/quickcheck/reverse_dependencies)). But those projects aren’t maintained anymore, which is a risk for those projects. Making Bolero compatible with either proptest or quickcheck would allow those projects to easily migrate their already-existing harnesses to Bolero, which could have a great impact on user adoption. In addition, there are many opportunities for Bolero and Kani to enhance each other by improving their integration. Bolero works with concrete executions while Kani works with symbolic ones, so it’s possible to develop a wide range of concolic testing features for a variety of purposes. The following are good examples: * Kani’s traces could be used to seed a fuzzer (this could allow Bolero to find corner cases that wasn’t able to find earlier). * Bolero’s shrinking algorithms can be used to reduce counter-examples in Kani (this would help Kani users better understand the counter-examples). * Re-usability of Arbitrary trait implementations between Kani and Bolero (this would remove the need to duplicate them for each tool). This goal has two objectives:
Overdue by 2 year(s)•Due by May 1, 2023First-time users of CBMC or Kani customers reach the limits of the tool (space-out or time-out) and are discouraged from using the tool. Existing users that try to extend formal verification to larger functions, or towards more functional properties are also likely reach the limits of the tool. Providing better scalability out of the box will help widen the adoption of FV for new users (eg: AL2, firecrab, etc. ) and extend the guarantees offered to existing users (FireTV, s2n-tls, aws-c-commons, etc). Our goal is to bring algorithmic improvements to the core algorithms in use today, that translate to a significant improvement for our users, as measured by the number of new problems solved on the benchmark suite, as well as the number of benchmarks amenable to unbounded verification. CBMC currently uses a bit-precise forward symbolic execution algorithm for GOTO programs that reduces verification to SAT with a very detailed memory model. There are many complementary model checking algorithms for GOTO-like languages, which could complement the default algorithm of CBMC: backwards symbolic simulation with loop folding, predicate abstraction, CEGAR algorithms, PRD algorithms, etc. to name a few. Our goal is to bring at least one of these alternative techniques to GOTOz programs, in order to be able to solve at least 50% of customer benchmarks that are identified as unsolvable today in our performance regression suite. In addition, the ability to perform unbounded verification is currently very limited (in the case of CBMC) or non-existent (in the case of Kani). We would like to add support for unbounded verification of array-manipulating programs in both CBMC and Kani through enabling an unbounded verification engine through one of the following means: 1. Integrating a Constrained Horn Clauses (CHC) engine in CBMC 2. Integrating an existing tool that supports unbounded verification (e.g. Creusot (https://github.com/xldenis/creusot) or Gillian (https://github.com/GillianPlatform/Gillian)) 3. Completing the support for function/loop contracts and hooking up this support in Kani
Overdue by 1 year(s)•Due by December 24, 2023•1/1 issues closedKani sometimes requires a user-specified bound to determine how many times it needs to iterate over loops in the target program. Without a bound, Kani may continue iterating over loops (unwinding) forever, failing to terminate. This confuses users and increases the time needed to write a working proof. Users can specify a maximum bound on how many times all loops can iterate, but it is not obvious what this unwinding value should be without resorting to trial-and-error. This is exacerbated by some of the ‘loops’ arising from the translation to the intermediate language (and not corresponding to loops in the original program), making it more difficult to intuit how many times they should be unwound. We aim to improve the poor user experience arising from Kani’s non-termination and the need to specify an unwinding bound in this case. Kani must either infer a loop unwind limit automatically, or time out while trying. We will measure this by running Kani on a large corpus of unit tests and seeing how often it is able to infer loop unwinding bounds.
Overdue by 1 year(s)•Due by December 1, 2023We will add support to model checking engeines portfolio for Kani by adding one new model checking engine, which will allow users to verify code that CBMC currently fails to verify in a reasonable time. Users will be able to choose a specific engine to run on each harness or to just run all engines in parallel until one finishes. This will enable users to use Kani to verify more complex harnesses and code that they couldn’t verify otherwise.
Overdue by 1 year(s)•Due by December 24, 2023•0/1 issues closedToday CBMC and Kani do not have a performance-oriented regression testing suite. As a consequence, it is impossible to consistently and reproducibly determine if a performance fix on a problem has the expected effects and does not cause unexpected regressions on some other problems. Such performance regressions have happened in the past and have been detected after releases, resulting in reduced user experience quality. We will collect benchmarks from the different sources, assess their initial hardness and categorize them (BMC, involves loops, involves function pointers, large call graph, etc.). We will collect from the following customer projects: * C language: AL2 linux, s2n-tls, FreeRTOS, coreHTTP, coreJSON, aws-c-commons; * Rust langage: firecracker, s2n-quic, firecrab. We will deliver a way for users to submit models as candidates for the performance benchmark suite and to update the benchmarks in response to upstream changes. We will deliver a way to run a given version of a GOTO solver tool on the benchmarks and collect performance metrics, and produce a performance dashboard. We will deliver a way to diff the performance of two versions of a GOTO solver tool. The benefits are the following: allow to avoid undetected performance regressions for our Kani and CBMC customers; allow us to identify hard problems that require better proof performance and monitor our progress on them; allow us to innovate faster by automating a lot of work done manually today.
Overdue by 2 year(s)•Due by June 7, 2023•2/2 issues closedThe GOTO intermediate verification language used inside CBMC has no standalone syntax and semantics specification. This resulted in a lot of time spent reverse engineering CBMC and backtracking on design choices made when implementing new features, or in new features behaving in hard to predict and possibly unsound ways. In order to let us innovate faster with better soundness guarantees for our users, we will: * define a reference syntax and semantics specification for the GOTO language * create an concrete evaluator for that reference semantics that can validate a trace against a model * create back-to-back testing tool that checks that a verification engine’s interpretation of a GOTO program complies with the reference semantics, by checking the compliance of a set of structure-covering traces produced by the verification tool. Making GOTO a standalone language and providing independent means for checking trace validity removes the exclusive dependency on CBMC, and will let us innovate faster with better soundness guarantees for our users. The reference evaluator can (will) later be used as an abstraction refinement oracle in a CEGAR loop for GOTO programs, as a starting point for a new fuzzing engine for GOTO programs, as starting point for a concolic or a symbolic execution engine for GOTO, etc.
Overdue by 2 year(s)•Due by June 7, 2023•4/14 issues closedCustomer proofs rely on the kani::any() operator. Currently, this operator is only supported out of the box for primitive types; customers must manually implement if for more compound types, which is not possible for types defined in a external crate due to Rust’s orphan rule (https://rust-lang.github.io/rfcs/0048-traits.html?highlight=orphan#coherence). This is a pain point for Kani adoption. We will deliver an automated mechanism to generate kani::any() for compound types.
Overdue by 2 year(s)•Due by June 15, 2023•1/1 issues closedAllow users to specify that a function/method definition should be swapped out for another one during verification.
No due date•26/36 issues closed- Overdue by 1 year(s)•Due by December 31, 2023•35/37 issues closed
- No due date•28/28 issues closed
Allow Kani to run on Bolero or Proptest harnesses where symbolic values are used in place of randomly-generated values.
Overdue by 2 year(s)•Due by December 5, 2022•3/4 issues closedThis milestone tracks the remaining tasks to stabilize the concrete playback feature.
No due date•18/21 issues closedTracking soundness issues for Kani.
Overdue by 1 year(s)•Due by December 31, 2023•10/19 issues closedThe RMC regression contains a set of unsupported tests currently labelled with "*fixme*" in their name. This milestone will be completed when we have no such tests.
No due date•11/13 issues closedPrototype implementation for source-based coverage report generation
No due date•5/8 issues closed