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.
SHF: Small: Control-Flow and Data-Flow Analysis of Android Software: Foundations and Applications