OOCFA2: a PDA-based higher-order flow analysis for object-oriented programs
Marquez, Nicholas Alexander
MetadataShow full item record
The application of higher-order PDA-based flow analyses to object-oriented languages enables comprehensive and precise characterization of program behavior, while retaining practicality with efficiency. We implement one such flow analysis which we've named OOCFA2. While over the years many advancements in flow analysis have been made, they have almost exclusively been with respect to functional languages, often modeled with the calculus. Object-oriented semantics--while also able to be modeled in a functional setting--provide certain structural guarantees and common idioms which we believe are valuable to reason over in a first-class manner. By tailoring modern, advanced flow analyses to object-oriented semantics, we believe it is possible to achieve greater precision and efficiency than could be had using a functional modeling. This, in turn, reflects upon the possible classes of higher-level analyses using the underlying flow analysis: the more powerful, efficient, and flexible the flow analysis, the more classes of higher-level analyses--e.g., security analyses--can be practically expressed. The growing trend is that smartphone and mobile-device (e.g., tablet) users are integrating these devices into their lives, in more frequent and more personal ways. Accordingly, the primary application and proof-of-concept for this work is the analysis of the Android operating system's permissions-based security system vis--vis potentially malicious applications. It is implemented atop OOCFA2. The use of a such a powerful higher-order flow analysis allows one to apply its knowledge to create a wide variety of powerful and practical security-analysis "front-ends"--not only the permissions-checking analysis in this work, but also, e.g., information-flow analyses. OOCFA2 is the first PDA-based higher-order flow analysis in an object-oriented setting. We empirically evaluate its accuracy and performance to prove its practical viability. We also evaluate the proof-of-concept security analysis' accuracy as directly related to OOCFA2; this shows promising results for the potential of building security-oriented "front-ends" atop OOCFA2.