SoS Quarterly Summary Report - CMU - January 2015
Lablet Summary Report
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.
A). Fundamental Research
Epistemic models for security [Harper, project 5]. The techniques described in previous quarterly reports have now been extended to support concurrent communicating processes. The techniques are based in epistemic logic, which provides a way to reason rigorously about knowledge and belief. The extension to concurrency enables reasoning about familiar systems such as web browsers. Concurrency adds significant complications, for example, due to timing-channel leaks.
This work supports progress in HP 1: Scalability and Composability. By framing the epistemic reasoning in a type-theoretic structure, it becomes possible to reason in a compositional way. Results include, for example, a proof that for a well-typed program, a low-security principal can learn a high-security secret only if it is explicitly authorized to do so by an integrated authorization logic.
Race Vulnerability Study and Hybrid Race Detection [Aldrich, project 8]. To better support the scientific process, two key steps were initiated this past quarter. (1) Development of RaceGarage, which is a corpus of applications with reproducible race vulnerabilities. (2) An initial set of interviews of experienced software engineers regarding their use of immutability. The purpose is to gain insight into the relationship among programmer needs, programming language features, and race vulnerabilities enhancing security metrics research by providing another dimension of security assessment criteria.
This work supports progress in HP 1: Scalability and Composability and HP 3: Metrics. Existing race detectors tend to produce excessive false positives or to be computationally expensive. The intent here, through composable techniques, is to gain both precision and efficiency. The metrics focus enables understanding of the root causes of races and associated vulnerabilities.
USE: User Security Behavior [Acquisti, Cranor, Christin, Telang, project 10]. After many months of preparation, including the developing of monitoring instruments, servers, and data management capabilities, the study has been launched. The initial cohort of 50 participants will expand over time. A wide range of data is being collected including client machines' processes, file-system meta-data (e.g., file path, file size, date created, date modified, permissions), network packet headers, Windows security logs, Windows updates, installed software, web browsing settings and behavior, and wireless access points.
This work supports progress in HP 5: Human Behavior and HP 3: Metrics. The Security Behavior Observatory collects data directly from people's own personal computers, thereby capturing the actuality of computing-related behavior "in the wild." This data is expected to be the closest to the ground truth of the users' everyday security and privacy challenges that the research community has ever collected, with the intent that the insights can influence research domains including behavioral sciences, computer security & privacy, economics, and human-computer interaction. The metrics work has two aspects. First, it enables evaluation of established metrics for measuring their user-reported security behaviors by comparing them to users' actual computing behavior, and second, it will support new predictive metrics on user behavior with the respect to computer security and privacy founded on highly ecologically-valid data analyses.
There are certain identified risks associated with this project, including the recruitment of participants, overcoming anti-virus response to the data collector probes, performance impacts on users, and adaptation to the variety and peculiarities of desktop configurations. The team is working to address these challenges.
Geo-Temporal Characterization of Security Threats [Carley, project 11]. This project makes use of data from Symantec. The data has supported development of a model of global cyber-attacks, with results demonstrating that the global cyber-security landscape is, in fact, not dominated by the US, Russia and China, but instead depends on the sophistication of the IT infrastructure in many developing nations. Initial examination of malware attacks reveals that, in general, developing countries are more impacted by newer malware than are more developed countries; however, the results depend on the type of malware. For example, compared to most countries (including Russia and China), the US is impacted by older viruses, and newer trojans and worms.
This work supports progress in HP 5: Human Behavior, with focus on network analysis.
B). Community Interaction
[Platzer, project 3].
CPS V&V Grand Prix competition for the Foundations of Cyber-Physical Systems course, December 10, 2014, Carnegie Mellon University (http://symbolaris.com/course/fcps14-competition.html).
Students presented their final projects to a panel of experts in CPS, who will give them feedback from an industry perspective and insights into the state-of-the-art verification & validation methods used for CPS as well as award prizes (http://www.cs.cmu.edu/~aplatzer/course/fcps14-competition.html).
CPS V&V Workshop, December 11 and 12th, 2014, Carnegie Mellon University (http://www.ls.cs.cmu.edu/CPSVVIF/index.html).
C. Educational
[Garlan, projects 1 and 7].
Course 17-707. Self-Adaptive Systems, taught by David Garlan and Bradley Schmerl.
An increasingly important requirement for software-based systems is the ability to adapt at run time to handle such things as resource variability, changing user needs, and system faults. In this graduate seminar we will examine past and current research into self-adaptation in software systems, including planning, control systems, programming language design for adaptation, software architecture, fault-tolerant computing, and machine learning.
Topics to be covered include the rationale for self-adaptation in software systems; case studies of systems that have done a good job at handling; self-adaptation; adaptation research in selected areas including autonomic computing; cloud computing, automated planning, machine learning, software architecture, control systems, multi-fidelity computation; biologically-inspired models of computation, graceful degradation, mixed initiative systems, self-securing systems.
- Approved by NSA
- Scalability and Composability
- Policy-Governed Secure Collaboration
- Metrics
- Resilient Architectures
- Human Behavior
- CMU
- A Language and Framework for Development of Secure Mobile Applications
- Epistemic Models for Security
- Geo-Temporal Characterization of Security Threats
- Highly Configurable Systems
- Multi-Model Run-Time Security Analysis
- Race Vulnerability Study and Hybrid Race Detection
- Science of Secure Frameworks
- Secure Composition of Systems and Policies
- Security Reasoning for Distributed Systems with Uncertainty
- Usable Formal Methods for the Design and Composition of Security and Privacy Policies
- USE: User Security Behavior
- FY14-18
- Jan'15