Vijay
Ganesh,
Department
of
Electrical
and
Computer
Engineering
University
of
Waterloo
Smart contracts represent one of the most interesting developments in the context of blockchains in recent years. Unfortunately, smart contracts remain vulnerable to various security attacks. Serious attacks have been witnessed in the past several years like the DAO attack and the Parity Wallet Hack, which resulted in a $60 million and $30 million Ether theft respectively. A systematic and scalable security analysis tool for smart contracts is essential, if they are to become viable in the long run.
In my talk, I will focus on one promising way to address the security issues facing smart contracts via the use of SAT/SMT solver and symbolic execution. The key insight behind symbolic analysis is that one can detect security vulnerabilities by reducing potentially vulnerable program paths to logic formulas, and then deploying logic solvers to expose these vulnerabilities. I will focus on the technical challenges we have addressed to make solvers efficient for symbolic execution.
Bio: Dr. Vijay Ganesh is an associate professor at the University of Waterloo. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his PhD in computer science from Stanford University in 2007.
Vijay's primary area of research is the theory and practice of automated mathematical reasoning algorithms aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3 string, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of the satisfiability problem for various mathematical theories.
He has won over 25 awards, honors, and medals to-date for his research, including an ACM Impact Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, an Ontario Early Researcher Award 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper citation at DATE 2008.