Skip to main content

Program Verification on Ethereum

Yoichi Hirai ( Ethereum Foundation )

Abstract:
The talk covers what Ethereum is, why I think Ethereum is a practical target of program verification techniques, and what I and others have been doing. Ethereum is a network protocol that runs an instance of a virtual machine (EVM) that no single owner or administrator can stop. The unstoppable nature introduces unstoppable buggy applications. In the most controversial case, many nodes agreed on an ad-hoc protocol change to rescue a considerable amount of funds from an unstoppable buggy program. Unstoppable verified programs would be better. For this goal, I defined EVM in Lem, Grigore Rosu and his team defined it in K-framework, and some commercial static analyzers were developed. I'll also touch the challenges in writing test cases for comparing EVM implementations.

Bio:
Yoichi Hirai is a formal verification engineer at Ethereum Foundation. After defending a thesis on proof theory at the University of Tokyo, he worked at a Japanese national research institute and then moved to Dresden for joining a microkernel verification project with FireEye. Later, he changed his target to EVM seeking a simpler computer.  For details, see http://yoichihirai.com/

Share this: