Safety Verification of Declarative Smart Contracts

TL;DR

This paper introduces DCV, an automated safety verification tool for declarative smart contracts in DeCon, which uses mathematical induction and heuristic invariant inference to verify correctness efficiently.

Contribution

The paper presents DCV, a novel verification tool that automatically infers invariants and verifies safety properties of declarative smart contracts without developer annotations.

Findings

DCV successfully verifies 20 benchmark contracts from public repositories.

DCV outperforms baseline tools in verification speed.

DCV can verify contracts unsupported by existing tools.

Abstract

Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.