Stream: wg-formal-methods

Topic: Verification case studies


Denis Merigoux (Apr 16 2019 at 09:30, on Zulip):

Hi all ! I wanted to share with you what I've been doing for a couple of months from November to January : https://blog.merigoux.fr/en/2019/04/16/verifying-rust.html. This blog post is intended for people who don't really know what verification is, so you can jump directly into the two case studies : https://blog.merigoux.fr/en/2019/04/16/textinput.html and https://blog.merigoux.fr/en/2019/04/16/bloom-filter.html. Basically I've translated manually bits of Rust code into F* and proven properties about them; you can see the result https://github.com/denismerigoux/rox-star.

Denis Merigoux (Apr 16 2019 at 09:32, on Zulip):

The interesting thing is that I annotated in comments all the new syntax I would have needed in Rust to specify my code, for instance https://github.com/denismerigoux/rox-star/blob/master/textinput/src/lib.rs. I used type refinements but also pre and post conditions. The code does not have loops so I don't have loop invariants.

Vytautas Astrauskas (Apr 16 2019 at 16:26, on Zulip):

Hello @Denis Merigoux. Thanks for sharing, your case studies look very interesting! I just wanted to clarify what seems to be a misconception about Viper: Viper is an infrastructure for deductive verification of concurrent programs. As such it can be used to prove full functional correctness, for example, to verify that if a binary search function returned None, then the searched element is not in the array. Viper has two back-end verifiers; one is based on symbolic execution and another is based on verification condition generation. If you have any questions, I would be happy to answer them.

Bobby Powers (Apr 17 2019 at 04:11, on Zulip):

This is so, so exciting! I have a number of types of specs I would love to figure out how to write + prove about software in rust. For example, it would be amazing to prove things about flow control in a proxy (like https://github.com/envoyproxy/envoy/blob/master/source/docs/flow_control.md ), and formally show that each connection or request had a configurable but fixed amount of memory it could consume. It would be fascinating to figure out how specs for fairly low-level stuff like this combine, and how modular they can be: how much would a flow-control spec have to change when you add another spec about correctness of routing (or about how every incoming request must get a JSON response back).

Do you have strong feelings about whether you will be able to write _all_ specs in rust, or if there are things you would necessarily need to fall back to F* for? Writing specs in a functional language like F* seems totally reasonable, and if it can keep the specs themselves shorter that also seems like a win.

Vytautas Astrauskas (Apr 17 2019 at 12:32, on Zulip):

For example, it would be amazing to prove things about flow control in a proxy (like https://github.com/envoyproxy/envoy/blob/master/source/docs/flow_control.md ), and formally show that each connection or request had a configurable but fixed amount of memory it could consume.

If I understand you correctly, you would like to prove that a connection does not consume more memory than XX, right? A possible approach for verifying this would be:
1. Add an invariant that the amount of allocated memory is X\leq X.
2. Propagate up the stack the preconditions that ensure that the invariant is maintained (this would probably include making sure that watermarks are not leaked and allowing to write only if the most recently seen watermark was low).

It would be fascinating to figure out how specs for fairly low-level stuff like this combine, and how modular they can be: how much would a flow-control spec have to change when you add another spec about correctness of routing

It depends on how deeply related are the concepts you specify. For example, does the routing depend on the state of watermarks? If not, then specifications could be completely independent.

Do you have strong feelings about whether you will be able to write _all_ specs in rust, or if there are things you would necessarily need to fall back to F* for?

For expressing properties such as sortidness of an array, it is necessary to have support for quantifiers, which are not part of Rust. However, since one can use a custom parser for Rust annotations, it is possible to write specifications in “extended Rust”. For example, a sortidness could be written as follows (edited):

#[requires="forall |i: usize, j: usize| {i <= j ==> arr[i] <= arr[j]}"]
fn binary_search(arr: Vec<i32>) -> ...
RalfJ (Apr 17 2019 at 12:34, on Zulip):

(i <= j) => arr[i] <= arr[j], I assume?

Vytautas Astrauskas (Apr 17 2019 at 12:37, on Zulip):

(i <= j) => arr[i] <= arr[j], I assume?

Yes :face_palm: . Fixed. Thanks!

Denis Merigoux (Apr 23 2019 at 13:39, on Zulip):

Hi @Vytautas Astrauskas, thanks for the clarification about Viper, I updated my blog post to reflect it.

Last update: Nov 15 2019 at 10:10UTC