Hyperproperties [Clarkson and Schneider 2010] can express security policies, such as secure information flow and service level agreements, which the standard kinds of trace properties used in program verification cannot.
Our objective is to develop verification methodologies for hyperproperties.
We intend to apply those methodologies to the construction of secure systems from components with known security properties, thereby addressing the problem of compositional security.
The 19th European Symposium on Research in Computer Security will be held in Wroclaw, Poland, at the Institute of Mathematics and Computer Science Wroclaw University of Technology, on September 7-11, 2014. ESORICS is the premier European research conference in computer security. ESORICS started in 1990 and has been held in several European countries, attracting an international audience from both the academic and industrial communities.
In highly configurable systems the configuration space is too big for (re-)certifying every configuration in isolation. In this project, we combine software analysis with network analysis to detect which configuration options interact and which have local effects. Instead of analyzing a system as Linux and SELinux for every combination of configuration settings one by one (>10^2000 even considering compile-time configurations only), we analyze the effect of each configuration option once for the entire configuration space. The analysis will guide us to designs separating interacting configuration options in a core system and isolating orthogonal and less trusted configuration options from this core.
Scalability and composability: Isolating conguration options or controlling their interactions will lead us toward composable analysis with regard to conguration options.
Predictive security metrics: To what degree can conguration-related indicate implementations that are more prone to vulnerabilities or in which vulnerabilities have more severe consequences?
We complement the Science of Security endeavor with a focus on the often overlooked problems of configuration options in systems. Whereas current approaches work on specific snapshots and require expensive recertification, our approaches extend underlying mathematical models (data-dependence graphs) with configuration knowledge and will thus scale analyses and reduce the need for repeating analyses. Furthermore, we expect that configuration complexity and configuration-specific program-dependence is a suitable empirical predictor for the likelihood and severity of vulnerabilities in complex systems. Finally, technical and empirical results of our work will also bring new approaches to the field of social network analysis that can be very powerful and applicable for Science of Security far beyond the scope of the current Lablet.
1. Kaestner, Christian & Pfeffer, Juergen (2014). Limiting Recertification in Highly Configurable Systems. Analyzing Interactions and Isolation among Configuration Options. HotSoS 2014: 2014 Symposium and Bootcamp on the Science of Security, April 8-9, Raleigh, NC.
Our research focuses on creating the scientific foundations to support model-based run-time diagnosis and repair of security attacks. Specifically, our research develops models that (a) scale gracefully with the size of system and have appropriate real-time characteristics for run-time use, and (b) support composition through multi-model analysis. Network models will complement architectural models in two ways: (a) to characterize the organizational context of a system, and (b) to detect anomalies through network representations of architectural behavior. The former can be particularly effective, for example, in detecting and preventing insider attacks, which are often linked to organizational issues. The latter will lead to the creation of a new set of architectural metrics (e.g., based on network measures) to rapidly detect anomalous behaviors.
PI: Juergen Pfeffer
Co-PIs: David Garlan, Bradley Schmerl
We address composability through multiple semantic models (here, architectural, organizational, and behavioral), which provide separation of concerns, while supporting synergistic benefits through integrated analyses. Our work is related to the thrust of resilience, through the use of adaptive models that can be used at run-time to predict, detect and repair security attacks. Finally, our work also bears on the topic of security metrics, since we will be adapting social network-based metrics to the problem of architecture-level anomaly detection.
Noninterference defines a program to be secure if changes to high-security inputs cannot alter low-security outputs thereby indirectly stating the epistemic property that no low-security principal acquires knowledge of high-security data. We consider a directly epistemic account of information-flow control focusing on the knowledge flows engendered by the program's execution. Storage effects are of primary interest, since principals acquire and disclose knowledge from the execution only through these effects. The information-flow properties of the individual effectful actions are characterized using a substructural epistemic logic that accounts for the knowledge transferred through their execution. We prove that a low-security principal never acquires knowledge of a high-security input by executing a well-typed program. Moreover, the epistemic approach facilitates going beyond noninterference to account for authorized declassification. We prove that a low-security principal acquires knowledge of a high-security input only if there is an authorization proof.
PI: Robert Harper