Skip to main content
Springer Nature Link
Log in

Secure Smart Contract Generation Based on Petri Nets

  • Chapter
  • First Online:
Blockchain Technology for Industry 4.0

Part of the book series: Blockchain Technologies ((BT))

  • 2760 Accesses

Abstract

Existing blockchain and smart contract development ecosystems do not support to design, develop, and verify secure smart contracts before deploying them. Recent attacks (see DAO hack [5]) on insecure smart contracts have caused a lot of financial loss—to avoid such issues in the future, we need better methods for creating secure smart contracts before deploying them in a blockchain. In this chapter, we present a method and a prototype tool to generate secure smart contracts based on Petri Nets. Our method allows to design and generate a secure smart contract template that can be deployed on a supported blockchain platform (e.g. Ethereum) with very little additional effort. One of the main advantages that our method brings into the smart contract development ecosystem is introducing a formal way to visually model, simulate, and verify business logic/workflows prior to the smart contract code generation. Modeling the smart contracts via Petri Nets helps the developers to minimize the logical errors—by verifying certain Petri Net properties such as deadlocks—during the modeling stage itself. Furthermore, our approach presents a technology-independent way to import and export the modeled use-case logic which can be translated into different smart contract language later.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 85.59
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 105.49
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
EUR 147.69
Price includes VAT (France)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/.

