{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T14:03:45Z","timestamp":1779631425627,"version":"3.53.1"},"reference-count":35,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T00:00:00Z","timestamp":1776384000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2022YFB2703500"],"award-info":[{"award-number":["2022YFB2703500"]}]},{"name":"Beijing Natural Science Foundation","award":["M22040"],"award-info":[{"award-number":["M22040"]}]},{"name":"Research Foundation of Beijing Wuzi University","award":["2024XJKY29"],"award-info":[{"award-number":["2024XJKY29"]}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Big Data"],"published-print":{"date-parts":[[2026,6,1]]},"abstract":"<jats:p>The formal semantics of blockchain smart contracts are the foundation of formal verification. They can be used to establish formal models to verify the security of contracts and help developers understand the specific execution rules of contracts. However, the mathematical logic involved in such modeling poses a high barrier to entry and cannot be directly integrated with other program analysis methods. This article proposes a semantic graph generation approach, KSG, for blockchain smart contracts. First, the semantic rules of the contract language are formally defined, and a semantic interpreter and prover are constructed to automatically transform smart contract code into a scalable semantic graph. This graph incorporates semantic control flow information, semantic data flow information, execution rules, and verification constraints. Next, the generated semantic graph can be utilized for vulnerability detection and symbolic execution and supports iterative optimization based on the analysis results. Finally, the detailed process of semantic graph generation and analysis is demonstrated through the verification of the reentrancy contract and the honeypot contract.<\/jats:p>","DOI":"10.1177\/2167647x261430300","type":"journal-article","created":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:43:39Z","timestamp":1776426219000},"page":"179-192","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["KSG: A Symbolic Semantics Graph Generation Method of Smart Contract Based on the K Framework"],"prefix":"10.1177","volume":"14","author":[{"given":"Jie","family":"Li","sequence":"first","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."},{"name":"School of Computer Science and Engineering, Beihang University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yucheng","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaoyu","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi","family":"Ding","sequence":"additional","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yidan","family":"Zou","sequence":"additional","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jun","family":"Jin","sequence":"additional","affiliation":[{"name":"School of Computer Science and Artificial Intelligence, Beijing Wuzi University, Beijing, China."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","published-online":{"date-parts":[[2026,4,17]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464421"},{"key":"e_1_3_3_3_1","doi-asserted-by":"crossref","unstructured":"2.Garfatta I Klai K Gaaloul W et al. A survey on formal verification for solidity smart contracts. In: Proceedings of the 2021 Australasian Computer Science Week Multiconference. ACM; 2021; pp. 1\u201310.","DOI":"10.1145\/3437378.3437879"},{"key":"e_1_3_3_4_1","doi-asserted-by":"crossref","unstructured":"3.Schneidewind C Grishchenko I Scherer M et al. Ethor: Practical and provably sound static analysis of ethereum smart contracts. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. ACM; 2020; pp. 621\u2013640.","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_3_3_5_1","unstructured":"4.Frank J Aschermann C Holz T. {ETHBMC}: A bounded model checker for smart contracts. In: 29th USENIX Security Symposium (USENIX Security 20). USENIX; 2020; pp. 2757\u20132774."},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/360018.360025"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1988.0029"},{"key":"e_1_3_3_8_1","doi-asserted-by":"crossref","unstructured":"7.Luu L Chu D-H Olickel H et al. Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM; 2016; pp. 254\u2013269.","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_3_9_1","doi-asserted-by":"crossref","unstructured":"8.Tsankov P Dan A Drachsler-Cohen D et al. Securify: Practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. ACM; 2018; pp. 67\u201382.","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_3_10_1","unstructured":"9.Krupp J Rossow C. {teEther}: Gnawing at ethereum to automatically exploit smart contracts. In: 27th USENIX Security Symposium (USENIX Security 18). USENIX; 2018; pp. 1317\u20131333."},{"key":"e_1_3_3_11_1","doi-asserted-by":"crossref","unstructured":"10.Contro F Crosara M Ceccato M et al. Ethersolve: Computing an accurate controlflow graph from ethereum bytecode. In: 2021 IEEE\/ACM 29th International Conference on Program Comprehension (ICPC). IEEE; 2021; pp. 127\u2013137.","DOI":"10.1109\/ICPC52881.2021.00021"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111653"},{"key":"e_1_3_3_13_1","doi-asserted-by":"crossref","unstructured":"12.Fang Y Wu D Yi X et al. Beyond \u201cprotected\u201d and \u201cprivate\u201d: An empirical security analysis of custom function modifiers in smart contracts. In: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2023; pp. 1157\u20131168.","DOI":"10.1145\/3597926.3598125"},{"key":"e_1_3_3_14_1","doi-asserted-by":"crossref","unstructured":"13.Ghaleb A Rubin J Pattabiraman K. Achecker: Statically detecting smart contract access control vulnerabilities. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE). IEEE; 2023; pp. 945\u2013956.","DOI":"10.1109\/ICSE48619.2023.00087"},{"key":"e_1_3_3_15_1","volume-title":"A structural approach to operational semantics","author":"Plotkin GD","year":"1981","unstructured":"14.Plotkin GD. A structural approach to operational semantics. University of Edinburgh; 1981."},{"key":"e_1_3_3_16_1","doi-asserted-by":"crossref","unstructured":"15.Hildenbrandt E Saxena M Rodrigues N et al. Kevm: A complete formal semantics of the ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE; 2018; pp. 204\u2013217.","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_3_3_17_1","doi-asserted-by":"crossref","unstructured":"16.\u015etef\u0103nescu A Ciob\u00e2c\u0103 \u015e Mereuta R et al. All-path reachability logic. In: International Conference on Rewriting Techniques and Applications. Springer; 2014; pp. 425\u2013440.","DOI":"10.1007\/978-3-319-08918-8_29"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_3_20_1","doi-asserted-by":"crossref","unstructured":"19.Schwartz EJ Avgerinos T Brumley D. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: 2010 IEEE Symposium on Security and Privacy. IEEE; 2010; pp. 317\u2013331.","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_3_3_21_1","doi-asserted-by":"crossref","unstructured":"20.Ghaleb A Rubin J Pattabiraman K. eTainter: Detecting gas-related vulnerabilities in smart contracts. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2022; pp. 728\u2013739.","DOI":"10.1145\/3533767.3534378"},{"key":"e_1_3_3_22_1","doi-asserted-by":"crossref","unstructured":"21.Brent L Grech N Lagouvardos S et al. Ethainter: A smart contract security analyzer for composite vulnerabilities. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM; 2020; pp. 454\u2013469.","DOI":"10.1145\/3385412.3385990"},{"key":"e_1_3_3_23_1","doi-asserted-by":"crossref","unstructured":"22.Liu Y Cai L Chai C et al. An approach to optimize symbolic execution in ethereum smart contracts. In: 2024 IEEE 24th International Conference on Software Quality Reliability and Security Companion (QRS-C). IEEE; 2024; pp. 21\u201330.","DOI":"10.1109\/QRS-C63300.2024.00014"},{"key":"e_1_3_3_24_1","doi-asserted-by":"crossref","unstructured":"23.Dxo Soos M Paraskevopoulou Z et al. Hevm a fast symbolic execution framework for evm bytecode. In: International Conference on Computer Aided Verification. Springer; 2024; pp. 453\u2013465.","DOI":"10.1007\/978-3-031-65627-9_22"},{"key":"e_1_3_3_25_1","doi-asserted-by":"crossref","unstructured":"24.Braghin C Del Castillo G Riccobene E et al. Using symbolic model execution to detect vulnerabilities of smart contracts. In: International Conference on Rigorous State-Based Methods. Springer; 2025; pp. 31\u201351.","DOI":"10.1007\/978-3-031-94533-5_3"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2025.3555622"},{"key":"e_1_3_3_27_1","doi-asserted-by":"crossref","unstructured":"26.Yadav K Naval S. Cfg analysis for detecting vulnerabilities in smart contracts. In: International Conference on Smart Trends for Information Technology and Computer Communications. Springer; 2023; pp. 753\u2013763.","DOI":"10.1007\/978-981-99-0838-7_65"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.003.0004"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9_2"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628143"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_3_3_33_1","doi-asserted-by":"crossref","unstructured":"32.Amani S B\u00e9gel M Bortin M et al. Towards verifying ethereum smart contract bytecode in isabelle\/hol. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM; 2018; pp. 66\u201377.","DOI":"10.1145\/3167084"},{"key":"e_1_3_3_34_1","doi-asserted-by":"crossref","unstructured":"33.Park D Zhang Y Saxena M et al. A formal verification tool for ethereum vm bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM; 2018; pp. 912\u2013915.","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_3_3_35_1","doi-asserted-by":"crossref","unstructured":"34.Jiao J Kan S Lin S-W et al. Semantic understanding of smart contracts: Executable operational semantics of solidity. In: 2020 IEEE Symposium on Security and Privacy (SP). IEEE; 2020; pp. 1695\u20131712.","DOI":"10.1109\/SP40000.2020.00066"},{"key":"e_1_3_3_36_1","article-title":"Matching logic","volume":"13","author":"Rosu G","year":"2017","unstructured":"35.Rosu G. Matching logic. LMCS2017;13, Issue 4.","journal-title":"LMCS"}],"container-title":["Big Data"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/2167647X261430300","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/2167647X261430300","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/2167647X261430300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T13:46:22Z","timestamp":1779630382000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/2167647X261430300"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,17]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,6,1]]}},"alternative-id":["10.1177\/2167647X261430300"],"URL":"https:\/\/doi.org\/10.1177\/2167647x261430300","relation":{},"ISSN":["2167-6461","2167-647X"],"issn-type":[{"value":"2167-6461","type":"print"},{"value":"2167-647X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,17]]}}}