@@ -143,45 +143,40 @@ Verification Time: 0.19135727s
143
143
## FAQ
144
144
145
145
** Q:** What is the Kani verifier?\
146
- ** A:** The
147
- [ Kani Rust Verifier] ( https://github.com/model-checking/kani ) is a bit-precise
148
- model checker for Rust. Kani is particularly useful for verifying unsafe code
149
- blocks in Rust, where the
146
+ ** A:** The [ Kani Rust Verifier] ( https://github.com/model-checking/kani ) is a
147
+ bit-precise model checker for Rust. Kani is particularly useful for verifying
148
+ unsafe code blocks in Rust, where the
150
149
“[ unsafe superpowers] ( https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers ) "
151
150
are unchecked by the compiler.
152
151
153
152
** Q:** What safety properties does Kani verify?\
154
- ** A:** Kani verifies memory
155
- safety properties (e.g., invalid-pointer dereferences, out-of-bounds array
156
- access), user-specified assertions (i.e., ` assert!(...) ` ), the absence of
157
- ` panic!() ` s (e.g., ` unwrap() ` on ` None ` values), and the absence of some types
158
- of unexpected behavior (e.g., arithmetic overflows). For a full overview, see
159
- the
153
+ ** A:** Kani verifies memory safety properties (e.g., invalid-pointer
154
+ dereferences, out-of-bounds array access), user-specified assertions (i.e.,
155
+ ` assert!(...) ` ), the absence of ` panic!() ` s (e.g., ` unwrap() ` on ` None ` values),
156
+ and the absence of some types of unexpected behavior (e.g., arithmetic
157
+ overflows). For a full overview, see the
160
158
[ Kani documentation] ( https://model-checking.github.io/kani/tutorial-kinds-of-failure.html ) .
161
159
162
160
** Q:** Do we expect all contributors to write harnesses for newly introduced
163
161
code?\
164
- ** A:** No. Kani is complementary to unit testing, and we do not have
165
- target for “proof coverage”. We employ formal verification in especially
166
- critical code areas. Generally we do not expect someone who might not be
167
- familiar with formal tools to contribute harnesses. We do expect all contributed
168
- code to pass verification though, just like we expect it to pass unit test!
162
+ ** A:** No. Kani is complementary to unit testing, and we do not have target for
163
+ “proof coverage”. We employ formal verification in especially critical code
164
+ areas. Generally we do not expect someone who might not be familiar with formal
165
+ tools to contribute harnesses. We do expect all contributed code to pass
166
+ verification though, just like we expect it to pass unit test!
169
167
170
168
** Q:** How should I report issues related to any Firecracker harnesses?\
171
- ** A:**
172
- Our Kani harnesses verify safety critical invariants. If you discover a flaw in
173
- a harness, please report it using the
169
+ ** A:** Our Kani harnesses verify safety critical invariants. If you discover a
170
+ flaw in a harness, please report it using the
174
171
[ security issue disclosure process] ( https://github.com/firecracker-microvm/firecracker/blob/main/SECURITY.md ) .
175
172
176
- ** Q:** How do I know which properties I should prove in the Kani
177
- harness?\
178
- ** A:** Generally, these are given by some sort of specification. This
179
- can either be the function contract described in its document (e.g. what
180
- relation between input and output do callers expect?), or even something formal
181
- such as the TCP/IP standard. Don't forget to mention the specification in your
182
- proof harness!
173
+ ** Q:** How do I know which properties I should prove in the Kani harness?\
174
+ ** A:** Generally, these are given by some sort of specification. This can either
175
+ be the function contract described in its document (e.g. what relation between
176
+ input and output do callers expect?), or even something formal such as the
177
+ TCP/IP standard. Don't forget to mention the specification in your proof
178
+ harness!
183
179
184
180
** Q:** Where do I debug a broken proof?\
185
- ** A:** Check out the Kani book section
186
- on
181
+ ** A:** Check out the Kani book section on
187
182
[ debugging verification failures] ( https://model-checking.github.io/kani/debugging-verification-failures.html ) .
0 commit comments