# Team Team Name: Soundproof Team members: Aurel Bílý, Felix Wolf Students/non students: PhD students Affiliation(s): ETH Zurich Tools used: Viper Are the team members developers of the used tools? yes # Tool Which tool(s) have you used? > Viper How did you choose the tool to use? Was the choice related to the specific challenge? > both team member know the tool Which tool feature did you find most helpful to solve the challenge? > separation logic Which tool limitation was the most significant obstacle to solve the challenge? > termination of the tool Is there any improvement to the tool that you would suggest based on your experience using it in the challenge? > not at the top of my head If you would be doing the same challenge again, would you pick another tool to solve it? Why or why not? > I would use Gobra for the second task # Challenge 1 Which verification tasks were specified? > (1), (2), (3) Which verification tasks were verified? > partially (1), (2), (3). The tool did not terminate. ## Implementation Does the implementation include all expected functionality? (If not, what’s missing) > we rewrote it to Viper, i.e. min, max comprehensions are more complicated. Are there any simplifications in the implementation? What were they, and why did you include them? > we rewrote min and max, since Viper does not support set comprehensions Does the implementation follow exactly the algorithm and data structure given in pseudo-code? If it deviates from it, how and why does it deviate? > to our knowledge, it is the same algorithm and data structure Is your implementation executable? If not, how much effort is it to make it executable? > it is not executable, hard to judge ## Specification Does the specification include basic correctness requirements (memory safety, termination, ...)? Which of such requirements are guaranteed by the implementation language (for example by its type system)? > none of the basic correctness requirements are guaranteed by Viper (without verifying them) ## Verification Does the verification guarantee correctness for all valid inputs? > yes Does the verification make any simplifying assumptions (such as: integers are unbounded, execution is sequential/single-threaded, etc.)? Is the verification of any properties partial or depending on restricting assumptions? > it is partial correctness (if termination is not shown) Does the verification depend on any (yet) unproved auxiliary statements (axioms, ‘sorry’s, admitted, etc)? > Viper offers assume statements. We have used assumptions to solve tasks partially. For each property that is not verified or not verified completely: Could it be proved given more proof guidance (such as more complex invariants), or does it reflect an intrinsic limitation of the tool/method that was used? > Viper is limited by Z3, so non-linear arithmetic can be a limit. However, we could add axioms and invoke them manually, making verification possible with more proof guidance. ## Process How much human effort was involved in verification? > We have to specify pre- and postconditions and invariants. Additionally, we have to add proof annotations in the form of unfold, fold statements, assertions, and the common proof techniques (case distinction, induction, etc). Examples of aspects that are relevant: modelling aspects of the specification, defining lemmas, proving them, adding intermediate assertions, optimizing the running time of the verifier, interacting with the prover, dealing with theories (such as properties of arithmetic), and so on. How much time is needed to run the proofs? On what hardware? > did not terminate. Before it stopped terminating, it took one minute. Are the proofs fully automatic? > yes If they are interactive: How much user effort was involved? How complex are the proof scripts? > not interactive How much additional time do you think would it take you to complete all verification tasks (including removing any restricting assumptions you may have used)? > hard to estimate. We expect a lot of time would be required. # Challenge 2 Which verification tasks were specified? > (1), (2), (3) permutation only, (5) permutation only Which verification tasks were verified? > (1), partially (2), (5) partially - not the base cases and permutation only ## Implementation Does the implementation include all expected functionality? (If not, what’s missing) > yes (for what we verified) Are there any simplifications in the implementation? What were they, and why did you include them? > no (except explicit assume statements) Does the implementation follow exactly the algorithm and data structure given in pseudo-code? If it deviates from it, how and why does it deviate? > yes Is your implementation executable? If not, how much effort is it to make it executable? > no, a lot of work ## Specification Does the specification include basic correctness requirements (memory safety, termination, ...)? Which of such requirements are guaranteed by the implementation language (for example by its type system)? > Viper's typesystem does not provide anything ## Verification Does the verification guarantee correctness for all valid inputs? > yes Does the verification make any simplifying assumptions (such as: integers are unbounded, execution is sequential/single-threaded, etc.)? Is the verification of any properties partial or depending on restricting assumptions? > it is partial correctness (if termination is not shown) Does the verification depend on any (yet) unproved auxiliary statements (axioms, ‘sorry’s, admitted, etc)? > Viper offers assume statements. We have used assumptions to solve tasks partially. For each property that is not verified or not verified completely: Could it be proved given more proof guidance (such as more complex invariants), or does it reflect an intrinsic limitation of the tool/method that was used? > Viper is limited by Z3, so non-linear arithmetic can be a limit. However, we could add axioms and invoke them manually, making verification possible with more proof guidance. ## Process How much human effort was involved in verification? > We have to specify pre- and postconditions and invariants. Additionally, we have to add proof annotations in the form of unfold, fold statements, assertions, and the common proof techniques (case distinction, induction, etc). Examples of aspects that are relevant: modelling aspects of the specification, defining lemmas, proving them, adding intermediate assertions, optimizing the running time of the verifier, interacting with the prover, dealing with theories (such as properties of arithmetic), and so on. How much time is needed to run the proofs? On what hardware? > 5s, modern (2021) laptop with i9 CPU Are the proofs fully automatic? > yes If they are interactive: How much user effort was involved? How complex are the proof scripts? > not interactive How much additional time do you think would it take you to complete all verification tasks (including removing any restricting assumptions you may have used)? > hard to estimate # Challenge 3 Which verification tasks were specified? > (1), (2) Which verification tasks were verified? > (1), most of (2) ## Implementation Does the implementation include all expected functionality? (If not, what’s missing) > Yes Are there any simplifications in the implementation? What were they, and why did you include them? > No simplifications Does the implementation follow exactly the algorithm and data structure given in pseudo-code? If it deviates from it, how and why does it deviate? > It follows it reasonably faithfully. "do while" loops were changed to equivalent loops with > loop counters for (unfinished) termination checking. Is your implementation executable? If not, how much effort is it to make it executable? > No ## Specification Does the specification include basic correctness requirements (memory safety, termination, ...)? Which of such requirements are guaranteed by the implementation language (for example by its type system)? > Yes. None are automatically proved by Viper, but both memory safety and termination are > features of the specification language. ## Verification Does the verification guarantee correctness for all valid inputs? > Does the verification make any simplifying assumptions (such as: integers are unbounded, execution is sequential/single-threaded, etc.)? > Minor simplification: the first "return false" in "member" relies on an assumption. > When choosing our model of witnesses for known-inserted members, we have not considered the > way an index can be chosed above the original hash one. As a result, even if a client holds > the witness for an inserted index, this inserted index might be higher than the original > hash and the verifier does not know that this implies that no invalid keys should be found > in the intermediate indices. Is the verification of any properties partial or depending on restricting assumptions? > partial correctness (termination not checked) Does the verification depend on any (yet) unproved auxiliary statements (axioms, ‘sorry’s, admitted, etc)? > Only the assumption detailed above. For each property that is not verified or not verified completely: Could it be proved given more proof guidance (such as more complex invariants), or does it reflect an intrinsic limitation of the tool/method that was used? > Yes, this property could have been proven if we extended our model of witnesses. ## Process How much human effort was involved in verification? > We have to specify pre- and postconditions and invariants. Additionally, we have to add proof annotations in the form of unfold, fold statements, assertions, and the common proof techniques (case distinction, induction, etc). Examples of aspects that are relevant: modelling aspects of the specification, defining lemmas, proving them, adding intermediate assertions, optimizing the running time of the verifier, interacting with the prover, dealing with theories (such as properties of arithmetic), and so on. How much time is needed to run the proofs? On what hardware? > 1.8 seconds, modern (2021) laptop with i9 CPU Are the proofs fully automatic? > yes If they are interactive: How much user effort was involved? How complex are the proof scripts? > not interactive How much additional time do you think would it take you to complete all verification tasks (including removing any restricting assumptions you may have used)? > hard to estimate. We expect a lot of time would be required.