RustHorn: CHC-based Verification for Rust Programs
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Matsushita, Yusuke
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
 Hello everyone, I'm Yusuke Matsushita at the University of Tokyo. Now I talk about our ETH-2020 paper, Rust-Hone CHC-based verification for Rust programs. Our work Rust-Hone presents a novel reduction from Rust programs to CHC for automated verification. We explain Rust and CHC later. Our method removes pointers by leveraging Rust's ownership guarantees. It turns a point of PA into the pair of its current and final target values, a A-circle, using the technique of prophecy. It supports various features, including recursive data types and reborrowing. We proved soundness and completeness of our reduction and evaluated our method using benchmarks. So I talk a bit about the background. CHC stands for Constraint Home Clothes, and CHC is commonly used for automated verification. Suppose you have a function mc91, and you want to verify its functional correctness in terms of this test. Then you turn this program into these logic formulas called phfeef. Here mc91 is a predicate variable that represents the input-output relation of the original function. The functional correctness of the original program is equivalent to the satisfiability of these phfeefs, and indeed they have a solution like this. There are a number of automated phfeefs always, such as spacer and hoist. They can automatically find solutions like this. So by reducing a program into phfeefs like this, we can perform automated program verification. However, when the program has pointers, verification is often hard. A naive approach is to model the memory as our array h. It's simple, but it easily fails in the presence of dynamic memory allocation. For example, consider this recursive function jreq. If we apply the naive approach to this program, we get these phfeefs. They are satisfiable, but the solution requires universal quantification. In particular, we need a quantified invariant that states that some memory region is unchanged. And automatically finding this kind of solution is very hard. So our Rust home removes pointers from programs to perform verification smoothly. Now I explain Rust in a nutshell. Rust is a systems programming language that allows low-level efficient memory operations and also provides safety guarantees by its unique type system. A keyword is ownership. In Rust, when you want to update an object, you need ownership on that object. And the ownership cannot be shared. In order to handle ownership flexibly, Rust has an operation called borough. It is temporary transfer of ownership to a newly created reference. Here's an example of borrowing. First, we create an integer object and name it A. And by borrowing from A, we create a new pointer or reference Pa that points at the integer object. And at this point, we determine the deadline of the borough. Until the deadline, Pa has the ownership on the integer object. Here, it increases the integer by 10. And after the deadline, Pa loses the ownership and A retrieves the ownership. So A can read the integer object and then know that it has been updated to 11. So this is basics of borrowing. Here's an interesting but basic example of borrowing, which is important in terms of verification. The function max takes two integer references Pa and PB and returns the one with a larger target integer value. The interesting point about the function max is that the return address is determined by a dynamic condition. The function test takes two integer objects, A and B, and borrows them until the same deadline. And passes the created references to the function max and take the reference PC and performs increment on the PC. And after the deadline, it checks that the values of A and B are now different. So now I describe our method. Our motivation is to remove pointers in Rust programs for smooth verification. A naive approach is to model each reference just as its target value. However, by doing so, we can't model the lender after the borough state line. For example, if we apply this naive approach to the previously discussed program, then we get THC's like this. It seems that we can represent the max function, but when we want to check the assertion here, we realize that we don't know what are the values for A and B at this point. So we cannot model this Rust program appropriately in this approach. So here's our method. The key idea is to take the final target value A circle for each borough. When we borrow A to reference PA, we prophesy the final target value A circle and model PA as A A circle, the pair of the current target value A and the final target value A circle. When we update the target of PA, we accordingly update A in the model. And when we release PA with the value A A circle, we set A circle to A at that point. Okay, so let's see an example. The Rust program with max and test is now translated into ZVTHC by our reduction. When we borrow A and B, we prophesy A circle and B circle, the value of A and B at the point here. And then we pass the references to the function max and suppose A is larger than B. Then we throw away PB here, so we constrain B circle to B here and we return PA, so r equals to A A circle. And now the returned reference is named PC. We perform increment on the PC and then we throw away it. We throw it away. So the constraint is C circle equals C plus 1. By doing so, we have the complete and sound information on the final target values A circle and B circle. So now we just need to check that A circle is not equal to B circle. And by this reduction, we have sound and complete representation of the original program, so we can successfully verify the Rust program. Let's see an advanced example with a recursive data type. The function pick takes a reference to a list PLA and returns a reference to some random element of the list. The test function inputs some list and borrows the list and calls the pick to take some reference PA and performs increment on that reference. And then checks that the sum of the list has increased by one. This Rust program turns into Zeev-CHC. And interestingly, Zeev-CHC have a very simple solution to pick. Like this. And indeed, we successfully verified this verification problem completely automatically in our experiment. We also formalized our core Rust and our reduction from Rust to CHC and then proved soundness and completeness of our reduction. The statement is that for any Rust function F that does not input references, the input output relation of F and Rust is equivalent to the least solution to F in our CHC representation. The proof goes by constructing a bifumulation between Rust and CHC resolution, modeling each prophecy a circle as a logic variable. Details are described in the paper. Now I talk about the evaluation. We implemented a prototype Rust verifier that uses our method, which is named RustHome. We did analyze Rust's mid-level intermediate representation and suppose various features of Rust. The back-end CHC solvers of RustHome are spacer and hoist. Then we evaluated RustHome in comparison with SeeHome, which is a CHC-based verifier that uses the array-based reduction that we discussed earlier. We used 58 benchmarks written both in Rust and See. 16 of them were from SeeHome's tests and 42 were made by us, featuring various use cases of borrowing. Here's an overview of experimental results. RustHome succeeded in various benchmarks. In particular, RustHome success-free verified a number of very interesting verification problems featuring borrowing and recursive data types. So now I talk about related work. There are a number of studies and CHC-based automated verification of pointer programs. SeeHome for See, C++ and JHome for Java do not use ownership unlike RustHome, but they easily raise false alarms. Rust for Java uses a fractional ownership model, which is different from Rust's ownership model. But it requires extra annotations on ownership unlike RustHome. Also, there are a number of studies and verification of Rust programs that leverage Rust's ownership guarantees. Rusty models Rust programs in a separation logic, and Electrolysis models Rust programs in a purely functional language, leveraging Rust's ownership guarantees. But they do not support some reference operations such as split-up references, unlike our Rust home. So here's a summary. Our Rust home proposed a novel approach to CHC-based automated verification of Rust programs. It leverages Rust's ownership guarantees. It turns a reference PA into the pair of its current and final target values ASL. It supports various features including recursive data types. Although we did correctness proof and experimental evaluation. Our ongoing work is to prove the correctness of our reduction in quark, supporting unsafe code extensively. It is under the project name RustHomeBuild. It unifies our Rust home and another existing study RustBuild. That's all for my talk. Thank you for listening.
 Hello everyone, I'm Yusuke Matsushita at the University of Tokyo.  Now I talk about our ETH-2020 paper, Rust-Hone CHC-based verification for Rust programs.  Our work Rust-Hone presents a novel reduction from Rust programs to CHC for automated verification.  We explain Rust and CHC later.  Our method removes pointers by leveraging Rust's ownership guarantees.  It turns a point of PA into the pair of its current and final target values, a A-circle,  using the technique of prophecy.  It supports various features, including recursive data types and reborrowing.  We proved soundness and completeness of our reduction and evaluated our method using benchmarks.  So I talk a bit about the background.  CHC stands for Constraint Home Clothes, and CHC is commonly used for automated verification.  Suppose you have a function mc91, and you want to verify its functional correctness in terms  of this test.  Then you turn this program into these logic formulas called phfeef.  Here mc91 is a predicate variable that represents the input-output relation of the original  function.  The functional correctness of the original program is equivalent to the satisfiability  of these phfeefs, and indeed they have a solution like this.  There are a number of automated phfeefs always, such as spacer and hoist.  They can automatically find solutions like this.  So by reducing a program into phfeefs like this, we can perform automated program verification.  However, when the program has pointers, verification is often hard.  A naive approach is to model the memory as our array h.  It's simple, but it easily fails in the presence of dynamic memory allocation.  For example, consider this recursive function jreq.  If we apply the naive approach to this program, we get these phfeefs.  They are satisfiable, but the solution requires universal quantification.  In particular, we need a quantified invariant that states that some memory region is unchanged.  And automatically finding this kind of solution is very hard.  So our Rust home removes pointers from programs to perform verification smoothly.  Now I explain Rust in a nutshell.  Rust is a systems programming language that allows low-level efficient memory operations  and also provides safety guarantees by its unique type system.  A keyword is ownership.  In Rust, when you want to update an object, you need ownership on that object.  And the ownership cannot be shared.  In order to handle ownership flexibly, Rust has an operation called borough.  It is temporary transfer of ownership to a newly created reference.  Here's an example of borrowing.  First, we create an integer object and name it A.  And by borrowing from A, we create a new pointer or reference Pa that points at the integer object.  And at this point, we determine the deadline of the borough.  Until the deadline, Pa has the ownership on the integer object.  Here, it increases the integer by 10.  And after the deadline, Pa loses the ownership and A retrieves the ownership.  So A can read the integer object and then know that it has been updated to 11.  So this is basics of borrowing.  Here's an interesting but basic example of borrowing, which is important in terms of verification.  The function max takes two integer references Pa and PB and returns the one with a larger  target integer value.  The interesting point about the function max is that the return address is determined by  a dynamic condition.  The function test takes two integer objects, A and B, and borrows them until the same deadline.  And passes the created references to the function max and take the reference PC and performs  increment on the PC.  And after the deadline, it checks that the values of A and B are now different.  So now I describe our method.  Our motivation is to remove pointers in Rust programs for smooth verification.  A naive approach is to model each reference just as its target value.  However, by doing so, we can't model the lender after the borough state line.  For example, if we apply this naive approach to the previously discussed program, then  we get THC's like this.  It seems that we can represent the max function, but when we want to check the assertion here,  we realize that we don't know what are the values for A and B at this point.  So we cannot model this Rust program appropriately in this approach.  So here's our method.  The key idea is to take the final target value A circle for each borough.  When we borrow A to reference PA, we prophesy the final target value A circle and model  PA as A A circle, the pair of the current target value A and the final target value  A circle.  When we update the target of PA, we accordingly update A in the model.  And when we release PA with the value A A circle, we set A circle to A at that point.  Okay, so let's see an example.  The Rust program with max and test is now translated into ZVTHC by our reduction.  When we borrow A and B, we prophesy A circle and B circle, the value of A and B at the  point here.  And then we pass the references to the function max and suppose A is larger than B. Then we  throw away PB here, so we constrain B circle to B here and we return PA, so r equals to  A A circle.  And now the returned reference is named PC.  We perform increment on the PC and then we throw away it.  We throw it away.  So the constraint is C circle equals C plus 1.  By doing so, we have the complete and sound information on the final target values A circle  and B circle.  So now we just need to check that A circle is not equal to B circle.  And by this reduction, we have sound and complete representation of the original program, so  we can successfully verify the Rust program.  Let's see an advanced example with a recursive data type.  The function pick takes a reference to a list PLA and returns a reference to some random  element of the list.  The test function inputs some list and borrows the list and calls the pick to take some reference  PA and performs increment on that reference.  And then checks that the sum of the list has increased by one.  This Rust program turns into Zeev-CHC. And interestingly, Zeev-CHC have a very simple  solution to pick.  Like this.  And indeed, we successfully verified this verification problem completely automatically  in our experiment.  We also formalized our core Rust and our reduction from Rust to CHC and then proved soundness  and completeness of our reduction.  The statement is that for any Rust function F that does not input references, the input  output relation of F and Rust is equivalent to the least solution to F in our CHC representation.  The proof goes by constructing a bifumulation between Rust and CHC resolution, modeling  each prophecy a circle as a logic variable.  Details are described in the paper.  Now I talk about the evaluation.  We implemented a prototype Rust verifier that uses our method, which is named RustHome.  We did analyze Rust's mid-level intermediate representation and suppose various features  of Rust.  The back-end CHC solvers of RustHome are spacer and hoist.  Then we evaluated RustHome in comparison with SeeHome, which is a CHC-based verifier  that uses the array-based reduction that we discussed earlier.  We used 58 benchmarks written both in Rust and See.  16 of them were from SeeHome's tests and 42 were made by us, featuring various use cases  of borrowing.  Here's an overview of experimental results.  RustHome succeeded in various benchmarks.  In particular, RustHome success-free verified a number of very interesting verification  problems featuring borrowing and recursive data types.  So now I talk about related work.  There are a number of studies and CHC-based automated verification of pointer programs.  SeeHome for See, C++ and JHome for Java do not use ownership unlike RustHome, but they  easily raise false alarms.  Rust for Java uses a fractional ownership model, which is different from Rust's ownership  model.  But it requires extra annotations on ownership unlike RustHome.  Also, there are a number of studies and verification of Rust programs that leverage Rust's ownership  guarantees.  Rusty models Rust programs in a separation logic, and Electrolysis models Rust programs  in a purely functional language, leveraging Rust's ownership guarantees.  But they do not support some reference operations such as split-up references, unlike our Rust  home.  So here's a summary.  Our Rust home proposed a novel approach to CHC-based automated verification of Rust programs.  It leverages Rust's ownership guarantees.  It turns a reference PA into the pair of its current and final target values ASL.  It supports various features including recursive data types.  Although we did correctness proof and experimental evaluation.  Our ongoing work is to prove the correctness of our reduction in quark, supporting unsafe  code extensively.  It is under the project name RustHomeBuild.  It unifies our Rust home and another existing study RustBuild.  That's all for my talk.  Thank you for listening.
