Security Vulnerabilities in Smart Contracts as Specifications in Linear Temporal Logic

Ethereum is a distributed computer with a native cryptocurrency. Like other monetary transaction based systems, a problem this platform faces is accounts and transactions being susceptible to theft and other hacks. Smart contracts (programs which run on this blockchain) can store money and initiate financial transactions. They need to be carefully studied to safeguard against threats. This is especially true before deployment, as they become immutable after. Software analysis and verification techniques are applied to study security vulnerabilities in smart contracts. Currently, there are over 35 tools that do so. Many of them directly study contracts written in high level languages such as Solidity. In this work, we similarly study contracts, but at the lower bytecode level. We focus on different classes of smart contract vulnerabilities– access control, bad randomness, denial of service, front running, integer overflow/underflow, re-entrancy, short address, time manipulation, and unchecked low-level calls. We create specifications based on linear temporal logic to describe vulnerabilities in each of these categories, and we test them against real-world contracts