Dear all,
It's my great pleasure to announce a very interesting presentation from two researchers of the ETH Zurich, in a field where progress is dearly needed: Automated Formal Verification of Smart Contracts.
Permissionless blockchains such as Bitcoin and Ethereum have allowed for mutually mistrusting entities to trade and interact, without relying on a trusted third party. Beyond the simple transfer of funds, Turing-complete smart contracts permit the execution of arbitrary code on top of the blockchain. Smart contracts are praised for simplifying many real-world processes due to the ability of being enforced autonomously.
Despite their potential, repeated security concerns have shaken the trust in handling billions of USD in decentralized smart contracts. It has become apparent that writing secure smart contracts is a significant challenge.
Reliable tools are therefore required to guide developers in writing secure contracts as well as to enable contract users to verify the contracts they interact with.
In their talk, Petar Tsankov and Arthur Gervais will present Securify (ww.securify.ch), the first smart contract checker that provides:
(i) strong security guarantees
(ii) fully automated analysis, and is
(iii) easily extensible to capture new security vulnerabilities.
Securify is capable to verify all execution paths in a given contract, and therefore provides maximum cover. Indeed, Securify discovers security issues in 38% of the smart contracts published on the Ethereum blockchain. For each vulnerable contract, Securify is capable to pinpoint the instructions that may cause security issues and therefore
provides practical and useful guidelines to contract developers. Securify is also easily extensible, allowing to capture new security vulnerabilities as soon as they are discovered.
