SHF: Medium: Optimistic Static Analysis

在计算机上运行的程序已成为当今社会必不可少的。他们使商业，操作机械，控制交通，加强社会互动，并执行无数其他重要任务。本研究项目探讨如何通过有效地监控程序的执行来确保程序在执行其使命时正确安全地运行。其智力优势是开发了一种新的方法来监视程序的执行，这比以前的方法产生的开销要少得多。该项目的更广泛的意义和重要性在于帮助程序更正确和安全地运行，因为它们在社会中执行基本功能。静态程序分析是理解，验证，优化和转换程序的强大技术。不幸的是，这些静态分析的有用性被证明其合理性的需要大大阻碍，因为合理性需要分析所有可能的执行和程序的合理过度近似。本研究设计并使用乐观静态分析。它们对程序做出乐观的假设，并且只有当这些假设在执行中成立时才是合理的。乐观的假设，称为可能的变量，通常通过观察一组有代表性的执行来学习。在运行时，检查这些假设，如果它们失败，则采取补救措施。由于乐观静态分析可以从考虑中修剪状态空间的大部分，因此其可扩展性和精度可以比传统声音分析高一到两个数量级。这个项目正在探索乐观静态分析的几个应用，从安全到并发到硬件综合。

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.