{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T13:26:40Z","timestamp":1775309200990,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"Icelandic Research Fund","award":["218202-05(1-3)"],"award-info":[{"award-number":["218202-05(1-3)"]}]},{"DOI":"10.13039\/501100014832","name":"Reykjavik University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100014832","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    In this article, we focus on\n                    <jats:sc>TinySol<\/jats:sc>\n                    , a minimal calculus for Solidity smart contracts, introduced by Bartoletti, Galletta and Murgia. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics for that language. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system that statically ensures both noninterference and call integrity; hence, well-typed programs satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.\n                  <\/jats:p>","DOI":"10.1145\/3786766","type":"journal-article","created":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T13:45:43Z","timestamp":1767015943000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Sound Type System for Secure Currency Flow"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2197-3018","authenticated-orcid":false,"given":"Luca","family":"Aceto","sequence":"first","affiliation":[{"name":"Reykjav\u00edk University, Reykjav\u00edk, Iceland and Gran Sasso Science Institute, L\u2019Aquila, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8859-9844","authenticated-orcid":false,"given":"Daniele","family":"Gorla","sequence":"additional","affiliation":[{"name":"Dip. Informatica, Sapienza Univ. di Roma, Roma, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8219-2285","authenticated-orcid":false,"given":"Stian","family":"Lybech","sequence":"additional","affiliation":[{"name":"Reykjav\u00edk University, Reykjav\u00edk, Iceland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,21]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.1"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-73709-1_25"},{"key":"e_1_3_3_4_2","unstructured":"Amal\u00a0Jamil Ahmed. 2004. Semantics of Types for Mutable State. PhD thesis Princeton University. Retrieved from http:\/\/www.ccs.neu.edu\/home\/amal\/ahmedsthesis.pdf"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","unstructured":"Aslan Askarov and Andrew\u00a0C. Myers. 2011. Attacker control and impact for confidentiality and integrity. Log. Methods Comput. Sci. 7 3 (2011) 1\u201333. DOI: 10.2168\/LMCS-7(3:17)2011","DOI":"10.2168\/LMCS-7(3:17)2011"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","unstructured":"Aslan Askarov and Andrei Sabelfeld. 2007. Gradual release: Unifying declassification encryption and key release policies. In 2007 IEEE Symposium on Security and Privacy (SP \u201907) 207\u2013221. DOI: 10.1109\/SP.2007.22","DOI":"10.1109\/SP.2007.22"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31500-9_15"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485523"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_2"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_17"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_9"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","unstructured":"Michael\u00a0R. Clarkson and Fred\u00a0B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18 6 (2010) 1157\u20131210. DOI: 10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","unstructured":"Silvia Crafa Matteo\u00a0Di Pirro and Elena Zucca. 2019. Is solidity solid enough? In Financial Cryptography Workshops.","DOI":"10.1007\/978-3-030-43725-1_11"},{"key":"e_1_3_3_18_2","unstructured":"DAO. 2016. The DAO smart contract. Retrieved from http:\/\/etherscan.io\/address\/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code"},{"key":"e_1_3_3_19_2","doi-asserted-by":"crossref","unstructured":"Thomas D. Dickerson Paul Gazzillo Maurice Herlihy Vikram Saraph and Eric Koskinen. 2018. Proof-carrying smart contracts. In Financial Cryptography Workshops.","DOI":"10.1007\/978-3-662-58820-8_22"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","unstructured":"Josselin Feist Gustavo Grieco and Alex Groce. Slither: A static analysis framework for smart contracts. In 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain. IEEE\/ACM 8\u201315. DOI: 10.1109\/WETSEB.2019.00008","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"e_1_3_3_21_2","unstructured":"Ethereum Foundation. 2022. Solidity Documentation. Retrieved January 15 2024 from https:\/\/docs.soliditylang.org\/"},{"key":"e_1_3_3_22_2","unstructured":"Arn\u00f3r Fri\u00f0riksson. 2024. Interpreter and Type Checker for TinySol. Retrieved March 3 2024 from https:\/\/github.com\/Zepeacedust\/TinySol-Type-checker"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.5220\/0009564100390051"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","unstructured":"J.\u00a0A. Goguen and J. Meseguer. 1982. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy 11\u201320. DOI: 10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_3"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523717"},{"key":"e_1_3_3_27_2","first-page":"243","volume-title":"Principles of Security and Trust","author":"Grishchenko Ilya","year":"2018","unstructured":"Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A semantic framework for the security analysis of Ethereum smart contracts. In Principles of Security and Trust. Lujo Bauer and Ralf K\u00fcsters (Eds.), Springer International Publishing, Cham, 243\u2013269."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","unstructured":"Daniel Hedin Arnar Birgisson Luciano Bello and Andrei Sabelfeld. 2014. JSFlow: Tracking information flow in JavaScript and its APIs. In Symposium on Applied Computing (SAC \u201914). Yookun Cho Sung Y. Shin Sang-Wook Kim Chih-Cheng Hung and Jiman Hong (Eds.) ACM 1663\u20131671. DOI: 10.1145\/2554850.2554909","DOI":"10.1145\/2554850.2554909"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1286821.1286822"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102343"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","unstructured":"Atsushi Igarashi Benjamin\u00a0C. Pierce and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23 3 (2001) 396\u2013450. DOI: 10.1145\/503502.503505","DOI":"10.1145\/503502.503505"},{"key":"e_1_3_3_32_2","doi-asserted-by":"crossref","unstructured":"Sukrit Kalra Seep Goel Mohan Dhawan and Subodh Sharma. 2018. ZEUS: analyzing safety of smart contracts. In 25th Annual Network and Distributed System Security Symposium. The Internet Society. Retrieved from https:\/\/www.ndss-symposium.org\/wp-content\/uploads\/2018\/02\/ndss2018_09-1_Kalra_paper.pdf","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 2005. Type-based information flow analysis for the pi-calculus. Acta Informatica 42 4\u20135 (2005) 291\u2013347. DOI: 10.1007\/s00236-005-0179-x","DOI":"10.1007\/s00236-005-0179-x"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_3_35_2","unstructured":"Stian Lybech. 2025. A Type-Theoretic Approach to Smart-Contract Safety. PhD thesis Reykjav\u00edk University. Retrieved from https:\/\/iris.landsbokasafn.is\/en\/publications\/a-type-theoretic-approach-to-smart-contract-safety"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"e_1_3_3_37_2","unstructured":"Andrew\u00a0C. Myers Lantian Zheng Steve Zdancewic Stephen Chong and Nathaniel Nystrom. 2006. Jif 3.0: Java Information Flow. Retrieved from http:\/\/www.cs.cornell.edu\/jif"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","unstructured":"Hanne\u00a0Riis Nielson and Flemming Nielson. 2007. Semantics with Applications: An Appetizer. Springer-Verlag London. DOI: 10.1007\/978-1-84628-692-6","DOI":"10.1007\/978-1-84628-692-6"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_8"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","unstructured":"Fran\u00e7ois Pottier and Vincent Simonet. 2003. Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25 1 (2003) 117\u2013158. DOI: 10.1145\/596980.596983","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","unstructured":"Vineet Rajani Iulia Bastys Willard Rafnsson and Deepak Garg. 2017. Type systems for information flow control: The question of granularity. ACM SIGLOG News 4 1 (2017) 6\u201321. DOI: 10.1145\/3051528.3051531","DOI":"10.1145\/3051528.3051531"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","unstructured":"Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. J. Log. Algebraic Methods Program 79 6 (2010) 397\u2013434. DOI: 10.1016\/j.jlap.2010.03.012","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784756"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","unstructured":"Andrei Sabelfeld and Andrew\u00a0C. Myers. 2003. Language-based information-flow security. IEEE J. Sel. Areas Commun. 21 1 (2003) 5\u201319. DOI: 10.1109\/JSAC.2002.806121","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_3_3_46_2","first-page":"1156","article-title":"Scripting smart contracts for distributed ledger technology","author":"Seijas Pablo\u00a0Lamela","year":"2016","unstructured":"Pablo\u00a0Lamela Seijas, Simon\u00a0J. Thompson, and Darryl McAdams. 2016. Scripting smart contracts for distributed ledger technology. IACR Cryptol. ePrint Arch. (2016), 1156.","journal-title":"IACR Cryptol. ePrint Arch"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268975"},{"key":"e_1_3_3_49_2","unstructured":"smlxl inc. 2023. An Ethereum virtual machine opcodes interactive reference Retrieved from https:\/\/evm.codes\/"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. A logical approach to type soundness. J. ACM 71 6 Article 40 (Nov. 2024) 1\u201375. DOI: 10.1145\/3676954","DOI":"10.1145\/3676954"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","unstructured":"Palina Tolmach Yi\u00a0Li Shang-Wei Lin Yang Liu and Zengxiang Li. A survey of smart contract formal specification and verification. ACM Computing Surveys 54 7 Article 148 (2020) 1\u201338. DOI: 10.1145\/3464421","DOI":"10.1145\/3464421"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030629"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","unstructured":"Dennis\u00a0M. Volpano Cynthia\u00a0E. Irvine and Geoffrey Smith. 1996. A sound type system for secure flow analysis. J. Comput. Security 4 2\/3 (1996) 167\u2013188. DOI: 10.3233\/JCS-1996-42-304","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","unstructured":"Renlord Yang Toby Murray Paul Rimba and Udaya Parampalli. 2019. Empirically analyzing Ethereum's gas mechanism. In IEEE European Symposium on Security and Privacy Workshops. IEEE 310\u2013319. DOI: 10.1109\/EuroSPW.2019.00041","DOI":"10.1109\/EuroSPW.2019.00041"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3786766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T12:37:59Z","timestamp":1775306279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3786766"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,21]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3786766"],"URL":"https:\/\/doi.org\/10.1145\/3786766","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,21]]},"assertion":[{"value":"2025-03-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-16","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}