TY - GEN
T1 - Behavioral simulation for smart contracts
AU - Beillahi, Sidi Mohamed
AU - Ciocarlie, Gabriela
AU - Emmi, Michael
AU - Enea, Constantin
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/6/11
Y1 - 2020/6/11
N2 - While smart contracts have the potential to revolutionize many important applications like banking, trade, and supply-chain, their reliable deployment begs for rigorous formal verification. Since most smart contracts are not annotated with formal specifications, general verification of functional properties is impeded. In this work, we propose an automated approach to verify unannotated smart contracts against specifications ascribed to a few manually-annotated contracts. In particular, we propose a notion of behavioral refinement, which implies inheritance of functional properties. Furthermore, we propose an automated approach to inductive proof, by synthesizing simulation relations on the states of related contracts. Empirically, we demonstrate that behavioral simulations can be synthesized automatically for several ubiquitous classes like tokens, auctions, and escrow, thus enabling the verification of unannotated contracts against functional specifications.
AB - While smart contracts have the potential to revolutionize many important applications like banking, trade, and supply-chain, their reliable deployment begs for rigorous formal verification. Since most smart contracts are not annotated with formal specifications, general verification of functional properties is impeded. In this work, we propose an automated approach to verify unannotated smart contracts against specifications ascribed to a few manually-annotated contracts. In particular, we propose a notion of behavioral refinement, which implies inheritance of functional properties. Furthermore, we propose an automated approach to inductive proof, by synthesizing simulation relations on the states of related contracts. Empirically, we demonstrate that behavioral simulations can be synthesized automatically for several ubiquitous classes like tokens, auctions, and escrow, thus enabling the verification of unannotated contracts against functional specifications.
KW - Blockchain
KW - Refinement
KW - Simulation
KW - Smart contracts
U2 - 10.1145/3385412.3386022
DO - 10.1145/3385412.3386022
M3 - Conference contribution
AN - SCOPUS:85086821549
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 470
EP - 486
BT - PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Donaldson, Alastair F.
A2 - Torlak, Emina
PB - Association for Computing Machinery
T2 - 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020
Y2 - 15 June 2020 through 20 June 2020
ER -