static analysis

Provably Sound Static Analysis for Ethereum Smart Contracts

Smart contracts are distributed applications, which govern financial assets in cryptocurrencies such as Ethereum and, hence, can implement advanced financial instruments, such as decentralized exchanges or autonomous organizations (DAOs). In this talk, I will overview our advances in developing static analyzers that come with provable guarantees. I will first show how to define generic security properties that characterize the absence of prominent attack classes (such as reentrancy or transaction order dependence) and then discuss different forms of static analysis that can prove these properties and that can be efficiently implemented to analyze real-world smart contracts.

TypeScript Analysis in Prime Video

TypeScript is a typed version of JavaScript widely used across Amazon, but poses challenges for static analysis: The language supports many intricate features used in practice, such as callbacks and higher-order functions, dynamic field access, and asynchronous code. At the same time, the size of industrial code bases such as the Prime Video application makes a highly precise whole-program analysis intractable. In this talk, we present how we approach this trade-off in Prime Video with a lightweight whole-program analysis followed by a more precise goal-directed analysis of potential bug locations. Our goal-directed analysis uses an imprecise call graph and points-to information generated upfront to guide a more expensive goal-directed analysis that attempts to prove that potential bugs cannot happen via abstract interpretation backed by an SMT solver.