Program Verification on Ethereum
-
12:00 10th November 2017 ( Michaelmas Term 2017 )
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/