mojtaba-eshghie / smartcontractdesignpatternsindcrgraphs Goto Github PK

Solidity Design Patterns Modeled by DCR Graphs

A comprehensive collection of high-level design patterns of smart contracts modeled in DCR graphs semantics.

📌 Table of Contents

🚀 DCR Graphs as a Formalism For Smart Contract Design Patterns

Design patterns are tried-and-true solutions to recurring problems, acting as templates to address well-known challenges [4]. When it comes to smart contracts, security is paramount as they manage funds, reactively execute rules, and are immutable or complicated to upgrade [1, 2]. Given the immutable and transparent nature of blockchain, any vulnerability can lead to irreversible consequences [6]. This is where DCR (Dynamic Condition Response) graphs come into play [5]. As a formalism, DCR graphs provide an encoding of the business process-level (contract-level) design of a contract, capturing its roles, action ordering, and time-based semantics. By leveraging DCR graphs, developers can visually represent and analyze the intricate logic of smart contracts, ensuring that they adhere to best practices and are free from potential pitfalls. It's a fusion of traditional design wisdom with uses in cutting-edge runtime verification [7, 8] of mentioned contract-level properties, ensuring that smart contracts not only function as intended but also stand robust against security threats.

📚 Cite Our Paper

Use the following bibtex entry to cite our work:

@inproceedings{captureDCR,
  title={Capturing Smart Contract Design with DCR Graphs},
  author={Mojtaba Eshghie and Wolfgang Ahrendt and Cyrille Artho and Thomas Troels Hildebrandt and Gerardo Schneider},
  booktitle={Proceedings of the 21st International Conference on Software Engineering and Formal Methods (SEFM 2023)},
  year={2023},
  address={Eindhoven University of Technology, Netherlands},
  month={November 8--10},
  organization={Eindhoven University of Technology (TU/e)},
  abstract={Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart-contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.},
}

📣 Feedback & Contributions: We welcome community feedback and contributions. If you have a design pattern that isn't listed here or suggestions to improve existing ones, please raise an issue or submit a pull request.

References:

1. N. Atzei, M. Bartoletti, and T. Cimoli, ‘A Survey of Attacks on Ethereum Smart Contracts SoK’, in Proceedings of the 6th International Conference on Principles of Security and Trust - Volume 10204, Berlin, Heidelberg: Springer-Verlag, Apr. 2017, pp. 164–186. doi: 10.1007/978-3-662-54455-6_8.
2. P. Tolmach, Y. Li, S.-W. Lin, Y. Liu, and Z. Li, ‘A Survey of Smart Contract Formal Specification and Verification’, ACM Comput. Surv., vol. 54, no. 7, p. 148:1-148:38, Jul. 2021, doi: 10.1145/3464421.
3. T. T. Hildebrandt, H. Normann, M. Marquard, S. Debois, and T. Slaats, ‘Decision Modelling in Timed Dynamic Condition Response Graphs with Data’, in Business Process Management Workshops, A. Marrella and B. Weber, Eds., in Lecture Notes in Business Information Processing. Cham: Springer International Publishing, 2022, pp. 362–374. doi: 10.1007/978-3-030-94343-1_28.
4. E. Gamma, R. Helm, R. Johnson, J. Vlissides, and G. Booch, Design Patterns: Elements of Reusable Object-Oriented Software, 1st edition. Reading, Mass: Addison-Wesley Professional, 1994.
5. T. Slaats, R. R. Mukkamala, T. Hildebrandt, and M. Marquard, ‘Exformatics Declarative Case Management Workflows as DCR Graphs’, in Business Process Management, F. Daniel, J. Wang, and B. Weber, Eds., in Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2013, pp. 339–354. doi: 10.1007/978-3-642-40176-3_28.
6. L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, ‘Making Smart Contracts Smarter’, in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, in CCS ’16. New York, NY, USA: Association for Computing Machinery, Oct. 2016, pp. 254–269. doi: 10.1145/2976749.2978309.
7. M. Eshghie, W. Ahrendt, C. Artho, T. T. Hildebrandt, and G. Schneider, ‘CLawK: Monitoring Business Processes in Smart Contracts’. arXiv, May 14, 2023. doi: 10.48550/arXiv.2305.08254.
8. M. Eshghie, ‘mojtaba-eshghie/CLawK’. Aug. 29, 2023. Accessed: Aug. 29, 2023. [Online]. Available: https://github.com/mojtaba-eshghie/CLawK