Modeling Insecurity: Enabling Recovery-Oriented Security with Dynamic Policies

Naldurg, Prasad G.

Permalink

https://hdl.handle.net/2142/10794 Copy

Description

Title

Modeling Insecurity: Enabling Recovery-Oriented Security with Dynamic Policies

Author(s)

Naldurg, Prasad G.

Issue Date

2004-05

Doctoral Committee Chair(s)

Campbell, Roy H.

Committee Member(s)

• Mickunas, Dennis
• Nahrstedt, Klara
• Kravets, Robin H.
• Meseguer, José

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/10794

Copyright and License 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).

Owning Collections