While the immutability of smart contracts ensures unparalleled trust and transparency, it is also a doubleedged sword, as any coding errors can lead to substantial financial losses and complex mitigation endeavours. VeriSolid is a security mitigation tool that offers a 'correct by design' platform, enabling developers to create and verify smart contracts using predefined property templates. After ensuring the correctness of the design, VeriSolid facilitates the automatic generation of equivalent Solidity code. Our motivational example is a prominent decentralized exchange (DEX), Uniswap, which is responsible for over 82% of DEX transactions. Our experiments uncover and resolve verification issues in two out of four VeriSolid templates. Additionally, we propose seven new templates, enhancing the VeriSolid platform through its open-source project. This research endeavor has yielded a significant enhancement in VeriSolid's coverage percentage, which represents the percentage of available software requirement specifications that can be formally represented and verified in VeriSolid. This study increased it from 45.6% to 90.5% based on a dataset consisting of 555 requirement specifications, thus enabling the verification of a wider range of property specifications.
Smart contracts, evolving from cryptocurrencies pioneered by Bitcoin [
Solutions are varied [
We have selected the Uniswap V2 Solidity code from the decentralized exchange (DEX) ecosystem as our real-world motivational example [14]. DEXs operate without intermediaries, facilitating peer-to-peer cryptocurrency transactions in a non-custodial manner. Our selection criteria included transaction count and percentage of total volume across all monitored DEXs on Etherscan.io. Uniswap V2 accounted for 82.51% of total transactions [15].
VeriSolid [16] employs a correct-by-design approach for smart contract development, emphasizing correctness during the design phase before code generation. However, our testing revealed verification errors and challenges in specifying desired properties, resulting in execution outcomes misaligned with defined properties. This paper addresses these issues, significantly improving VeriSolid’s coverage from 45.6% to 90.5% across a dataset of 555 specifications, thereby enabling broader property verification.
We offer a concise overview of VeriSolid in Section 2, with an analysis of and improvements to VeriSolid’s functionality in Section 3. Our contributions have been integrated into the VeriSolid codebase, now accessible to the community. Section 4 summarizes our findings and outlines potential future enhancements.
VeriSolid is a correct-by-design tool that enables users to design contracts by modeling them as state machines. Using the Solidity language, users can specify details such as transition guards, statements, inputs, and contract definitions (e.g., internal variables). The user has access to predefined templates to specify desired properties on the contract. Once verification is triggered, VeriSolid translates the designed model and specified properties into BIP [ 17, 18] and then into CTL (Computational Tree Logic) [19] specifications in nuXmv [20]. The nuXmv tool subsequently verifies whether the CTL properties hold for the contract model. In the case of negative results, it provides counterexamples at the nuXmv level and then translates them back to the BIP level. In this paper, we assume the reader has basic knowledge of CTL [21].
While specifying our Uniswap model and verifying properties within the VeriSolid environment, a surprising incorrect verification verdict resulting from the second and third templates (Table 1) came to our attention. We explain this issue using a simpler model, i.e., one of the predefined smart contracts of the VeriSolid project called “RockPaperScissors” and depicted in Fig. 1.
The problematic scenario can be observed by providing “close#cancelPlay” as values to the second template definition (Table 1), which hence asserts that “the event (close) can happen only after the event (cancelPlay)”. Surprisingly, the verification tool yields a result indicating that this property holds, despite our intuitive understanding suggesting otherwise. The same issue is also encountered with the third template, with parameters “close#cancelReveal#finish”, which asserts that “if (close) happens, (cancelReveal) can happen only after (nfiish) happens”. Once again, the verification reports that this property holds, despite the property trivially not holding.
Our investigation revealed that in the original VeriSolid tool, weak until ([ ]) properties were incorrectly encoded in nuXmv as strong until ([ ]) properties with an additional fairness constraint. Specifically, this encoding occurred for templates 2 and 3 (Table 1), which led to the generation of fairness constraints for the first (resp. third) parameter of the 2 (resp. 3) template [22]. These wrong encodings are the root cause of the issues described previously.
Fairness constraints must be satisfied infinitely often within the system [ 23]. However, this encoding does not accurately capture the semantics of weak until properties. For instance, in the scenarios described earlier, it would require visiting innfiitely often states such as “close” in the second template example and “finish” in the third template example, which is impossible due to the absence of a loopback mechanism. Since FAIRNESS(p) is used in nuXmv to restrict the verification to executions in which p holds infinitely often, this results in the fact that there are no paths satisfying this property; consequently any property becomes trivially true [21]. To address this issue, proper encoding of weak until using constructs supported by the verification engine is required. To this extent, we can leverage the equivalence [ ] = ¬[¬ (¬ ∧ ¬)] (see e.g., [24]), and rewrite each occurrence of weak until accordingly wherever needed.
We have also extended the supported verification templates of VeriSolid according to the most common CTL patterns [25]. Table 1 presents the VeriSolid property templates’ logical descriptions and categorizations [25] between parentheses. The “CTL Formula” column represents the encoding in CTL. “Sts.” corresponds to the status: “–” (unchanged), “fixed” (resolved in this paper), “impl” (introduced in a VeriSolid paper [16], implemented here), and “new” (introduced and implemented here). The last column reveals pattern coverage on a 555-example dataset [25]. The table encompasses all patterns with a score exceeding 1 in [25]. Our work significantly boosts VeriSolid’s coverage, from 45.6% to 90.5%, enhancing its property verification capabilities. With these improvements, it is now possible to continue our analysis of the Uniswap smart contract.
In this paper, we have improved the verification capabilities of VeriSolid, a correct-by-design development environment for smart contracts. Our investigations on this tool revealed incorrect encodings in nuXmv of two property templates. We corrected these issues and further contributed by implementing twelve new property templates. As a result, the verification templates now cover 90.5% of the 555 specification examples collected by Dwyer [ 25]. All these contributions are now available in the VeriSolid Git repository [26].
For future work, we are considering the following items. First, extend the current verification using advanced features in nuXmv by, e.g., encoding patterns in Linear Temporal Logic (LTL) [27] to then utilize advanced SAT-based model checking algorithms. Second, allow infinite state variables (reals, integers) beyond Boolean variables in guards and use SMT-based verification [ 28] available in nuXmv. Third, add checks to ensure the specified model is deadlock-free (each state has at least one future state). Fourth, bring back counterexamples in user level inspection. Finally, increase the granularity of the “lock” concept from FSolidM [29] (VeriSolid’s predecessor) to eradicate reentrancy vulnerability in a “foolproof” manner, ensuring single transition execution at a time and preventing function nesting. Since this mechanism is overly restrictive, it is recommended to establish distinct locks for each method. Furthermore, we can offer users to define specific locks for individual transitions to ensure mutual exclusivity in concurrent transaction executions. We thank Dr. A. Mavridou for her invaluable support throughout this research endeavor. We extend our appreciation to the anonymous reviewers whose insightful comments greatly contributed to enhancing the paper’s quality. Prof. M. Roveri acknowledges partial funding from the CrossCon EU-funded project under Grant Agreement 101070537. [13] I. Grishchenko, M. Maffei, C. Schneidewind, A semantic framework for the security analysis of Ethereum smart contracts, in: Principles of Security and Trust: 7th International Conference, POST 2018, Springer, 2018, pp. 243–269. doi:10.1007/978-3-319-89722-6_10. [14] etherscan.io, Uniswap (UNI) token tracker | Etherscan, 2023. URL: https://etherscan.io/ token/0x1f9840a85d5af5bf1d1762f925bdaddc4201f984. [15] etherscan.io, DEX activity | Etherscan, 2023. URL: http://etherscan.io/stat/dextracker. [16] A. Mavridou, A. Laszka, E. Stachtiari, A. Dubey, VeriSolid: Correct-by-design smart contracts for Ethereum, in: International Conference on Financial Cryptography and Data Security. FC 2019, Springer, 2019, pp. 446–465. doi:978-3-030-32101-7_27. [17] A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber, T. Nguyen, J. Sifakis, Rigorous component-based system design using the BIP framework, IEEE Softw. 28 (2011) 41–48.
URL: https://doi.org/10.1109/MS.2011.27. doi:10.1109/MS.2011.27. [18] S. Bliudze, A. Cimatti, M. Jaber, S. Mover, M. Roveri, W. Saab, Q. Wang, Formal verification of infinite-state BIP models, in: International Symposium on Automated Technology for Verification and Analysis, Springer, 2015, pp. 326–343. doi: 10.1007/ 978-3-319-24953-7_25. [19] E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, in: Workshop on logic of programs, Springer, 1981, pp. 52–71. doi:10.1007/BFb0025774. [20] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta, The nuXmv symbolic model checker, in: Computer Aided Verification: 26th International Conference, CAV 2014, Springer, 2014, pp. 334–342. doi:10.1007/978-3-319-08867-9_22. [21] C. Baier, J.-P. Katoen, Principles of model checking, MIT Press, 2008. [22] A. Mavridou, VerifyContract.js, 2023. URL: https://github.com/anmavrid/smart-contracts/ blob/master/src/plugins/VerifyContract/VerifyContract.js. [23] R. Cavada, A. Cimatti, G. Keighren, E. Olivetti, M. Pistore, M. Roveri, NuSMV 2.6 tutorial, 2015. URL: https://nusmv.fbk.eu/NuSMV/tutorial/v26/tutorial.pdf. [24] M. Dwyer, Property pattern mappings for CTL, 2023. URL: https://matthewbdwyer.github.
io/psp/patterns/ctl.html. [25] M. B. Dwyer, G. S. Avrunin, J. C. Corbett, Patterns in property specifications for finite-state verification, in: Proceedings of the 21st International Conference on Software Engineering, 1999, pp. 411–420. doi:10.1145/302405.302672. [26] A. Mavridou, VerifyContract.js, 2023. URL: https://github.com/anmavrid/smart-contracts. [27] A. Pnueli, The temporal logic of programs, in: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society, 1977, pp. 46–57. URL: https://doi.org/10.1109/SFCS.1977.32. doi:10.1109/SFCS.1977.32. [28] C. W. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, Satisfiability Modulo Theories, volume 185 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2009. doi:10.3233/ 978-1-58603-929-5-825. [29] A. Mavridou, A. Laszka, Designing secure Ethereum smart contracts: A finite state machine based approach, in: Financial Cryptography and Data Security. FC 2018, Springer, 2018, pp. 523–540. doi:978-3-662-58387-6_28.