Smart contracts are programs stored on a blockchain that can be used to automate agreements and transactions. Their immutable nature carries the risk of financial losses due to vulnerabilities and bugs. Consequently, verification processes, often supported by formal methods, are indispensable in mitigating these risks. Constrained Horn Clauses (CHCs) are commonly used for representing verification conditions (VCs) in smart contract analysis and verification, and several tools have been developed based on CHCs. Despite their utility in formal verification, CHCs pose a challenge in terms of human readability. In this paper we present preliminary work in the development of a tool aimed at visualizing CHCs, helping experts inspect VCs and their correspondence with smart contract code during the auditing process. The tool combines different translations in order to generate Predicate Dependency Graphs (PDGs), depicting the relationships among CHC predicates that have been derived from smart contract functions and the properties under verification. While the current representation of PDGs is static, future developments aim to render it dynamic and user-friendly. This enhancement would enable auditors to selectively display sections of the PDGs, interact with nodes and the associated clauses and code, apply CHC transformations and invoke CHC satisfiability solvers.
Visualizing CHC Verification Conditions for Smart Contracts Auditing
Fioravanti F.
;
2024-01-01
Abstract
Smart contracts are programs stored on a blockchain that can be used to automate agreements and transactions. Their immutable nature carries the risk of financial losses due to vulnerabilities and bugs. Consequently, verification processes, often supported by formal methods, are indispensable in mitigating these risks. Constrained Horn Clauses (CHCs) are commonly used for representing verification conditions (VCs) in smart contract analysis and verification, and several tools have been developed based on CHCs. Despite their utility in formal verification, CHCs pose a challenge in terms of human readability. In this paper we present preliminary work in the development of a tool aimed at visualizing CHCs, helping experts inspect VCs and their correspondence with smart contract code during the auditing process. The tool combines different translations in order to generate Predicate Dependency Graphs (PDGs), depicting the relationships among CHC predicates that have been derived from smart contract functions and the properties under verification. While the current representation of PDGs is static, future developments aim to render it dynamic and user-friendly. This enhancement would enable auditors to selectively display sections of the PDGs, interact with nodes and the associated clauses and code, apply CHC transformations and invoke CHC satisfiability solvers.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
