Smart contracts manage sizable assets on a blockchain, so their security is paramount. In the past years, many approaches have been developed to find low-level vulnerabilities at code level or general types of vulnerabilities through static and dynamic analysis. Now, more and more exploits address flaws in a contract’s internal logic. This raises the issue: How can we capture application-specific properties and verify them?
We present dynamic condition response (DCR) graphs as an engineering-friendly way to capture key features of a smart contract’s business logic. DCR graphs provide a graphical notation for a formal, machine-readable specification of business logic. Combined with a tool that monitors transactions on a blockchain against the specification, we can successfully detect potential exploits in tests of exploits against vulnerable contracts.