604907f41a80aac83ca25d55_0_47.png 604907f41a80aac83ca25d55_48_131.png 604907f41a80aac83ca25d55_132_287.png 604907f41a80aac83ca25d55_288_419.png 604907f41a80aac83ca25d55_420_1355.png 604907f41a80aac83ca25d55_1356_1523.png 604907f41a80aac83ca25d55_1524_3431.png 604907f41a80aac83ca25d55_3432_5291.png 604907f41a80aac83ca25d55_5292_5447.png 604907f41a80aac83ca25d55_5448_8255.png 604907f41a80aac83ca25d55_8256_9971.png 604907f41a80aac83ca25d55_9972_10115.png 604907f41a80aac83ca25d55_10116_11807.png 604907f41a80aac83ca25d55_11808_12263.png 604907f41a80aac83ca25d55_12264_14459.png 604907f41a80aac83ca25d55_14460_15011.png 604907f41a80aac83ca25d55_15012_16019.png 604907f41a80aac83ca25d55_16020_17807.png 604907f41a80aac83ca25d55_17808_18959.png 604907f41a80aac83ca25d55_18960_19079.png 604907f41a80aac83ca25d55_19080_20567.png 604907f41a80aac83ca25d55_20568_21227.png 604907f41a80aac83ca25d55_21228_21335.png 604907f41a80aac83ca25d55_21336_21479.png 604907f41a80aac83ca25d55_21480_23243.png 604907f41a80aac83ca25d55_23244_24946.png