Visible to the public Science of Secure Frameworks (CMU/Wayne State University/George Mason University Collaborative Proposal) - October 2016Conflict Detection Enabled

Submitted by Jamie Presken on Thu, 09/15/2016 - 8:05am

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 (University of California, Irvine), Joshua Sunshine (CMU), Bradley Schmerl (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 and Sam Malek. "Titanium: Efficient Analysis of Evolving Alloy Specifications." 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016), Seattle, WA, November 2016.

  • Bradley Schmerl, Jeffrey Gennari, Alireza Sadeghi, Hamid Bagheri, Sam Malek, Javier Camara and David Garlan. Architecture Modeling and Analysis ofSecurity in Android Systems. In Proceedings of the 10th European Conference on Software Architecture (ECSA 2016), Vol. 9839 of Lecture Notes in Computer Science, Springer, Copenhagen, Denmark, 30 November - 2 December 2016.

3) KEY HIGHLIGHTS

Due to the guarantees that they afford, formal approaches for assessing the security properties of software systems are highly desired. An example of a formal specification and analysis technique that has shown to be quite useful in security analysis of software is Alloy. However, analyzing Alloy specifications with the help of a constraint solver is known to be extremely expensive. Thus, its applications at runtime and during the evolution of a software system for evaluating its changing security properties has been limited. We have developed a new method of analyzing Alloy specifications that is substantially faster than all prior techniques for repeated analysis of an evolving specification. The tool realizing this approach is called Titanium (see paper above). It provides a systematic method of reusing solutions calculated in previous analyses of an Alloy specification, thereby drastically improving the time and resources required to analyze evolving Alloy specifications. We are now exploring ways in which Titanium can be used at runtime for evaluating security properties of software. As a first step in this direction, we are experimenting with applications of Titanium to evaluate security properties of changing configuration of Android apps installed on a mobile device.

Enhanced a semi-automated algorithm and tool 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.

Groups: