Precise Static Modeling of Ethereum “Memory”

on YouTube ↗15m

" summary

Declarative modeling of EVM memory using datalog rules and a gigahorse decompiler recovers source-level arguments and array allocations from low-level MSTORE/MLOAD/SHA3 patterns, modeling 92.7% of MLOADs and 94.6% of MSTOREs across 70,063 verified contracts. A repeated-calls detector using this model achieves 85.9% precision versus Securify’s 16.1%. A fallback gas analysis reports 1,468 warnings; dynamic replays hit 292 cases and confirm 272 failures for a 93% precision. Work informs EIP impact and wins Ethereum Foundation recognition.

AI-written summary · about

" chapters (19)

1. 0:00Precise Static Modeling of Ethereum "Memory"
2. 0:13Ethereum: a programmable blockchain
3. 0:49Ethereum Virtual Machine (EVM)
4. 1:19Solidity Smart Contract Example
5. 2:24"Memory" hides a lot of implicit computation!
6. 3:17Smart Contract Example - Decompiled
7. 5:35Main takeaway: High-level memory abstractions from low-level input
8. 6:28Analysis - Input
9. 7:10Analysis - Interfacing and mutually recursive analysis modules
10. 7:49Analysis - Intermediate and output relations
11. 8:21Analysis - Symbolic Value Creation
12. 9:13A taste: memory analysis recursive with others
13. 9:41A taste of final outputs
14. 10:28Evaluation - General Metrics
15. 10:45Memory modeling benefits analysis of external calis
16. 11:00Client Analysis - Repeated Calls
17. 12:08Evaluation - Repeated Calls
18. 12:42Client Analysis - Gas Consumption - EIP-1884
19. 14:01Evaluation - EIP-1884 Gas Cost

" related talks

• 15mSymbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart ContractsYannis Smaragdakis, Neville Grech, Ilias Tsatiris, Sifis Lagouvardos, Konstantinos Triantafyllou · OOPSLA 2021
• 31mSo, you think you can write an EVM decompiler?Yannis Smaragdakis · Solidity Summit 2025
• 21mWeak Memory Demands Model-based Compiler TestingLuke Geeson · The Future of Weak Memory 2024
• 14mMaat: Analyzing and Optimizing Overcharge on Blockchain StorageSen Yang, Ting Chen, Jingwei Li, Xiapu Luo, Xiaosong Zhang, Zheyuan He, Zihao Li, Ao Qiao, Feng Luo, Gelei Deng, Shuwei Song · FAST '25
• 15mSymbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic ChoiceJay Richards, Daniel Wright, Simon Cooksey, Mark Batty · OOPSLA 2025
• 01h 06mKeynote: Memory of Past and Future – Wasm’s Evolving Model of StoreAndreas Rossberg · ISMM 2024
• 22mReconciling High-level Optimizations and Low-level Code in LLVMJuneyoung Lee · OOPSLA 2018
• 19mVarLifter: Recovering Variables and Types from Bytecode of Solidity Smart ContractsWei Song, Jeff Huang, Yichuan Li · OOPSLA 2024