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 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.