Feeds: iCal | RSS | JSON | CSV (as of 03/15/2019)
Login | Need an account?

Mooly Sagiv on Formally Verifying Smart Contracts

Setup Time:
30 minutes
Sunday, March 25, 2018 at 06:00pm
Sunday, March 25, 2018 at 09:00pm
Teardown Time:
15 minutes
Estimated size:
Large Event Room

We're pleased to have Professor Mooly Sagiv [1] from Tel Aviv University and the Vmware Research Group speak to us on formal verification of smart contracts. We will begin the event with a short talk from Eric McCarthy [2] of the Kestrel Institute on how ACL2 [3] could be used to verify the EVM.

Mooly's abstract: "Smart contracts define transactions to be executed on top of Blockchain technology. The combination of a decentralized secure computation platform provided by blockchains, and the rich expressiveness of smart contracts, allows us to automate and secure processes which today are manual, slow, inefficient and prone to forgery. However, smart contracts are vulnerable to software errors which are exploited, e.g., for money thefts. In the last 18 months, there were 3 high-impact (over $500M) incidents caused directly by buggy smart contracts that were either exploited maliciously or mistakenly compromised."

"I will present a high level overview of two techniques which can be used for early detection of contract vulnerabilities and preventing them by combining compile-time and run-time techniques: deductive verification and runtime checking."

Mooly is co-author on the work that Yan Michalevsky presented to us recently [4].

[1] http://www.cs.tau.ac.il/~msagiv/
[2] http://www.kestrel.edu/home/people/mccarthy/
[3] http://www.cs.utexas.edu/users/moore/acl2/
[4] https://www.youtube.com/watch?v=Ru6X043Q63U


Member RSVP

Hacker Dojo members may login to reserve space in the event room up to 48 hours before the event.

Member RSVP does not imply event registration if applicable.