Abstract: Software architecture modeling is important for analyzing system quality attributes, particularly security. However, such analyses often assume that the architecture is completely known in advance. In many modern domains, especially those that use plugin-based frameworks, it is not possible to have such a complete model because the software system continuously changes. The Android mobile operating system is one such framework, where users can install and uninstall apps at run time. We need ways to model and analyze such architectures that strike a balance between supporting the dynamism of the underlying platforms and enabling analysis, particularly throughout a system�s lifetime. In this paper, we describe a formal architecture style that captures the modifiable architectures of Android systems, and that supports security analysis as a system evolves. We illustrate the use of the style with two security analyses: a predicatebased approach defined over architectural structure that can detect some common security vulnerabilities, and inter-app permission leakage determined by model checking. We also show how the evolving architecture of an Android device can be obtained by analysis of the apps on a device, and provide some performance evaluation that indicates that the architecture can be amenable for use throughout the system�s lifetime.

Abstract: Successful attacks are nearly inevitable as sophisticated threat actors are committed to inflicting damage, leaving digital and physical destruction in their wakes. As defenders recognize the inevitability of successful attacks, they must change their defense paradigms from only preventing attacks to also weathering the attacks that penetrate first-line defenses. Instead, the systems' abilities to provide functionality should be minimally disrupted while simultaneously containing an attacker. The engineering challenge is to build and operate systems that are resilient to attack, able to adapt to trade off some functionality to preserve trust in more-critical functionality. We refer to this concept as graceful degradation. Defenders would be in a far better position to address the increasingly dire situation confronting them if they had a method and tool to support graceful degradation. However, this requires the ability to reason despite uncertainties at architecture and design time and at run time. Automation can be supported by formal modeling of systems, but it must not be labor-intensive. We propose and develop an approach that directly addresses these challenges. We can architect and operate systems that are better able to weather attacks by automating the evaluation of systems' security properties to enable effective automated graceful degradation of systems in the presence of uncertainty through an approach of formally modeling systems and system behavior at an architectural level of abstraction to explore hypothetical attacks and the systems' abilities to respond. We describe our approach and provide tooling to demonstrate our concept.