SHF: Medium: Optimistic Static Analysis

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

Programs running on computers have become essential to today's society. They enable commerce, operate machinery, control transportation, enhance social interaction, and perform innumerable other important tasks. This research project examines how to ensure that programs run correctly and securely as they carry out their mission by monitoring their execution efficiently. The intellectual merits are developing a new way to monitor programs as they execute, which incurs far less overhead than prior methods. The project's broader significance and importance are in helping programs programs run more correctly and securely as they perform essential functions in society. Static program analysis is a powerful technique for understanding, verifying, optimizing, and transforming programs. Unfortunately, usefulness of those static analyses is greatly hindered by the need to prove their soundness, as soundness requires analysis of all possible executions and sound over-approximations of a program. This research is designing and using optimistic static analyses. They make optimistic assumptions about a program, and are sound only when those assumptions hold true in an execution. The optimistic assumptions, called likely variants, are typically learnt by observing a representative set of executions. At runtime, these assumptions are checked, and if they fail, remedial actions are taken. As optimistic static analysis can prune a large fraction of the state space from consideration, its scalability and precision can be one to two orders of magnitude higher than conventional sound analysis. This project is exploring several applications of optimistic static analysis ranging from security to concurrency to hardware synthesis.