SHF: Small: Control-Flow and Data-Flow Analysis of Android Software: Foundations and Applications

SHF：小：Android 软件的控制流和数据流分析：基础和应用

• 批准号: 1526459
• 负责人: Atanas Rountev
• 金额: $ 47.02万
• 依托单位: Ohio State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1526459&HistoricalAwards=false
• 关键词: SHF; Small; Control; Flow; Data

In recent years the growth in the number of computing devices has been driven primarily by smartphones and tablets. For such devices, Android is the dominant platform. The correctness, security, and performance of Android devices is of paramount importance for many millions of users. However, the scientific foundations for software analysis, verification, and transformation in this area are still very inadequate. The proposed work will significantly advance the state of the art in software analysis for Android. The results will be made available to other researchers, which will help design new analyses to improve software quality. Integration of research and education will develop the expertise of new developers of mobile software. Recruitment of underrepresented students will contribute to increased diversity in computing. Through commercial and academic software tools, new software analyses could enter real-world use in the development toolkits of Android programmers, resulting in better software quality and faster time to market.Android applications are framework-based and event-driven. The complex semantics of the framework event/callback model presents a major challenge to static analysis. The project will develop a precise semantic description that captures essential abstraction of the run-time execution model, including modeling of components, their interactions through calls and callbacks, and their handling of external events. Based on this semantics, the project will design a general program representation of application control flow and data flow, and will develop algorithms for constructing and traversing it. The resulting representation and algorithms can serve as basis for a wide variety of static analyses. Three exemplar client analyses will be designed and evaluated: (1) detection of resource leaks, (2) detection of energy-related defects, and (3) taint analysis. These analyses target important quality problems and can help improve the performance and security of Android software. A suite of public algorithm implementations and experimental subjects will be made publicly available, to enable development and evaluation of existing and new static analyses for Android.

近年来，计算设备数量的增长主要是由智能手机和平板电脑推动的。对于这类设备，Android是占主导地位的平台。Android设备的正确性、安全性和性能对数百万用户至关重要。然而，这方面的软件分析、验证和转换的科学基础仍然很不足。这项拟议的工作将极大地提高Android软件分析的水平。结果将提供给其他研究人员，这将有助于设计新的分析来提高软件质量。研究和教育的结合将培养新的移动软件开发人员的专业知识。招收代表性不足的学生将有助于增加计算的多样性。通过商业和学术软件工具，新的软件分析可以进入Android程序员的开发工具包的实际使用，从而带来更好的软件质量和更快的上市时间。Android应用程序是基于框架和事件驱动的。框架事件/回调模型的复杂语义对静态分析提出了重大挑战。该项目将开发准确的语义描述，以捕获运行时执行模型的基本抽象，包括组件的建模、它们通过调用和回调进行的交互，以及它们对外部事件的处理。基于这种语义，该项目将设计应用程序控制流和数据流的通用程序表示，并开发构造和遍历它的算法。由此产生的表示和算法可以作为各种静态分析的基础。将设计和评估三个样本客户分析：(1)检测资源泄漏，(2)检测与能源相关的缺陷，以及(3)污点分析。这些分析针对重要的质量问题，有助于提高Android软件的性能和安全性。一套公开的算法实现和实验对象将公开可用，以便对现有的和新的Android静态分析进行开发和评估。