{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T17:40:18Z","timestamp":1757612418964,"version":"3.44.0"},"reference-count":35,"publisher":"Frontiers Media SA","license":[{"start":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T00:00:00Z","timestamp":1756944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100031478","name":"NextGenerationEU","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100031478","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["frontiersin.org"],"crossmark-restriction":true},"short-container-title":["Front. Comput. Sci."],"abstract":"<jats:p>Smart contracts are software that runs in blockchain and expresses the rules of an agreement between parties. An incorrect smart contract might allow blockchain users to violate its rules and even jeopardize its expected security. Smart contracts cannot be easily replaced to patch a bug since the nature of contracts requires them to be immutable. More problems occur when a smart contract is written in a general-purpose language, such as Java, whose executions, in a blockchain, could hang the network, break consensus or violate data encapsulation. To limit these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in the blockchain. This so-called <jats:italic>off-chain<\/jats:italic> verification is <jats:italic>optional<\/jats:italic> because programmers are not forced to use it. This paper presents a general framework for the verification of smart contracts, instead, that is part of the protocol of the nodes and applies when the code of the smart contracts gets installed. It is a <jats:italic>mandatory<\/jats:italic> entry filter that bans code that does not abide by the verification rules. Consequently, such rules become part of the consensus rules of the blockchain. Therefore, an improvement in the verification protocol entails a consensus update of the network. This paper describes an implementation of a smart contracts application layer with protocol-based verification for smart contracts written in the Takamaka subset of Java, that filters only those smart contracts whose execution in blockchain is not dangerous. This application layer runs on top of a consensus engine such as Tendermint and its derivatives Ignite and CometBFT (proof of stake), or Mokamint (proof of space). This paper provides examples of actual implementations of verification rules that check if the smart contracts satisfy some constraints required by the Takamaka language. This paper shows that protocol-based verification works and reports how consensus updates are implemented. It shows actual experiments as well as limits to its use, mainly related to the fact that protocol-based verification must be fast and its complexity must never explode, or otherwise, it would compromise the performance of the blockchain network.<\/jats:p>","DOI":"10.3389\/fcomp.2025.1596804","type":"journal-article","created":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:04:32Z","timestamp":1756991072000},"update-policy":"https:\/\/doi.org\/10.3389\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An application layer with protocol-based java smart contract verification"],"prefix":"10.3389","volume":"7","author":[{"given":"Luca","family":"Olivieri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fausto","family":"Spoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Tagliaferro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1965","published-online":{"date-parts":[[2025,9,4]]},"reference":[{"key":"B1","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-70697-9_13","article-title":"\u201cBeyond hellman's time-memory trade-offs with applications to proofs of space,\u201d","author":"Abusalah","year":"2017","journal-title":"Proceedings of Advances in Cryptology, the 23rd International Conference on the Theory and Applications of Cryptology and Information Security (ASIACRYPT'17), part II"},{"volume-title":"Mastering Bitcoin: Unlocking Digital Cryptocurrencies","year":"2017","author":"Antonopoulos","key":"B2"},{"volume-title":"Mastering Ethereum: Building Smart Contracts and Dapps","year":"2018","author":"Antonopoulos","key":"B3"},{"key":"B4","first-page":"11","article-title":"\u201cTowards a sound construction of EVM bytecode control-flow graphs,\u201d","volume-title":"Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs, FTfJP 2024","author":"Arceri","year":"2024"},{"key":"B5","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/978-3-319-10879-7_31","article-title":"\u201cProofs of space: when space is of the essence,\u201d","author":"Ateniese","year":"2014","journal-title":"Proceedings of the 9th International Conference on Security and Cryptography for Networks (SCN'14)"},{"key":"B6","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","article-title":"\u201cA survey of attacks on ethereum smart contracts (SoK),\u201d","volume-title":"6th International Conference on Principles of Security and Trust (POST'17)","author":"Atzei","year":"2017"},{"key":"B7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","article-title":"The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems","volume":"72","author":"Bagnara","year":"2008","journal-title":"Sci. Comput. Progr"},{"key":"B8","unstructured":"Buterin\n              V.\n            \n          \n          Ethereum Whitepaper\n          \n          2013"},{"key":"B9","unstructured":"2025"},{"key":"B10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.tcs.2019.02.001","article-title":"Algorand: a secure and efficient distributed ledger","volume":"777","author":"Chen","year":"2019","journal-title":"Theor. Comput. Sci"},{"key":"B11","unstructured":"Blockchain Security &Ethereum Smart Contract Audits\n          \n          2025"},{"key":"B12","doi-asserted-by":"publisher","first-page":"2701","DOI":"10.1007\/s10586-022-03756-3","article-title":"Fungible and non-fungible tokens with snapshots in java","volume":"26","author":"Crosara","year":"2023","journal-title":"Cluster Comput"},{"key":"B13","unstructured":"Dua\n              R.\n            \n          \n          Ethlint \u2013 Documentation\n          \n          2025"},{"key":"B14","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-662-48000-7_29","article-title":"\u201cProofs of space,\u201d","author":"Dziembowski","year":"2015","journal-title":"Proceedings of Advances in Cryptology (CRYPTO 2015)"},{"key":"B15","first-page":"8","article-title":"\u201cSlither: a static analysis framework for smart contracts,\u201d","volume-title":"2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB@ICSE'19)","author":"Feist","year":"2019"},{"key":"B16","first-page":"557","article-title":"\u201cEchidna: effective, usable, and fast fuzzing for smart contracts,\u201d","volume-title":"29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'20)","author":"Grieco","year":"2020"},{"key":"B17","doi-asserted-by":"publisher","first-page":"104142","DOI":"10.1016\/j.jnca.2025.104142","article-title":"A comprehensive survey of smart contracts vulnerability detection tools: techniques and methodologies","volume":"237","author":"Hejazi","year":"2025","journal-title":"J. Netw. Comput. Applic"},{"key":"B18","doi-asserted-by":"publisher","first-page":"57037","DOI":"10.1109\/ACCESS.2022.3169902","article-title":"Ethereum smart contract analysis tools: a systematic review","volume":"10","author":"Kushwaha","year":"2022","journal-title":"IEEE Access"},{"key":"B19","unstructured":"Kwon\n              J.\n            \n          \n          Tendermint: Consensus without Mining\n          \n          2014"},{"key":"B20","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1145\/2976749.2978309","article-title":"\u201cMaking smart contracts smarter,\u201d","author":"Loi","year":"2016"},{"volume-title":"Java Generics and Collections: Speed Up the Java Development Process","year":"2006","author":"Naftalin","key":"B21"},{"key":"B22","unstructured":"Nakamoto\n              S.\n            \n          \n          34691875\n          Bitcoin: A Peer-to-Peer Electronic Cash System\n          \n          2008"},{"key":"B23","doi-asserted-by":"publisher","first-page":"1864","DOI":"10.1007\/s10664-019-09796-5","article-title":"An exploratory study of smart contracts in the ethereum blockchain platform","volume":"25","author":"Oliva","year":"2020","journal-title":"Empir. Softw. Eng"},{"key":"B24","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-662-63958-0_28","article-title":"\u201cOn-chain smart contract verification over tendermint,\u201d","author":"Olivieri","year":"2021","journal-title":"Financial Cryptography and Data Security. FC 2021 International Workshops"},{"key":"B25","unstructured":"The OpenZeppelin Security Audit\n          \n          2025"},{"key":"B26","doi-asserted-by":"publisher","first-page":"111653","DOI":"10.1016\/j.jss.2023.111653","article-title":"Enhancing ethereum smart-contracts static analysis by computing a precise control-flow graph of ethereum bytecode","volume":"200","author":"Pasqua","year":"2023","journal-title":"J. Syst. Softw"},{"journal-title":"A Hacking of More than","year":"2016","author":"Popper","key":"B27"},{"key":"B28","unstructured":"Solhint - Official Website\n          \n          2025"},{"key":"B29","article-title":"Vulnerability detection in ethereum smart contracts via machine learning: a qualitative analysis","author":"Ressi","year":"2024","journal-title":"arXiv preprint arXiv:2407.18639"},{"key":"B30","first-page":"621","article-title":"\u201ceThor: practical and provably sound static analysis of ethereum smart contracts,\u201d","volume-title":"Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS '20","author":"Schneidewind","year":"2020"},{"key":"B31","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/s12599-020-00656-x","article-title":"The energy consumption of blockchain technology: beyond myth","volume":"62","author":"Sedlmeir","year":"2020","journal-title":"Bus. Inf. Syst. Eng"},{"key":"B32","first-page":"122","article-title":"\u201cA java framework for smart contracts,\u201d","volume-title":"3rd Workshop on Trusted Smart Contracts (WTSC'19)","author":"Spoto","year":"2019"},{"key":"B33","article-title":"\u201cA formalization of signum's consensus,\u201d","volume-title":"9th Workshop on Trusted Smart Contracts (WTSC'25), Lecture Notes in Computer Science, Miyakojima, Japan","author":"Spoto","year":"2025"},{"key":"B34","doi-asserted-by":"publisher","first-page":"2099","DOI":"10.1007\/s10586-022-03688-y","article-title":"On the use of generic types for smart contracts","volume":"26","author":"Spoto","year":"2023","journal-title":"Cluster Comput"},{"key":"B35","doi-asserted-by":"publisher","DOI":"10.1145\/3194113.3194115","article-title":"\u201cSmartCheck: static analysis of ethereum smart contracts,\u201d","author":"Tikhomirov","year":"2018","journal-title":"2018 IEEE\/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB)"}],"container-title":["Frontiers in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fcomp.2025.1596804\/full","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:04:36Z","timestamp":1756991076000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fcomp.2025.1596804\/full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,4]]},"references-count":35,"alternative-id":["10.3389\/fcomp.2025.1596804"],"URL":"https:\/\/doi.org\/10.3389\/fcomp.2025.1596804","relation":{},"ISSN":["2624-9898"],"issn-type":[{"type":"electronic","value":"2624-9898"}],"subject":[],"published":{"date-parts":[[2025,9,4]]},"article-number":"1596804"}}