WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants
Reading group: Frambot Paul presented "WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants" at 4A301 the 7/1/2022 at 10h00.
Abstract
This WIP paper describes our experience using formal verification to find bugs in smart contracts. Perhaps surprisingly, the most difficult part of the formal verification process is not the verification itself, but specification: that is, expressing the desired properties of the program. In the domain of smart contracts, we have found that the same invariants apply across many different software versions and platforms. This creates a potential network effect where the cost of formal verification drops as the repertoire of reusable invariants grows. We aim to jumpstart this process by: (i) sharing several invariants we have already identified and found to be useful and (ii) suggesting a specification framework that formalizes these invariants as parameterized Hoare triples. The second point addresses the challenge that differences arise between platforms in the exact form of the invariants. By adopting a common specification language, the community will be able to better communicate knowledge about important invariants between projects, and to collaborate in building tools that support reasoning about such invariants. Finally, we present some preliminary results from applying a tool for automatically checking invariants to some sample contracts