References

  1. Atluri V, Huang W (1996) An authorization model for workflows. In: Computer security—ESORICS 96, 4th European symposium on research in computer security, Rome, Italy, 25–27 September, 1996, Proceedings, pp 44–64. https://doi.org/10.1007/3-540-61770-1_27

  2. Atluri V, Huang W (2000) A petri net based safety analysis of workflow authorization models. J Comput Secur 8(2/3):209–240. http://content.iospress.com/articles/journal-of-computer-security/jcs113

  3. Choudhury O, Rudolph N, Sylla I, Fairoza N, Das (2018) A Auto-generation of smart contracts from domain-specific ontologies and semantic rules. In: IEEE Blockchain Conference, vol 2018

    Google Scholar 

  4. Delmolino K, Arnett M, Kosba AE, Miller A, Shi E (2015) Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. IACR Cryptology ePrint Archive, vol 2015, p 460. https://eprint.iacr.org/2015/460.pdf

  5. Dhillon V, Metcalf D, Hooper M (2017) The DAO hacked. Apress, Berkeley, pp 67–78. https://doi.org/10.1007/978-1-4842-3081-7_6

  6. Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8):453–457. http://portal.acm.org/citation.cfm?doid=360933.360975

  7. A Pinna A, Tonelli R, Orrú M, Marchesi M (2018) A Petri Nets model for blockchain analysis. Comput J 61(9):1374–1388. https://doi.org/10.1093/comjnl/bxy001. Automatic code generation from high-level Petri-Nets for model driven systems engineering

  8. Esparza J (1998) Decidability and complexity of Petri Net problems an introduction. In: Lectures on Petri Nets I: basic models. Springer, Berlin, p 55. http://www.springerlink.com/index/0nl351947367n07l.pdf

  9. Ethereum (2018) Solidity solidity. https://solidity.readthedocs.io/en/develop/. Accessed August 2018

  10. Ethereum (2018) What are smart contracts—EthereumWiki. http://www.ethereumwiki.com/ethereum-wiki/smart-contracts/. Accessed March 2018

  11. Freytag T, Sänger M (2014) Woped-an educational tool for workflow nets. In: BPM (Demos), p 31

    Google Scholar 

  12. García-Bañuelos L, Ponomarev A, Dumas M, Weber I (2017) Optimized execution of business processes on blockchain. In: Business process management—15th international conference, BPM 2017, Barcelona, Spain, 10–15 September 2017, Proceedings, pp 130–146. https://doi.org/10.1007/978-3-319-65000-5_8

  13. Haber S, Stornetta WS (1991) How to time-stamp a digital document. J Cryptol 3(2):99–111. https://doi.org/10.1007/BF00196791

  14. Jamal M, Zafar NA (2016) Transformation of activity diagram into coloured Petri Nets using weighted directed graph. In: 2016 international conference on frontiers of information technology (FIT). IEEE, pp 181–186. http://ieeexplore.ieee.org/document/7866750/

  15. Jensen K, Kristensen LM, Wells L (2007) Coloured petri nets and CPN tools for modelling and validation of concurrent systems. STTT 9(3–4):213–254. https://doi.org/10.1007/s10009-007-0038-x

  16. Kasinathan P, Cuéllar J (2018) Securing the integrity of workflows in iot. In: Proceedings of the 2018 International Conference on Embedded Wireless Systems and Networks, EWSN 2018. Madrid, Spain, 14–16 February 2018, pp 252–257. http://dl.acm.org/citation.cfm?id=3234908

  17. Kasinathan P, Cuéllar J (2018) Workflow-aware security of integrated mobility services. In: Computer security—23rd European symposium on research in computer security, ESORICS 2018, Barcelona, Spain, 3–7 September 2018, Proceedings, Part II, pp 3–19. https://doi.org/10.1007/978-3-319-98989-1_1

  18. Kasinathan P, Cuellar J (2019) Securing emergent IoT applications. Springer International Publishing, Cham, pp 99–147. https://doi.org/10.1007/978-3-030-17601-3_3

  19. Kiepuszewski B, ter Hofstede A, van der Aalst W (2003) Fundamentals of control flow in workflows. Acta Inf 39(3):143–209. https://doi.org/10.1007/s00236-002-0105-4

  20. Knorr K (2000) Dynamic access control through petri net workflows. In: 16th annual computer security applications conference (ACSAC 2000), 11–15 December 2000, New Orleans, Louisiana, USA, pp 159–167. https://doi.org/10.1109/ACSAC.2000.898869

  21. Luu L, Chu DH, Olickel H, Saxena P, Hobor A (2016) Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC conference on computer and communications security—CCS’16. ACM Press, New York, pp 254–269. http://dl.acm.org/citation.cfm?doid=2976749.2978309

  22. Mavridou A, Laszka A (2017) Designing secure ethereum smart contracts: a finite state machine based approach

    Google Scholar 

  23. Mavridou A, Laszka A (2018) Tool demonstration: Fsolidm for designing secure ethereum smart contracts. In: Principles of security and trust—7th international conference, POST 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, 14–20 April 2018, Proceedings. pp 270–277. https://doi.org/10.1007/978-3-319-89722-6_11

  24. Mavridou A, Laszka A, Stachtiari E, Dubey A (2019) Verisolid: correct-by-design smart contracts for ethereum. CoRR abs/1901.01292. http://arxiv.org/abs/1901.01292

  25. Modelio—open source tool (2018) Modelio—The open source modeling tool. https://www.modelio.org/. Accessed Aug 2018

  26. Mortensen KH (2000) Automatic code generation method based on coloured petri net models applied on an access control system. In: Nielsen M, Simpson D (eds) Application and theory of petri nets 2000. Springer, Berlin, pp 367–386

    Chapter  Google Scholar 

  27. Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541–580. http://ieeexplore.ieee.org/document/24143/

  28. Nakamoto S (2008) Bitcoin: a peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf. Accessed Oct 2018

  29. Nakamura H, Miyamoto K, Kudo M (2018) Inter-organizational business processes managed by blockchain. In: Hacid H, Cellary W, Wang H, Paik HY, Zhou R (eds) Web Information Systems Engineering - WISE 2018. Springer International Publishing, Cham, pp 3–17

    Chapter  Google Scholar 

  30. Narayanan A, Bonneau J, Felten E, Miller A, Goldfeder S (2016) Bitcoin and cryptocurrency technologies: a comprehensive introduction. Princeton University Press, Princeton

    Google Scholar 

  31. Petri CA (1966) Communication with automata. http://edoc.sub.uni-hamburg.de/informatik/volltexte/2010/155/

  32. Philippi S (2006) Automatic code generation from high-level petri-nets for model driven systems engineering. J Syst Softw 79(10):1444–1455. http://www.sciencedirect.com/science/article/pii/S0164121205001901, architecting Dependable Systems

  33. Reisig W (1985) Petri nets: an introduction, EATCS monographs on theoretical computer science, vol 4. Springer, Berlin. https://doi.org/10.1007/978-3-642-69968-9

  34. Swan M (2015) Blockchain: blueprint for a new economy. O’Reilly Media, Inc

    Google Scholar 

  35. Szabo N (2001) Smart contracts: building blocks for digital markets, 1996. EXTROPY: J Transhumanist Thought. http://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo.best.vwh.net/smart_contracts_2.html

  36. Tateishi T, Yoshihama S, Sato N, Saito S (2019) Automatic smart contract generation using controlled natural language and template. IBM J Res Dev 1–1

    Google Scholar 

  37. van der Aalst WMP (1997) Verification of workflow nets. In: Lecture notes in computer science (including subseries Lecture notes in artificial intelligence and lecture notes in bioinformatics), vol 1248, pp 407–426. Springer, Berlin. http://link.springer.com/10.1007/3-540-63139-9_48

  38. van der Aalst WMP (1998) The application of Petri nets to workflow management. J Circuit Syst Comput 08(01):21–66. http://www.worldscientific.com/doi/abs/10.1142/S0218126698000043

  39. van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2011) Soundness of workflow nets: classification, decidability, and analysis. Form Asp Comput 23(3):333–363. https://doi.org/10.1007/s00165-010-0161-4

  40. van der Aalst WM, Ter Hofstede AH (2005) Yawl: yet another workflow language. Inf Syst 30(4):245–275

    Google Scholar 

  41. Weber M, Kindler E (2003) The petri net markup language. Springer, Berlin, pp 124–144. https://doi.org/10.1007/978-3-540-40022-6_7

