Fully Automated Inductive Invariants Inference for Solidity Smart Contracts by Leo Alt
One of the hardest challenges in formal verification is handling loops in a fully automated way. A common approach is to compute inductive loop invariants, properties that formally capture the essence of the loop independent of the rest of the program. These sound loop summaries are then used to check further desired properties from a specification. In the context of Solidity smart contracts, properties over state variables can also be seen as loop invariants where one loop iteration is one transaction.
We developed a technique using systems of Horn clauses to infer state and loop inductive invariants at compile-time in a fully automated way, while proving safety properties. The algorithms are released as part of the SMTChecker module inside the Solidity compiler. Thus, the process is seamless to the developer and requires nothing more than the source code. The generated inductive invariants can be used by the compiler and other tools to check properties more easily, to confirm/correct external specifications, and to provide potentially hidden program logic insights to the developer.
The goal of the talk is to present the technicalities and use cases of our approach, and to continue discussions around formal verification and inductive invariants.
Support this Site
Article comments