Managing Risk in Mobile Applications With Formal Security Policies

Abstract

Department of Defense (DoD) acquisition requires information technology (IT) to undergo the DoD information assurance certification and accreditation process (DIACAP), which makes strong architecture-dependent assumptions. Emerging IT architectures, such as mobile computing platforms, invalidate these assumptions and prevent the DoD from acquiring commercial technologies that are readily available to adversaries. To address this problem, we introduce a preliminary framework in which an application profile is expressed in a formal language and scaled with evolving architectural assumptions. This profile aims to incorporate information assurance (IA) requirements that are commensurate with risk and scalable based on an application's changing external dependencies. Information assurance risk levels that account for changing user identities and IA parameters (confidentiality, integrity, and availability) will result from dynamic recombination of mobile applications during runtime. The language is expressed in first-order logic and includes an evolvable lexicon to describe changing system configurations. We envision that software developers and certification authorities can use these formal profiles with an inference engine to complete the DIACAP and maintain compliance as IT systems evolve over time. The framework has been evaluated using existing DoD acquisition and DIACAP policy and a case study in a popular mobile application ecosystem.