Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2022

Abstract

We propose VetSC, a novel UI-driven, program analysis guided model checking technique that can automatically extract contract semantics in DApps so as to enable targeted safety vetting. To facilitate model checking, we extract business model graphs from contract code that capture its intrinsic business and safety logic. To automatically determine what safety specifications to check, we retrieve textual semantics from DApp user interfaces. To exclude untrusted UI text, we also validate the UI-logic consistency and detect any discrepancies. We have implemented VetSC and applied it to 34 real-world DApps. Experiments have demonstrated that VetSC can accurately interpret smart contract code, enable autonomous safety vetting, and discover safety risks in real-world Dapps. Using our tool, we have successfully discovered 19 new safety risks in the wild, such as expired lottery tickets and double voting.

Keywords

decentralized apps, safety verification, semantics, smart contracts

Discipline

Finance and Financial Management | Information Security

Research Areas

Cybersecurity

Publication

CCS '22: Proceedings of the ACM Conference on Computer and Communications Security, Los Angeles, November 7-11

First Page

921

Last Page

935

ISBN

9781450394505

Identifier

10.1145/3548606.3559384

Publisher

ACM

City or Country

New York

Additional URL

https://doi.org/10.1145/3548606.3559384

Download

Share

COinS