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.
TolmachP, LiY, LinS-W, et al.A survey of smart contract formal specification and verification. ACM Comput Surv2022;54(7):1–38.
2.
GarfattaI, KlaiK, GaaloulW, 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–10.
3.
SchneidewindC, GrishchenkoI, SchererM, 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–640.
4.
FrankJ, AschermannC, HolzT. {ETHBMC}: A bounded model checker for smart contracts. In: 29th USENIX Security Symposium (USENIX Security 20). USENIX; 2020; pp. 2757–2774.
5.
AllenFE, CockeJ. A program data flow analysis procedure. Commun ACM1976;19(3):137.
6.
CowardPD. Symbolic execution systems—A review. Softw Eng J UK1988;3(6):229–239.
7.
LuuL, ChuD-H, OlickelH, et al.Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM; 2016; pp. 254–269.
8.
TsankovP, DanA, Drachsler-CohenD, 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–82.
9.
KruppJ, RossowC. {teEther}: Gnawing at ethereum to automatically exploit smart contracts. In: 27th USENIX Security Symposium (USENIX Security 18). USENIX; 2018; pp. 1317–1333.
10.
ControF, CrosaraM, CeccatoM, 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–137.
11.
PasquaM, BeniniA, ControF, et al.Enhancing ethereum smart-contracts static analysis by computing a precise control-flow graph of ethereum bytecode. J Syst Softw2023;200:111653.
12.
FangY, WuD, YiX, et al.Beyond “protected” and “private”: 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–1168.
13.
GhalebA, RubinJ, PattabiramanK. Achecker: Statically detecting smart contract access control vulnerabilities. In: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE; 2023; pp. 945–956.
14.
PlotkinGD. A structural approach to operational semantics. University of Edinburgh; 1981.
15.
HildenbrandtE, SaxenaM, RodriguesN, 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–217.
16.
ŞtefănescuA, CiobâcăŞ, MereutaR, et al.All-path reachability logic. In: International Conference on Rewriting Techniques and Applications. Springer; 2014; pp. 425–440.
17.
KingJC. Symbolic execution and program testing. Commun ACM1976;19(7):385–394.
18.
CadarC, SenK. Symbolic execution for software testing: Three decades later. Commun ACM2013;56(2):82–90.
19.
SchwartzEJ, AvgerinosT, BrumleyD. 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–331.
20.
GhalebA, RubinJ, PattabiramanK. 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–739.
21.
BrentL, GrechN, LagouvardosS, 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–469.
22.
LiuY, CaiL, ChaiC, 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–30.
23.
Dxo,Soos M, ParaskevopoulouZ, et al.Hevm, a fast symbolic execution framework for evm bytecode. In: International Conference on Computer Aided Verification. Springer; 2024; pp. 453–465.
24.
BraghinC, Del CastilloG, RiccobeneE, et al.Using symbolic model execution to detect vulnerabilities of smart contracts. In: International Conference on Rigorous State-Based Methods. Springer; 2025; pp. 31–51.
25.
ChenJ, ShaoZ, YangS, et al.Numscout: Unveiling numerical defects in smart contracts using LLM-pruning symbolic execution. IIEEE Trans Software Eng2025;51(5):1538–1553.
26.
YadavK, NavalS. Cfg analysis for detecting vulnerabilities in smart contracts. In: International Conference on Smart Trends for Information Technology and Computer Communications. Springer; 2023; pp. 753–763.
27.
WinskelG. The Formal Semantics of Programming Languages: An Introduction. MIT press: Cambridge, Massachusetts; 1993; pp. 11–13.
28.
RoşuG, ŞerbănutăTF. An overview of the k semantic framework. J Log Algebr Program2010;79(6):397–434.
29.
NipkowT, WenzelM, PaulsonLC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer: Berlin Heidelberg; 2002; pp. 9–26.
30.
MulliganDP, OwensS, GrayKE, et al.Lem: Reusable engineering of real-world semantics. SIGPLAN Not2014;49(9):175–188.
31.
HiraiY. Defining the ethereum virtual machine for interactive theorem provers. In: Financial Cryptography and Data Security: FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April 7, 2017, Revised Selected Papers. Springer; 2017; pp. 520–535.
32.
AmaniS, BégelM, BortinM, 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–77.
33.
ParkD, ZhangY, SaxenaM, 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–915.
34.
JiaoJ, KanS, LinS-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–1712.
