A new academic research institute to improve understanding of the science behind the growing Cyber Security threat was announced today by the government. The Institute, which opens on 1 October, will be hosted at UCL and led by Professor Angela Sasse (UCL Computer Science).
Abstract
The U.S. Institute of Medicine commissioned my 2011 report on the role of trustworthy software in the context of the "510(k)" U.S. medical device regulations. This talk will provide a glimpse into the risks, benefits, and regulatory issues for medical device cybersecurity and innovation of trustworthy medical device software.
Making sound security decisions when designing, operating, and maintaining a complex enterprise-scope system is a challenging task. Quantitative security metrics have the potential to provide valuable insight on system security and to aid in security decisions. To produce model-based quantitative security metrics, we developed the ADversary VIew Security Evaluation (ADVISE) method and implemented it in the prototype tool Möbius-SE (Möbius Security Edition), which is suitable for use by security modeling experts. Our goal in this project is to extend the ADVISE method and tool to explicitly account for the behavior of human users as part of the system. While cyber security models traditionally model the behavior of the attacker, they usually do not explicitly account for the behavior of the users of a system, and how that use can create or eliminate system vulnerabilities.
Increasingly, accumulated cyber security data indicate that system users can play an important role in the creation or elimination of cyber security vulnerabilities. Thus, there is a need for cyber security analysis tools that take into account the actions and decisions of human users.
We are 1) developing a Möbius-SE-compatible, process-oriented modeling formalism for modeling how human users interact with systems, using the concept of a human decision point to explicitly represent decisions that affect the security of a system; 2) implementing the formalism as an atomic model editor in Möbius-SE that generates models that can interact with other Möbius-SE models, e.g., models of the systems itself and the attacker; and 3) demonstrating the use of the implemented tool in a variety of government- and industry-motivated case studies, as suggested by our sponsor and industry partners (HP and GE).
William H. Sanders, David M. Nicol, Jim Blythe (University of Southern California), and Sean W. Smith (Dartmouth College)
This project is developing a common logical framework that will account for two principal sources of trust in software: digital signatures and explicit proof. The framework will allow us to rigorously specify, enforce, and analyze security policies that rely on multiple modes and sources of trust. Based on earlier work by the PI and collaborators, the framework is being cast as a modal type theory that comes equipped with a notation for programs and proofs. We will exploit this relationship to guarantee composability (since types govern interfaces between code) and usability from the programmer's point of view (since type checking is effective during software development). The project will proceed in two phases: framework design and metatheoretic study in the first phase, and a testbed implementation in the second phase. A possible third phase may study usability from the end user's point of view.
Frank Pfenning (CSD, CMU) and Elsa L. Gunter
In this project, we are formulating a formal science of securing packet forwarding in computer networks. In particular, we are developing a formal algebra of the network's data plane (packet-forwarding) operations. Our approach represents the network’s forwarding behavior and state in the form of Boolean satisfiability (SAT) clauses. Our framework enables rigorous analysis and study of the way that networks forward packets, including the ability to check correctness invariants against a specific network deployment (e.g., reachability, service quality, classification level), providing metrics that capture the degree of packet-forwarding security, and enabling the derivation of theorems about how to build networks with strong security properties on packet-forwarding behavior. We are bridging the gap between theory and practice by developing a system to directly read SAT clauses from network deployments and are building upon existing SAT solver technologies to perform automated reasoning. To speed progress, we are building upon our earlier work on using satisfiability checking for testing network reachability.
This project falls within the areas of control theory and game & decision theory, and aims at addressing some foundational issues. It builds on a platform of ongoing research on strategic decision‐making that accommodates elements of security, robustness, learning, and adversarial intrusion, using control‐ and game‐theoretic frameworks.
Starting from the premise that cyber attacks have quantifiable objectives, our long-term goal is to develop computational tools that quickly recover the objective associated with any given attack by observing its effects. Knowledge of this objective is critical to threat assessment. It allows us to understand the scope of an attack, to predict how the attack will proceed, and to respond in a systematic and targeted way. Our approach to recovering this objective is based on a new method for solving the problem of "inverse optimal control." Much of our recent work has focused on establishing the theoretical foundations for this method of solution. In this project we are exploring its application to threat assessment.
The criticality of the information protection and assurance (IPA) problem has understandably sparked rich intellectual and material investment into finding a solution. Several efforts have centered on understanding, identifying, tolerating, and patching security vulnerabilities at different levels of the electronic system stack for various security attack models. Most of these approaches tend to fall into the "sand-boxing" category, whereby unusual events are sequestered until their potential impacts are identified. Such efforts tend to be directed at well-known threats, and thus require that all existing techniques be revisited as newer attack models emerge.
This project is formulating a framework for designing secure computing platforms that treat security infractions as computational errors and employ error-resiliency techniques to tolerate them, while simultaneously providing the user with alert levels based on a grading of the severity of the infractions. Our ongoing work on stochastic computing is being leveraged to provide a foundation for the framework.
In this project, we are using our invariant generation methodologies for security focused applications, like generation of invariants for a new application from the Android app store. We are investigating the science behind re-engineering a system through iterative invariant generation. We are also studying the connections between the machine-learning model used by the data mining and the finite state machine model of the program that is actually learned. We will generalize the models/abstractions obtained from this study and validate these methods of learning invariants using empirical evidence from a real security application.
This project is developing methods for resilient, efficient recognition of distributed attacks on clouds, data warehouses, clusters, and other massively parallel systems. Such attacks cannot usually be detected through local monitoring alone. Specifically, we are developing a probabilistic distributed temporal logic for characterizing such attacks and methods of verifying formulas in such a logic. The novel approach of combining probabilistic, distributed, and temporal operators will yield a new representation for system properties. These operators will enable us to express more sophisticated attack patterns, as well as describe a wide variety of local and global properties, ranging from performance to availability.
Using distributed operators localizes the description and supplies the necessary scalability and performance. Probabilistic reasoning adds resilience against the uncertainty inherent in parallel systems. Temporal operators provide for history-awareness and anticipation of future events. The new semantics and associated algorithms we are researching will allow for reasoning about and proving of these properties. We will prototype a compiler that translates formulas into monitoring programs that can instantly be deployed in the network.