{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T08:38:52Z","timestamp":1787560732027,"version":"build-2736575974"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Ensuring the reliability of smart contracts is of vital importance due to the wide adoption of smart contract programs in decentralized financial applications. However, statically checking many rich properties of smart contract programs can be challenging. On the other hand, dynamic validation approaches have shown promise for widespread adoption in practice. Nevertheless, as part of the programming environment for smart contracts, existing dynamic validation approaches have not provided programmers with a notion to clearly articulate the interface between components, especially for addresses representing opaque contract instances. We argue that the \u201cdesign-by-contract\u201d approach should complement the development of smart contract programs. Unfortunately, there is limited linguistic support for it in existing smart contract languages.<\/jats:p>\n                  <jats:p>In this paper, we design a Solidity language extension, ConSol, that supports behavioral contracts. ConSol provides programmers with a modular specification and monitoring system for both functional and latent address behaviors. The key capability of ConSol is to attach specifications to first-class addresses and monitor violations when invoking these addresses. We evaluate ConSol using 20 real-world cases, demonstrating its effectiveness in expressing critical conditions and preventing attacks. Additionally, we assess ConSol\u2019s efficiency and compare gas consumption with programs fixed with manually inserted assertions, showing that our approach introduces only marginal gas overhead. By separating specifications and implementations using behavioral contracts, ConSol assists programmers in writing more robust and readable smart contracts.<\/jats:p>","DOI":"10.1145\/3656416","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T12:27:20Z","timestamp":1718886440000},"page":"965-989","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Consolidating Smart Contracts with Behavioral Contracts"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3150-2033","authenticated-orcid":false,"given":"Guannan","family":"Wei","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4359-4625","authenticated-orcid":false,"given":"Danning","family":"Xie","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8039-0528","authenticated-orcid":false,"given":"Wuqi","family":"Zhang","sequence":"additional","affiliation":[{"name":"The Hong Kong University of Science and Technology, Hong Kong, China"},{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2619-2288","authenticated-orcid":false,"given":"Yongwei","family":"Yuan","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6515-0021","authenticated-orcid":false,"given":"Zhuo","family":"Zhang","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2000.895178"},{"key":"e_1_3_1_3_2","unstructured":"Hayden Adams Noah Zinsmeister and Dan Robinson. 2020. Uniswap v2 Core. (2020)."},{"key":"e_1_3_1_4_2","unstructured":"Hayden Adams Noah Zinsmeister Moody Salem River Keefer and Dan Robinson. 2021. Uniswap v3 core. Tech. rep. Uniswap Tech. Rep. (2021)."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428277"},{"key":"e_1_3_1_6_2","unstructured":"Beosin Alert. 2023. https:\/\/twitter.com\/BeosinAlert\/status\/1646481687445114881."},{"key":"e_1_3_1_7_2","unstructured":"Chickn Bao. 2023. Analysis and Response to the July 4th baoETH Exploit. https:\/\/medium.com\/baomunity\/analysisand-response-to-the-july-4th-baoeth-exploit-3d60b886fcce."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31500-9_15"},{"key":"e_1_3_1_9_2","unstructured":"Block Sec. 2022. https:\/\/twitter.com\/BlockSecTeam\/status\/1584959295829180416."},{"key":"e_1_3_1_10_2","unstructured":"BlockSec. 2023. https:\/\/twitter.com\/BlockSecTeam\/status\/1668084629654638592."},{"key":"e_1_3_1_11_2","unstructured":"BlockSec. 2023. https:\/\/blocksec.com\/blog\/yet-another-tragedy-of-precision-loss-an-in-depth-analysis-of-the-kyber-swap-incident-1."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485523"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385990"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"issue":"37","key":"e_1_3_1_16_2","first-page":"2","article-title":"A next-generation smart contract and decentralized application platform","volume":"3","author":"Buterin Vitalik","year":"2014","unstructured":"Vitalik Buterin et al. 2014. A next-generation smart contract and decentralized application platform. white paper 3, 37 (2014), 2\u20131.","journal-title":"white paper"},{"key":"e_1_3_1_17_2","unstructured":"Lorenzo Caminiti. 2023. Boost.Contract. https:\/\/www.boost.org\/doc\/libs\/1_82_0\/libs\/contract\/doc\/html\/index.html"},{"key":"e_1_3_1_18_2","unstructured":"CertiK. 2023. https:\/\/certik.medium.com\/qubit-bridge-collapse-exploited-to-the-tune-of-80-million-a7ab9068e1a0."},{"key":"e_1_3_1_19_2","unstructured":"CertiK Alert. 2023. https:\/\/twitter.com\/CertiKAlert\/status\/1647530789947469825."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/11916246_5"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Haoxian Chen Gerald Whitters Mohammad Javad Amiri Yuepeng Wang and Boon Thau Loo. 2022. Declarative smart contracts. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 281\u2013293.","DOI":"10.1145\/3540250.3549121"},{"key":"e_1_3_1_22_2","first-page":"122","volume-title":"SETSS (Lecture Notes in Computer Science, Vol. 12154)","author":"Chen Xiaohong","year":"2019","unstructured":"Xiaohong Chen and Grigore Rosu. 2019. K - A Semantic Framework for Programming Languages and Formal Analysis. In SETSS (Lecture Notes in Computer Science, Vol. 12154). Springer, 122\u2013158."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678888"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Michael Coblenz. 2017. Obsidian: A Safer Blockchain Programming Language. In 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C). 97\u201399. https:\/\/doi.org\/10.1109\/ICSE-C.2017.150 10.1109\/ICSE-C.2017.150","DOI":"10.1109\/ICSE-C.2017.150"},{"key":"e_1_3_1_25_2","unstructured":"Consensys. 2023. Consensys. https:\/\/www.consensys.net\/."},{"key":"e_1_3_1_26_2","unstructured":"Consensys. 2023. solc-typed-ast. https:\/\/github.com\/Consensys\/solc-typed-ast."},{"key":"e_1_3_1_27_2","first-page":"138","volume-title":"Financial Cryptography Workshops (Lecture Notes in Computer Science, Vol. 11599)","author":"Crafa Silvia","year":"2019","unstructured":"Silvia Crafa, Matteo Di Pirro, and Elena Zucca. 2019. Is Solidity Solid Enough?. In Financial Cryptography Workshops (Lecture Notes in Computer Science, Vol. 11599). Springer, 138\u2013153."},{"key":"e_1_3_1_28_2","unstructured":"crytic. 2024. medusa. https:\/\/github.com\/crytic\/medusa."},{"key":"e_1_3_1_29_2","unstructured":"Numen Cyber. 2023. https:\/\/twitter.com\/numencyber\/status\/1669278694744150016?cxt=HHwWgMDS9Z2IvKouAAAA."},{"key":"e_1_3_1_30_2","unstructured":"Phil Daian. 2016. The analysis of the DAO exploit. https:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/."},{"key":"e_1_3_1_31_2","first-page":"117","volume-title":"ICFP","author":"Dimoulas Christos","year":"2016","unstructured":"Christos Dimoulas, Max S. New, Robert Bruce Findler, and Matthias Felleisen. 2016. Oh Lord, please don\u2019t let contracts be misunderstood (functional pearl). In ICFP. ACM, 117\u2013131."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034800"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/EDCC.2018.00036"},{"key":"e_1_3_1_34_2","unstructured":"Ethereum. 2023. Solidity Documentation. https:\/\/docs.soliditylang.org\/en\/v0.8.21\/types.html."},{"key":"e_1_3_1_35_2","unstructured":"Sturdy Finance. 2023. Sturdy Finance. https:\/\/sturdy.finance\/."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_1_37_2","unstructured":"fountry-rs. 2024. Foundry. https:\/\/github.com\/foundry-rs\/foundry."},{"key":"e_1_3_1_38_2","doi-asserted-by":"crossref","unstructured":"Asem Ghaleb Julia Rubin and Karthik Pattabiraman. 2022. eTainter: detecting gas-related vulnerabilities in smart contracts. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 728\u2013739.","DOI":"10.1145\/3533767.3534378"},{"key":"e_1_3_1_39_2","doi-asserted-by":"crossref","unstructured":"Asem Ghaleb Julia Rubin and Karthik Pattabiraman. 2023. AChecker: Statically Detecting Smart Contract Access Control Vulnerabilities. Proc. ACM ICSE (2023).","DOI":"10.1109\/ICSE48619.2023.00087"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Gustavo Grieco Will Song Artur Cygan Josselin Feist and Alex Groce. 2020. Echidna: effective usable and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis. 557\u2013560.","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","unstructured":"Alex Groce and Gustavo Grieco. 2021. echidna-parade: A tool for diverse multicore smart contract fuzzing. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. 658\u2013661.","DOI":"10.1145\/3460319.3469076"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_3_1_45_2","unstructured":"PeckShield Inc. 2023. https:\/\/twitter.com\/peckshield\/status\/1690877589005778945."},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00066"},{"key":"e_1_3_1_47_2","volume-title":"ICIS","author":"Ke Ping Fan","year":"2022","unstructured":"Ping Fan Ke and Ka Chung Boris Ng. 2022. Bank Error in Whose Favor? A Case Study of Decentralized Finance Misgovernance. In ICIS. Association for Information Systems."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385982"},{"key":"e_1_3_1_49_2","doi-asserted-by":"crossref","unstructured":"Zeqin Liao Sicheng Hao Yuhong Nan and Zibin Zheng. 2023. SmartState: Detecting State-Reverting Vulnerabilities in Smart Contracts via Fine-Grained State-Dependency Analysis. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. 980\u2013991.","DOI":"10.1145\/3597926.3598111"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2019.8668038"},{"key":"e_1_3_1_51_2","unstructured":"MevRefund. 2022. https:\/\/twitter.com\/MevRefund\/status\/1580917351217627136."},{"key":"e_1_3_1_52_2","volume-title":"Eiffel: The Language","author":"Meyer Bertrand","year":"1991","unstructured":"Bertrand Meyer. 1991. Eiffel: The Language. Prentice-Hall."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TOOLS.1998.711043"},{"key":"e_1_3_1_55_2","unstructured":"Miner. 2023. https:\/\/twitter.com\/minerercx\/status\/1757787864299934023."},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000096"},{"key":"e_1_3_1_57_2","unstructured":"Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. Decentralized business review (2008)."},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_1_60_2","unstructured":"Paradigm. 2023. Reth: Modular contributor-friendly and blazing-fast implementation of the Ethereum protocol. https:\/\/github.com\/paradigmxyz\/reth."},{"key":"e_1_3_1_61_2","unstructured":"Parquery. 2023. icontract. Accessed: July 13 2023."},{"key":"e_1_3_1_62_2","unstructured":"PeckShield Inc. 2023. https:\/\/twitter.com\/peckshield\/status\/1626493024879673344."},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3546186.3549930"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454112"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23413"},{"key":"e_1_3_1_66_2","unstructured":"RugDoctorApe. 2023. https:\/\/twitter.com\/RugDoctorApe\/status\/1565739119606890498."},{"key":"e_1_3_1_67_2","unstructured":"Runtime Verification. 2018. ERC20-Semantics: Formal semantics and verification properties for ERC20 smart contracts. https:\/\/github.com\/runtimeverification\/erc20-semantics. Accessed on 2024-03-24."},{"key":"e_1_3_1_68_2","unstructured":"S7iter. 2023. https:\/\/medium.com\/@S7iter_\/erc2771-multicall-arbitrary-address-spoofing-attack-analysis-andrecurrence-48c57fdb9a98."},{"key":"e_1_3_1_69_2","unstructured":"Scribble. 2024. Scribble Documentation. https:\/\/docs.scribble.codes\/"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01807-7_3"},{"key":"e_1_3_1_71_2","unstructured":"SharkTeam. 2023. https:\/\/app.chainaegis.com\/home\/news\/detail?contentId=341&lang=en-US."},{"key":"e_1_3_1_72_2","doi-asserted-by":"crossref","unstructured":"Chaofan Shou Shangyin Tan and Koushik Sen. 2023. ItyFuzz: Snapshot-Based Fuzzer for Smart Contract. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. 322\u2013333.","DOI":"10.1145\/3597926.3598059"},{"key":"e_1_3_1_73_2","unstructured":"SlowMist. 2023. https:\/\/twitter.com\/SlowMist_Team\/status\/1644936375924584449."},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485540"},{"key":"e_1_3_1_75_2","unstructured":"Yannis Smaragdakis Neville Grech Sifis Lagouvardos Konstantinos Triantafyllou and Tony Rocco Valentine. 2023 Program Analysis for High-Value Smart Contract Vulnerabilities: Techniques and Insights. (2023)."},{"key":"e_1_3_1_76_2","unstructured":"Solidity. 2023. https:\/\/docs.soliditylang.org\/en\/develop\/security-considerations.html#use-the-checks-effectsinteractions-pattern."},{"key":"e_1_3_1_77_2","unstructured":"Solidity. 2023. Solidity Contracts: Function Modifiers. https:\/\/docs.soliditylang.org\/en\/latest\/contracts.html#functionmodifiers Accessed on 2023-11-17."},{"key":"e_1_3_1_78_2","unstructured":"Solidity Developers. 2023. Solidity Documentation: Function Modifiers. Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.20\/contracts.html#modifiers Accessed on July 20 2023."},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00085"},{"key":"e_1_3_1_80_2","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_3_1_81_2","unstructured":"SunWeb3Sec. 2022. https:\/\/github.com\/SunWeb3Sec\/DeFiHackLabs\/blob\/main\/past\/2022\/README.md#20220204-tecraspace---any-token-is-destroyed."},{"key":"e_1_3_1_82_2","unstructured":"SunWeb3Sec. 2023. https:\/\/github.com\/SunWeb3Sec\/DeFiHackLabs\/blob\/main\/src\/test\/ERC20TokenBank_exp.sol."},{"key":"e_1_3_1_83_2","unstructured":"SunWeb3Sec. 2023. DeFi Hacks Reproduce - Foundry. https:\/\/github.com\/SunWeb3Sec\/DeFiHackLabs."},{"key":"e_1_3_1_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498665"},{"key":"e_1_3_1_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464421"},{"key":"e_1_3_1_86_2","unstructured":"Trail of Bits. 2023. Trail of Bits. https:\/\/www.trailofbits.com\/."},{"key":"e_1_3_1_87_2","unstructured":"Uno.Reinsure. 2022. Umbrella Network Hacked: $700K Lost. https:\/\/medium.com\/uno-re\/umbrella-network-hacked-700k-lost-97285b69e8c7."},{"key":"e_1_3_1_88_2","unstructured":"Fabian Vogelsteller and Vitalik Buterin. 2023. EIP-20: Token Standard. https:\/\/eips.ethereum.org\/EIPS\/eip-20."},{"key":"e_1_3_1_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360615"},{"key":"e_1_3_1_90_2","unstructured":"Guannan Wei Danning Xie Wuqi Zhang Yongwei Yuan and Zhuo Zhang. 2024. ConSol Artifact. https:\/\/github.com\/Kraks\/contract-for-contract\/."},{"key":"e_1_3_1_91_2","unstructured":"XCarnival. 2023. https:\/\/twitter.com\/XCarnival_Lab\/status\/1541226298399653888."},{"key":"e_1_3_1_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"},{"key":"e_1_3_1_93_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00061"},{"key":"e_1_3_1_94_2","doi-asserted-by":"crossref","unstructured":"Liyi Zhou Xihan Xiong Jens Ernstberger Stefanos Chaliasos Zhipeng Wang Ye Wang Kaihua Qin Roger Wattenhofer Dawn Song and Arthur Gervais. 2022. SoK: Decentralized Finance (DeFi) Attacks. IACR Cryptol. ePrint Arch. (2022) 1773.","DOI":"10.1109\/SP46215.2023.10179435"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656416","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:41:56Z","timestamp":1751647316000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656416"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":93,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656416"],"URL":"https:\/\/doi.org\/10.1145\/3656416","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}