Science of Secure Frameworks (CMU/Wayne State University/George Mason University Collaborative Proposal) - April 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
Hamid Bagheri, Alireza Sadeghi, Joshua Garcia, and Sam Malek. COVERT: Compositional Analysis of Android Inter-App Security Vulnerabilities. Accepted to appear in the IEEE Transactions on Software Engineering.
Alireza Sadeghi, Hamid Bagheri, and Sam Malek. Analysis of Android Inter-App Security Vulnerabilities Using COVERT. Accepted to appear at the International Conference on Software Engineering, Tool Demo Track, Florence, Italy, May 2015.
Bradley Schmerl, Jeff Gennari, David Garlan. An Architecture Style for Android Security Analysis (Poster). 2015 Symposium and Bootcamp on the Science of Security (HotSoS), Urbana IL, April 21-22, 2015.
3) KEY HIGHLIGHTS
We have transitioned the first draft of an Android architectural style focused on capturing and analyzing security properties (both statically and dynamically) to GMU. We are working with them to integrate our two approaches to have a standard model for information from static analysis of Android systems and run-time monitoring and mitigation.
Completed an initial implementation including the user interface and small-scale evaluation of an inference algorithm for iteratively and interactively refining a global hierarchical graph while maintaining its soundness, thus tackling the scalability hard problem associated with using the Scoria approach.
Completed a data-driven approach that uses code patterns identified by visitors and metrics to identify systems where the abstract runtime structure is significantly different from the code structure, thus making more complex reasoning about runtime properties such as security.