From e956e85e172609c42e2762d8d16416f3cfe504ed Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 25 Mar 2022 21:08:47 +0000 Subject: [PATCH 1/2] Documentation: Applications (new section) --- docs/src/SUMMARY.md | 7 +++--- docs/src/application.md | 14 +++++++++++ docs/src/kani-tutorial.md | 19 ++++----------- docs/src/tool-comparison.md | 25 ++++++++++---------- docs/src/tutorial-first-steps.md | 2 -- docs/src/tutorial-real-code.md | 40 +++++++++++--------------------- 6 files changed, 47 insertions(+), 60 deletions(-) create mode 100644 docs/src/application.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index db9de14f2fd3..7294ca8dcf27 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -12,6 +12,9 @@ - [Failures that Kani can spot](./tutorial-kinds-of-failure.md) - [Loop unwinding](./tutorial-loop-unwinding.md) - [Nondeterministic variables](./tutorial-nondeterministic-variables.md) + +- [Application](./application.md) + - [Comparison with other tools](./tool-comparison.md) - [Where to start on real code](./tutorial-real-code.md) - [Developer documentation](dev-documentation.md) @@ -23,7 +26,3 @@ - [Rust feature support](./rust-feature-support.md) - [Overrides](./overrides.md) - ---- - -[Comparison with other tools](./tool-comparison.md) diff --git a/docs/src/application.md b/docs/src/application.md new file mode 100644 index 000000000000..e41b75050549 --- /dev/null +++ b/docs/src/application.md @@ -0,0 +1,14 @@ +# Application + +You may be interested in applying Kani if you're in this situation: + +1. You're working on a moderately important project in Rust. +2. You've already invested heavily in testing to ensure correctness. +3. You want to invest further, to gain a much higher degree of assurance. + +> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking. +> These yield good results, are very cheap to apply, and are often easier to adopt and debug. +> Kani is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with. + +In this section, we explain [how Kani compares with other tools](./tool-comparison.md) +and suggest [where to start applying Kani in real code](./tutorial-real-code.md). diff --git a/docs/src/kani-tutorial.md b/docs/src/kani-tutorial.md index b078a787e40f..74ff646e2c8b 100644 --- a/docs/src/kani-tutorial.md +++ b/docs/src/kani-tutorial.md @@ -1,21 +1,10 @@ -# Kani tutorial +# Tutorial -If you're interested in applying Kani, then you're probably in this situation: - -1. You're working on a moderately important project in Rust. -2. You've already invested heavily in testing to ensure correctness, and possibly fuzzing to ensure the absence of shallow security issues. -3. You want to invest further, to gain a much higher degree of assurance. - -> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking. -> These yield good results, are very cheap to apply, and are often easier to adopt and debug. -> Refactoring work to make your code more property-testable will generally also make the code more model-checkable as well. -> Kani is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with. +> Note: This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first. This tutorial will step you through a progression from simple to moderately complex tasks with Kani. It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured. It will also teach you the basics of "debugging" proof harnesses, which mainly consists of diagnosing and resolving non-termination issues with the solver. -1. [Begin with Kani installation.](./install-guide.md) This will take through to running `kani` on your first Rust program. -2. Consider reading our [tool comparison](./tool-comparison.md) to understand what Kani is. -3. [Work through the tutorial.](./tutorial-first-steps.md) -4. Consider returning to the [tool comparison](./tool-comparison.md) after trying the tutorial to see if any of the abstract ideas have become more concrete. +You may also want to read the [Application](./application.md) section to better +understand what Kani is and how it can be applied on real code. diff --git a/docs/src/tool-comparison.md b/docs/src/tool-comparison.md index a113af06714c..d11e50c9968c 100644 --- a/docs/src/tool-comparison.md +++ b/docs/src/tool-comparison.md @@ -1,29 +1,30 @@ # Comparison with other tools **Fuzzing** (for example, with [`cargo-fuzz`](https://github.com/rust-fuzz/cargo-fuzz)) is a unguided approach to random testing. -A fuzzer generally provides an input of random bytes, and then examines fairly generic properties ("doesn't crash or commit undefined behavior") about the behavior of the resulting program. +A fuzzer generally provides an input of random bytes, and then examines fairly generic properties (such as "doesn't crash" or "commit undefined behavior") about the resulting program. + Fuzzers generally get their power through a kind of evolutionary algorithm that rewards new mutant inputs that "discover" new branches of the program under test. -Fuzzers are excellent for testing security boundaries, precisely because they make no validity assumptions (hence "unguided") when generating the input. +Fuzzers are excellent for testing security boundaries, precisely because they make no validity assumptions (hence, they are "unguided") when generating the input. + +**Property testing** (for example, with [Proptest](https://github.com/AltSysrq/proptest)) is a guided approach to random testing. +"Guided" in the sense that the test generally provides a strategy for generating random values that constrains their range. +The purpose of this strategy is to either focus on interesting values, or avoid failing assertions that only hold for a constrained set of inputs. +Tests in this style do actually state properties: *For all inputs (of some constrained kind), this condition should hold*. -**Property testing** (for example, with [`proptest`](https://github.com/AltSysrq/proptest)) is a guided approach to random testing. -"Guided" in the sense that the test generally provides a strategy (for generating random values) that constrains their range. -The purpose of this is to either focus on interesting values, or because the assertions in the test will only hold for a constrained set of inputs. -This generator is sampled several times, and the test's assertions are checked for each sample. -Tests in this style do actually state properties: "forall inputs (of some constrained kind), this condition should hold." -Property testing is often quite effective, but the engine can't fully prove the property, it can only sample randomly a few of those values to test (though property testing libraries frequently give interesting "edge cases" higher probability, making them more effective at bug-finding). +Property testing is often quite effective, but the engine can't fully prove the property: It can only sample randomly a few of those values to test (though property testing libraries frequently give interesting "edge cases" a higher probability, making them more effective at bug-finding). -**Model checking** is similar to these techniques in how you use them, but model checking is non-random and exhaustive (though often only up to some bound on input or problem size). +**Model checking** is similar to these techniques in how you use them, but it is non-random and exhaustive (though often only up to some bound on input or problem size). Thus, properties checked with a model checker are effectively proofs. Instead of naively trying all possible _concrete_ inputs (which could be infeasible and blow up exponentially), model checkers like Kani will cleverly encode program traces as _symbolic_ "[SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)/[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)" problems, and hand them off to SAT/SMT solvers. -Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!) +Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model- checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!) Model checking allows you to prove non-trivial properties about programs, and check those proofs in roughly the same amount of time as a traditional test suite would take to run. -The downside is many types of properties can quickly become "too large" to practically model check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does. +The downside is many types of properties can quickly become "too large" to practically model-check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does. This process basically boils down to "debugging" the proof. ## Looking for concurrency? -Kani does not yet support verifying concurrent Rust code. +At present, Kani [does not support verifying concurrent code](./rust-feature-support.md). Two tools of immediate interest are [Loom](https://github.com/tokio-rs/loom) and [Shuttle](https://github.com/awslabs/shuttle). Loom attempts to check all possible interleavings, while Shuttle chooses interleavings randomly. The former is sound (like Kani), but the latter is more scalable to large problem spaces (like property testing). diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md index d9078697bf18..3c2625ad114f 100644 --- a/docs/src/tutorial-first-steps.md +++ b/docs/src/tutorial-first-steps.md @@ -1,7 +1,5 @@ # First steps with Kani -> This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first. - Kani is unlike the testing tools you may already be familiar with. Much of testing is concerned with thinking of new corner cases that need to be covered. With Kani, all the corner cases are covered from the start, and the new concern is narrowing down the scope to something manageable for the checker. diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md index c8f544fbfa12..6ec8816e121c 100644 --- a/docs/src/tutorial-real-code.md +++ b/docs/src/tutorial-real-code.md @@ -5,11 +5,11 @@ This section will try to help you get over that hurdle. In general, you're trying to do three things: -1. Find a place it'd be valuable to have a proof. -2. Find a place it won't be too difficult to prove something, just to start. +1. Find a place where it'd be valuable to have a proof. +2. Find a place where it won't be too difficult to prove something, just to start. 3. Figure out what a feasible longer-term goal might be. -**By far the best strategy is to follow your testing.** +**By far, the best strategy is to follow your testing.** Places where proof will be valuable are often places where you've written a lot of tests, because they're valuable there for the same reasons. Likewise, code structure changes to make functions more unit-testable will also make functions more amenable to proof. Often, by examining existing unit tests (and especially property tests), you can easily find a relatively self-contained function that's a good place to start. @@ -18,7 +18,7 @@ Often, by examining existing unit tests (and especially property tests), you can 1. Where complicated things happen with untrusted user input. These are often the critical "entry points" into the code. -These are also places where you probably want to try fuzz testing. +These are also places where you probably want to try other techniques (e.g., fuzz testing). 2. Where `unsafe` is used extensively. These are often places where you'll already have concentrated a lot of tests. @@ -36,7 +36,7 @@ Dependencies can sometimes blow up the tractability of proofs. This can usually be handled, but requires a lot more investment to make it happen, and so isn't a good place to start. 2. Don't forget to consider starting with your dependencies. -Sometimes the best place to start won't be your code, but in code you depend on. +Sometimes the best place to start won't be your code, but the code you depend on. If it's used by more projects that just yours, it will be valuable to more people, too! 3. Find well-tested code. @@ -47,14 +47,13 @@ Here are some things to avoid, when starting out: 1. Lots of loops, or at least nested loops. As we saw in the last section, right now we often need to put upper bounds on these to make more limited claims. -2. "Inductive data structures." -These are data of unbounded size. -(For example, linked lists and trees.) -Much like needing to put bounds on loops, these can be hard to model since you needs to put bounds on their size, too. +2. Inductive data structures. +These are data structures with unbounded size (e.g., linked lists or trees.) +These can be hard to model since you need to set bounds on their size, similar to what happens with loops. -3. I/O code. -Kani doesn't model I/O, so if you're depending on behavior like reading/writing to a file, you won't be able to prove anything. -This is one obvious area where testability helps provability: often we separate I/O and "pure" computation into different functions, so we can unit test the latter. +3. Input/Output code. +Kani doesn't model I/O, so if you depend on behavior like reading/writing to a file, you won't be able to prove anything. +This is one obvious area where testability helps provability: often we separate I/O and "pure" computation into different functions, so we can unit-test the latter. 4. Deeper call graphs. Functions that call a lot of other functions can require more investment to make tractable. @@ -68,7 +67,7 @@ Rust tends to discourage this, but it still exists in some forms. A first proof will likely start in the following form: -1. Nondeterministically initialize variables that will correspond to function inputs, with as few constraints as possible +1. Nondeterministically initialize variables that will correspond to function inputs, with as few constraints as possible. 2. Call the function in question with these inputs. 3. Don't (yet) assert any post-conditions. @@ -81,18 +80,5 @@ Running Kani on this simple starting point will help figure out: (If the problem is initially intractable, try `--unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.) Once you've got something working, the next step is to prove more interesting properties than what Kani covers by default. -You accomplish this by adding new assertions. -These are not necessarily assertions just in your proof harness: consider also adding new assertions to the code being run. -These count too! +You accomplish this by adding new assertions (not just in your harness, but also to the code being run). Even if a proof harness has no post-conditions being asserted directly, the assertions encountered along the way can be meaningful proof results by themselves. - - -## Summary - -In this section: - -1. We got some advice on how to choose a higher-value starting point for a first proof. -2. We got some advice on how to choose an easier starting point for a first proof. -3. We got some advice on how to structure our first proof, at least initially. - -> TODO: This section is incomplete. We should probably add an example session of finding a proof to write for, perhaps, Firecracker. From eff1842c827fc6546191dd460fcc07188317d3b8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 4 Apr 2022 21:11:44 +0000 Subject: [PATCH 2/2] Address Jai's comments. --- docs/src/tutorial-real-code.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md index 6ec8816e121c..db8c77f1a4a1 100644 --- a/docs/src/tutorial-real-code.md +++ b/docs/src/tutorial-real-code.md @@ -36,7 +36,7 @@ Dependencies can sometimes blow up the tractability of proofs. This can usually be handled, but requires a lot more investment to make it happen, and so isn't a good place to start. 2. Don't forget to consider starting with your dependencies. -Sometimes the best place to start won't be your code, but the code you depend on. +Sometimes the best place to start won't be your code, but the code that you depend on. If it's used by more projects that just yours, it will be valuable to more people, too! 3. Find well-tested code. @@ -52,7 +52,7 @@ These are data structures with unbounded size (e.g., linked lists or trees.) These can be hard to model since you need to set bounds on their size, similar to what happens with loops. 3. Input/Output code. -Kani doesn't model I/O, so if you depend on behavior like reading/writing to a file, you won't be able to prove anything. +Kani doesn't model I/O, so if your code depends on behavior like reading/writing to a file, you won't be able to prove anything. This is one obvious area where testability helps provability: often we separate I/O and "pure" computation into different functions, so we can unit-test the latter. 4. Deeper call graphs.