Low-level bytecode programs are difficult to handle by formal reasoning, particularly in the case of sound and precise reasoning about memory operations. There is often no distinguished allocation operation: high-level object allocations are affected via pointer arithmetic. Type information is lost in the compilation: the abstraction of memory is simply an unstructured array of bytes. To recover high-level information, a sound pointer analysis is an invaluable resource. Such an analysis enables optimizations and elucidates program behavior that would otherwise be obscured in a low-level setting. This talk describes a new static analysis algorithm we have developed for sound pointer analysis for low-level bytecode. We make this broad problem tractable by first restricting our focus to bytecode programs that manage memory via a bump allocator that operates on a distinguished free pointer. In other words, we target bytecode programs where memory is divided into disjoint regions, each of which corresponds to an “object”. Our analysis algorithm uses a novel technique for mapping updates of a distinguished free pointer to provably non-aliased abstract addresses, which enables standard pointer analysis techniques. Our static pointer analysis uses a “trust but verify” approach: we build our analysis on the expectation that the compiler has properly managed memory via the free pointer/bump allocator, but at each step, we verify that regions of memory allocated via the bump allocator are properly disjoint, i.e., every read/write of memory provably accesses only one, distinct region. This talk discusses our practical experience using this analysis in verifying smart contracts that run on the Ethereum Virtual Machine. In particular, we outline multiple high-profile memory management bugs uncovered by our analysis, and the downstream optimizations and precision improvements unlocked by our pointer analysis results.

My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable. I am interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive process, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic. I am applying these techniques to verify safety of liveness of distributed systems.