Files in this item



application/pdfModeling Insecu ... with Dynamic Policies.pdf (910kB)
(no description provided)PDF


Title:Modeling Insecurity: Enabling Recovery-Oriented Security with Dynamic Policies
Author(s):Naldurg, Prasad G.
Doctoral Committee Chair(s):Campbell, Roy H.
Doctoral Committee Member(s):Mickunas, Dennis; Nahrstedt, Klara; Kravets, Robin H.; Meseguer, José
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Security
Denial of Service (DoS)
Abstract:Policy engineering for access-control security has traditionally focused on specification and verification of safety properties (``nothing bad happens''). In most real systems however, resources and access mechanisms are regularly compromised, either maliciously by attackers, or inadvertently due to vulnerabilities caused by poor systems-engineering. I argue that the all-or-nothing nature of assurance provided by safety-engineering cannot describe or reason about systems that are secure and survivable--systems that can be engineered to proactively or reactively change their security policies and policy enforcement mechanisms, and thereby continue to provide assurance for critical resources, in spite of compromises and failures. In this thesis, I present a framework that extends traditional state-transition models of access control security, to describe timing guarantees and stochastic behavior, and show how we can introduce notions of information compromise, subsequent recovery (whenever possible) and flexible-response in a modular fashion. Our framework is also capable of describing insider attacks. I show how we need to focus on liveness properties (``something good eventually happens'') to explicitly capture the temporal and dynamic nature of enforceable guarantees required for survivability. I develop a new class of properties expressed as branching-time temporal logic formulas that focus on secure availability as a measure of survivability. For finite-state models, the validation of these formulas is decidable in polynomial time using automated model-checking techniques. To showcase the expressive power of our framework, I apply it to study network Denial of Service (DoS) attacks, and model resilience to such attacks as a survivability property. I show how we can systematically analyze the relative impact of different anti-DoS strategies by changing policies and mechanisms during an attack. Using our automated verification methodology, we formally prove for the first time whether strategies such as selective filtering, strong-authentication, and client-puzzles reduce the vulnerability of an example network to DoS attacks.
Issue Date:2004-05
Genre:Technical Report
Dissertation / Thesis
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-14

This item appears in the following Collection(s)

Item Statistics