Applying social network analysis to Social Media data supports better assessment of cyber-security threats by analyzing underground Social Media activities, dynamics between cyber-criminals, and topologies of dark networks. However, Social Media data are big and state of the art algorithms for social network analysis metrics require >=O(n + m) space and run in >=O(nm) time - some in O(n^2) or O(n^3) - with n = number of nodes, m = number of edges. Therefore, real-time analysis of Social Media activities to mitigate cyber-security threats with sophisticated social network metrics is not possible. To tackle this problem, we apply ideas of composability to big data and algorithms for social network analysis metrics. A network of humans, organizations, etc. is modeled with a graph G = (N, E) by aggregation of observed interactions E between targeted entities N. Because of the algorithmic complexity, composing network analysis metrics by analyzing sub-networks G1, G2, etc. can result in tremendous gain in calculation time.
ABOUT THE PROJECT:
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).
OUR TEAM:
William H. Sanders, David M. Nicol, Jim Blythe (University of Southern California), and Sean W. Smith (Dartmouth College)
ABOUT THE PROJECT:
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.
OUR TEAM:
Frank Pfenning (CSD, CMU) and Elsa L. Gunter
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
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.
OUR TEAM:
ABOUT THE PROJECT:
Modern networked systems are large and heterogeneous, and employ a variety of access control mechanisms that are the first line of defense against cyber-attack. These mechanisms include, but are not limited to:
- router-based dedicated firewalls, such as the Cisco PIX series;
- host-based firewalls, which could be based in software (such as iptables in Linux, or in-built firewalls in the operating system) or hardware (such as specialized NICs);
- operating-system-based mechanisms, such as discretionary access control in Linux or Windows, or more sophisticated mechanisms, such as the mandatory access control in NSA's SELinux and similar functionality provided for Windows by the Cisco Security Agent; and
- middleware-based mechanisms, such as the Java Security Manager, that provide for specification and enforcement of fine-granularity access control policies for Java programs.
This project is addressing the problem of estimating the degree to which the actual security posture given by the configurations of these diverse mechanisms complies with machine-checkable global policy, when (1) the system is too large to admit to an exhaustive analysis, and (2) we consider the possibility of intruders creating connections through compromised hosts set up as stepping stones. The foundational science we are developing consists of application of the statistical method of importance sampling to the problem of statistically estimating metrics that quantify a system’s compliance with global policy, and to the problem of finding the hosts that, if compromised, would have the largest negative impact on accessibility compliance, under our two assumptions. The results of our research will quickly be included in an existing tool we've developed that exhaustively validates compliance. This will transition the technology into practice; furthermore, the insights we gain will have application in other security domains where the challenge is to estimate the number of rare but disastrous states in combinatorially huge state spaces.