SmartPulse: Automated Checking of Temporal Properties in Smart Contracts

Authors: Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig

Abstract: Smart contracts are programs that run on the blockchain and digitally enforce the execution of contracts between parties. Because bugs in smart contracts can have serious monetary consequences, ensuring the correctness of such software is of utmost importance. In this paper, we present a novel technique, and its implementation in a tool called SmartPulse, for automatically verifying full functional correctness of smart contracts. SmartPulse is the first smart contract verification tool that is capable of checking liveness properties, which ensure that "something good" will eventually happen (e.g., "I will eventually receive my refund"). We experimentally evaluate SmartPulse on a broad class of smart contracts and properties and show that (a) SmartPulse allows automatically verifying important liveness properties, (b) it is competitive with or better than state-of-the-art tools for safety verification, and (c) it can automatically generate attacks for vulnerable contracts.

Full Text: pdf

Bibtex:

@inproceedings{stephens2021smartpulse,
 title={SmartPulse: Automated Checking of Temporal Properties in Smart Contracts},
 author={Stephens, Jon and Ferles, Kostas and Mariano, Benjamin and Lahiri, Shuvendu and Dillig, Isil},
 booktitle={Proceedings of the 42nd IEEE Symposium on Security and Privacy},
 year={2021},
 organization={IEEE}
 }