IBM Research Staff Member
India Research Laboratory IBM
New Delhi, India
Mohan is a Researcher Staff Member with IBM Research, India. He is broadly interested in Systems, Security and Program Analysis, with a current focus on Blockchain. Mohan has published several papers in high impact conferences. He earned his PhD in Computer Science from Rutgers University in 2013.
Analyzing Safety of Smart Contracts using Zeus : A smart contract is hard to patch for bugs once it is deployed, irrespective of the money it holds. A recent bug caused losses worth around $50 million of cryptocurrency. We present Zeus---a sound fault detection framework to verify smart contracts. Zeus leverages both abstract interpretation and symbolic model checking, along with the power of constrained horn clauses to quickly verify contracts for safety. We have built a prototype of Zeus for Ethereum and Fabric blockchain platforms, and evaluated it with over 22.4K smart contracts. Our evaluation indicates that about 94.6% of contracts (containing cryptocurrency worth more than $0.5 billion) are vulnerable. Zeus is sound with zero false negatives and has a low false positive rate, with an order of magnitude improvement in analysis time as compared to prior art.