In my thesis I examine the problem of survivability in the context of access control security. Traditional state-transition models of access control systems focus on safety properties, with respect to preserving information confidentiality and integrity. The focus of modeling and analysis in this context is to validate whether mechanisms (derived from policies) that intercept requests and deny access can prevent the system for entering an unsafe state. Our goal in evaluating access control models extends beyond evaluating mechanisms that deny access, which can themselves become a method of attack. We investigate the design and analysis of mechanisms that can keep the system secure and available to authorized users, even when the system enters unsafe states as a result of an attack. We also formalize the notion of possible recovery from the impact of an attack, by activating appropriate response mechanisms.
We present an
extended access control model that can simulate attacker behavior, and
describe a framework where we can reason, both quantitatively and
qualitatively,
about the effectiveness of different access control survivability
mechanisms.
We show how we can validate survivability properties of interest using
standard model checking (including probabilistic model checking)
techniques
and use our model to study flexible and automated response to attacks.
Specifically, we present examples of how we can use our framework to
model
and analyze different strategies that can improve the assurance of
existing
access control configurations with respect to privilege escalation
attacks,
and in the mitigation of Denial of Service (DoS) threats.
Download my thesis here:
Modeling
Insecurity: Enabling Recovery-Oriented Security with Dynamic
Policies
(Send me an email for more details and if you want to read a draft about any of these topics)
DDoS Modeling
(Joint work with Adam Lee, Mahesh Viswanathan and Roy Campbell): As
a real world application of the formal models I present in my thesis,
we
investigate how we can measure the impact of different attacks on the
survivability
of a DDoS attack victim. One of the challenges with defeating a DDoS
(or
DoS) attack is that any solution that requires a server under attack
expend
more resources to characterize and filter attack packets makes the
server
more vulnerable to the attack in the first place. We show how we can
quantify
the ability of a victim to do useful work, even when the victim is
under
attack, and use this as a measure to compare different DDoS prevention
strategies. Our proposed framework can model and analyze of the costs
incurred
in implementing different DDoS prevention mechanisms, including
different
types of filtering, and provide feedback to security engineers
about
their relative benefits.
Access
Control Failure: Over the years,
security engineers have developed various strategies to mitigate the
impact
of an attack on the confidentiality and integrity of information in the
context of an access control system. An example is the chroot
"jail"
on Unix systems wherein the impact of an attack is contained by access
control mechanisms. In this project, we investigate the use of formal
methods
to analyze the effectiveness of such mechanisms with respect to
privilege
separation.
Unlinkability Analysis (Joint work with Apu Kapadia): We propose a policy engineering framework to address the unlinkability problem in the context of attribute-based access to distributed services. Our work examines how users with access to different audit logs in an organization can link access transactions and expose privacy sensitive attributes. We show how this problem may persist even when users employ anonymous credentials to gain access. We formalize the problem by defining the notion of an audit flow that represents an association between an end user and the set of users who can access this data. We present a framework for policy negotiation that can analyze conflicts and generate constraints, which when attached to audit records can provably enforce unlinkability. We show how these constraints are precise and complete under strong tranquility assumptions and extend our results to weak tranquility with versioning.
Sensor
Network-Authentication
(Joint
work with Chris Andrews and Aatif Awan): The
Mobile
Sensor-Network Authentication project is funded by NCASSR to
investigate
novel authentication and authorization mechanisms for sensor
networks.
In this project, we explore the feasibility of limited use of
public-key
cryptography in sensor networks by designing assymetric protocols that
shift the burden of executing public-key operations on base-stations
and
explore the use of attribute certificates for message
authentication.
Security for Pervasive Computing Systems: I am also interested in exploring issues related to developing infrastructure support for security services and protecting privacy concerns of users in pervasive computing enviroments. Our work in this area is motivated by security problems exemplified in the context of the Gaia project. I have worked on various projects in this context, including the design of an access control model that supports dynamic roles, with support for explicit collaboration among users in such environments; an authorization framework based on PKI with explicit support for attribute certificates; a cryptographic file system to protect confidentiality and integrity across heterogeneous underlying platforms; and a novel middleware infrastructure for security services in this context. Two of these (the authorization framework and the cryptographic file system) evolved out of student term projects from my class in Spring 2004.
Intrusion Detection (Joint work with Koushik Sen and Prasannaa Thati): We propose a new framework for intrusion detection that is based on runtime monitoring of temporal logic specifications. We specify intrusion patterns as formulas in an expressively rich and efficiently monitorable logic called EAGLE. EAGLE supports data-values and parameterized recursive equations, and allows us to succinctly express security attacks with complex temporal event patterns, as well as attacks whose signatures are inherently statistical in nature. We use an online monitoring algorithm that matches specifications of the absence of an attack with system execution traces, and raises an alarm whenever the specification is violated. We present our implementation of this approach in a prototype tool, called MONID and report our results obtained by applying it to detect a variety of security attacks in log-files. We believe that our approach is a useful application of light-weight formal methods technology to practical problems.
Secure Routing
In the context
of securing routing , we introduce the notion of "security awareness",
in terms of representing as well as enhancing route-setup based on
security
attributes carried within routing protocol packets. We investigate how
we can encode confidence, measured quantitatively in terms of trust
attributes,
as well as "Quality of Protection" metrics in terms of quantitative
parameters
used in cryptographic algorithms for message authenticity,
confidentiality
and integrity properties.