CAREER: Adaptive Large-Scale Program Analysis

点击翻译按钮获取中文摘要

Automated program analyses developed over the last three decades have demonstrated the ability to prove non-trivial properties of real-world programs. This ability, in turn, has applications to emerging software challenges in security, software-defined networking, cyber-physical systems, and beyond. The diversity of such applications necessitates adapting the underlying program analyses to client needs, in aspects of scalability, applicability, and accuracy. Today's program analyses, however, do not provide useful tuning knobs. The goal of this research is a general computer-assisted approach to effectively adapt program analyses to diverse clients. It bridges the gap between decades of program analysis research on one hand and diverse artifacts built atop them to address emerging software challenges on the other. In doing so, it broadens and enhances the benefits of program analysis to its users, as well as users of software whose quality is impacted by program analysis.The research has three key ingredients. First, it poses optimization problems that expose a large set of choices to adapt various aspects of a program analysis, such as its cost, the accuracy of its result, and the assumptions it makes about missing information. Second, it solves those optimization problems by new search algorithms that efficiently navigate large search spaces, reason in the presence of noise, interact with users, and learn across programs. Third, it builds a program analysis platform that facilitates users to specify and compose analyses, enables search algorithms to reason about analyses, and allows using large-scale computing resources to parallelize analyses. The approach is demonstrated in the context of analyzing mobile apps -- programs that run on advanced mobile devices such as smartphones and tablets. Mobile apps represent an increasing use of non-expert programmers and they are likely to be used across a wide range of users in heterogeneous and demanding conditions that can benefit from what-if analyses that program analysis can offer.