|VeriSmart： A Highly Precise Safety Verifier for Ethereum Smart Contracts (오학주 교수, 고려대)|
o 일정 및 장소
- 일시: 2019.12.10(화) 16:00~
- 장소: N1건물 110호
Title: VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts
This talk will present VeriSmart, our recent work on verification of smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high precision and recall at the same time, inherently limited to producing annoying false alarms or missing critical bugs. By contrast, VeriSmart aims for an uncompromising analyzer that performs exhaustive verification with high precision or scalability, thereby greatly reducing the burden of manually checking undiscovered or incorrectly-reported issues. To achieve this goal, we present a new domain-specific algorithm for verifying smart contracts, which is able to automatically discover and leverage transaction invariants that are essential for precisely analyzing smart contracts. Evaluation with real-world smart contracts shows that VeriSmart can detect all arithmetic bugs with a negligible number of false alarms, far outperforming existing analyzers.
Hakjoo Oh is an Associate Professor in the Computer Science Department at Korea University. He received his Bachelors degree in Computer Science from KAIST in 2005 and his PhD from Seoul National University in 2012. He was a research associate at the center of software analysis for error-free computing in SNU before joining Korea University in 2015. His research interest includes program analysis, testing, synthesis, and repair. He has published papers in top venues in programming languages, software engineering, and software security such as PLDI, OOPSLA, ICSE, FSE, and S&P.