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, smart contracts, safety verification, semantics

Discipline

Information Security

Research Areas

Information Systems and Management

Publication

Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, Los Angeles, USA, Nov 7-11

First Page

921

Last Page

935

Identifier

10.1145/3548606.3559384

Publisher

ACM

City or Country

New York

Copyright Owner and License

Authors

Additional URL

http://doi.org/10.1145/3548606.3559384

Download

Share

COinS