Download references

Author information

Authors and Affiliations

  1. Siemens AG, Corporate Technology, Munich, Germany

    Nejc Zupan, Prabhakaran Kasinathan, Jorge Cuellar & Markus Sauer

  2. University of Passau, IT-Security Group, Passau, Germany

    Prabhakaran Kasinathan & Jorge Cuellar

Authors
  1. Nejc Zupan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Prabhakaran Kasinathan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jorge Cuellar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Markus Sauer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nejc Zupan .

Editor information

Editors and Affiliations

  1. Universidade do Vale do Rio dos Sinos, Sao Leopoldo, Brazil

    Rodrigo da Rosa Righi

  2. ICT Lab, Information and Communications Technologies (Inatel), Santa Rita do Sapucai, Minas Gerais, Brazil

    Antonio Marcos Alberti

  3. Endicott College of International Studies, Woosong University, Daejeon, Korea (Republic of)

    Madhusudan Singh

7 Appendix

7 Appendix

1.1 7.1 Petri Net Markup Language (PNML) Example

The exported PNML code of the supply chain use case presented in Sect. 5.1 is shown in listing 1. Some parts of the XML code are omitted for readability (brevity) reasons.

figure a

1.2 7.2 Solidity Code

The generated Solidy smart contract of the supply chain use case presented in Sect. 5.1 is shown in listing 2.

figure b

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Zupan, N., Kasinathan, P., Cuellar, J., Sauer, M. (2020). Secure Smart Contract Generation Based on Petri Nets. In: Rosa Righi, R., Alberti, A., Singh, M. (eds) Blockchain Technology for Industry 4.0. Blockchain Technologies. Springer, Singapore. https://doi.org/10.1007/978-981-15-1137-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-981-15-1137-0_4

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-15-1136-3

  • Online ISBN: 978-981-15-1137-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation