The HEVM Symbolic Simulation Framework
In realm of digital finance, a decade-long revolution has reshaped financial systems. Amidst this upheaval, substantial research investments focus on validating digital contracts — complex programs managing billion-dollar transactions. The sakes are high, where even a minor bug can cause irreversible losses, sometimes reaching hundreds of millions of USD [1]. Hence, verifying the correctness of these contracts is paramount. In this talk, we will discuss the details of the HEVM symbolic execution framework [2] that can be used to verify properties of digital contracts written in EVM bytecode, the most popular digital contract execution framework.
[1] Explore real-world examples at https://de.fi/rekt-database
[2] Dive into the HEVM framework at https://github.com/ethereum/hevm/
Online Meeting link (for those who cannot join in person): Webex link
Meeting number: 2515 059 6247
Meeting password: AHeeYm8X3M5
Speaker Biography
Mate Soos obtained his PhD from INRIA in 2009 and has since been working both in academia and industry on formal verification, breaking lightweight cryptographic primitives, and IT security. He is the author of the SAT solver CryptoMiniSat, and has worked with Kuldeep Meel on the model counters ApproxMC and Ganak, as well as the almost-uniform sampler CMSGgen, and the probabilistically approximate sampler UniGen. He has also helped reverse engineer and break the lightweight ciphers HiTag2 and Megamos, among others, through a combination of SAT solving, algebraic cryptanalysis, GPGPU, and FPGA programming. He is currently employed by the Ethereum Foundation to work on Formal Methods tooling for the Ethereum ecosystem, and regularly does research at the National University of Singapore on formal methods.
