Science of Secure Frameworks (CMU/Wayne State University/George Mason University Collaborative Proposal) - January 2015

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): David Garlan (CMU), Jonathan Aldrich (CMU)
Researchers: Marwan Abi Antoun (Wayne State University), Sam Malek (George Mason University), Joshua Sunshine (CMU), Bradley Schmerly (CMU)

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
This refers to Hard Problems, released November 2012.

By leveraging approaches to software architecture we will be able to better understand the security implications of frameworks used to build many of today's mobile software systems. This will allow us and provide tools and techniques for building more scalable and composable frameworks that have security assurances that can be verified statically, can be used for building self-securing resllient systems, and that ultimately reduce security vulnerabilities in frameworks and applications based on them in practice.

2) PUBLICATIONS

Riyadh Mahmood, Nariman Mirzaei, and Sam Malek. EvoDroid: Segmented Evolutionary Testing of Android Apps. Published in proceedings of the 22th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2014), Hong Kong, November 2014.

Khalaj, E., Wang, Y., Giang, A., Abi-Antoun, M., and Rajlich, V. Impact Analysis based on a Global Hierarchical Object Graph. In 22nd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER), 2015. Montreal, Canada. To appear. 10 pp.

3) KEY HIGHLIGHTS

The two tools produced by subcontractors (Scoria and COVERT) could be used by other projects that are interested in analyzing security properties of Android systems.

COVERT has been evaluated on more the 200 real-world Android apps, uncovering vulnerabilities in (many of which were unknown) in some popular apps.

Performed an empirical study of benign open source Java applications and frameworks and established that the way they interact with the Java security manager differs from malicious applications. This has resulted in the development of run time monitors to prevent security manager modification and privilege escalation.

Investigated how an abstract object graph extracted using abstract interpretation can be used to derive more precise dependencies during impact analysis during general code modification tasks, or when fixing security vulnerabilities that are found. By mining and ranking the dependencies based on the object graph, we were able to double the effectiveness compared to an existing approach based on visiting the abstract syntax tree.

Completed an initial inference algorithm for iteratively and interactively refining a global hierarchical graph while maintaining its soundness, thus tackling the scalability hard problem associated with using such an approach.