SaTC: CORE: Medium: Bedrock: Security for Smart Contracts

Over the last several years, blockchain technology and Web3 applications and protocols have experienced explosive growth and generated significant monetary value. In 2024, the total market cap of cryptocurrencies has exceeded two trillion US dollars, and there are millions of applications (smart contracts) deployed on blockchains, providing an ecosystem of financial and other services. Unfortunately, attackers have taken notice of vulnerabilities in the Web3 ecosystem and found opportunities to steal money and defraud victims. This project will develop novel techniques and better systems to identify vulnerable applications and detect malicious attacks, with the goal of protecting the millions of users who interact with and invest in Web3 applications, as well as thwarting the opportunities of adversaries to use illicitly gained funds for nefarious purposes. This research effort will also train graduate and undergraduate students in the techniques and approaches necessary to secure the financial infrastructure and introduce new educational tools, such as blockchain-focused courses and capture-the-flag security competitions. This project introduces a novel approach, called Bedrock, to identify high-level, semantic vulnerabilities in Web3 applications through a multi-layer framework. This framework starts from the low-level bytecode of smart contracts, captures and reasons about the behavior of multiple interacting smart contracts, and takes into account their financial context. The Bedrock framework will introduce novel ideas at each of its abstraction layers. First, it introduces a multi-chain program analysis platform that directly operates on low-level smart contract bytecode. This platform allows for the re-use of analyses in different blockchain environments as well as the unified modeling of multi-chain applications, such as bridges. Second, the framework introduces novel analyses and techniques that identify higher-level, logic flaws in smart contracts. Third, Bedrock automatically extracts high-level models of complex DeFi (decentralized finance) applications. These models provide the context for the evaluation of the impact of the logic flaws identified by the security analysis. This will allow for the accurate and scalable detection of flaws in smart contracts and the financial protocols that they implement. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.