Yan Michalevsky talks on "Ethereum Bugs Through the Lens of Formal Verification" on Jan 21, 2018 to the Silicon Valley Ethereum meetup at an event [1] co-hosted by the Stanford Bitcoin Club [2] and held on Stanford campus. The material [3] Yan presents is joint work with Shelly Grossman [4] of Tel Aviv University, and others at Tel Aviv and VMware Research. The slides Yan used during the talk are available at the link [5] below. The video was arranged and paid for by the Proof of Authority network [6] and Igor Barinov.

Yan's abstract follows:"The DAO bug employed callbacks to steal $150M. Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object’s local states by external objects in unexpected fashions, thus breaking modularity. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contract executions, excluding these of the DAO or of contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state."
[1] [ Ссылка ]
[2] [ Ссылка ]
[3] [ Ссылка ]
[4] [ Ссылка ]
[5] [ Ссылка ]
[6] [ Ссылка ]

свернуть