SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts

TL;DR

SciviK is a comprehensive framework that enhances the specification and verification of smart contracts, combining expressive annotations, a detailed EVM model, and integrated proof tools to improve security guarantees efficiently.

Contribution

It introduces a versatile framework with an expressive annotation system, a fine-grained EVM model, and IR-level verification integrating SMT and Coq for smart contract security.

Findings

Automatic verification of 151 properties within 2 seconds

Verified security properties for real-world DeFi contract

Efficient verification of multiple security patterns

Abstract

The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial) security guarantees for smart contracts or require huge proof effort. To address this challenge, we present SciviK, a versatile framework for specifying and verifying industrial-grade smart contracts. SciviK's versatile approach extends previous efforts with three key contributions: (i) an expressive annotation system enabling built-in directives for vulnerability pattern checking, neural-based loop invariant inference, and the verification of rich properties of real-world smart contracts (ii) a fine-grained model for the Ethereum Virtual Machine (EVM) that provides low-level execution semantics, (iii) an IR-level verification framework integrating both SMT solvers and the Coq proof assistant. We use SciviK to specify and verify security properties for 12 benchmark contracts and a real-world Decentralized Finance (DeFi) smart contract. Among all 158 specified security properties (in six types), 151 properties can be automatically verified within 2 seconds, five properties can be automatically verified after moderate modifications, and two properties are manually proved with around 200 lines of Coq code.