4 papers
Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
Prokhor Shlyakhtun, Alexander Gryzlov, Vladimir Kukharenko +5
We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it control…
Systematization of Knowledge: Formal Verification of Consensus Protocols
Nikita Bondarev, Kirill Ziborov, Yury Yanovich
Formal verification is increasingly critical for blockchain consensus protocols, where subtle bugs can cause irreversible financial loss and network failure. Yet the literature on…
BugMagnifier: TON Transaction Simulator for Revealing Smart Contract Vulnerabilities
Yury Yanovich, Victoria Kovalevskaya, Maksim Egorov +6
The Open Network (TON) blockchain employs an asynchronous execution model that introduces unique security challenges for smart contracts. A primary concern is race conditions arisi…
From Paradigm Shift to Audit Rift: Empirical Analysis and Validation of Security Audit Methodologies for Asynchronous Smart Contract Systems
Yury Yanovich, Sergey Sobolev, Yash Madhwal +6
The Open Network (TON) is a high-performance blockchain platform designed for scalability and efficiency, leveraging an asynchronous execution model and a multi-layered architectur…