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.