Transcript Theory Generation for Security Protocols

Vulnerability Analysis Using Attack Graphs
Jeannette M. Wing
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA USA
joint work with Somesh Jha (Wisconsin) and Oleg Sheyner (CMU)
Network of Networks
MIT
Microsoft
Office of Homeland
Security
Arsenal of Actions
• buffer overflow
• ftp .rhosts
• remote login
Carnegie Mellon
•…
Attack Graphs
2
Jeannette M. Wing
Example of Attack Graph Developed by a
Professional Red Team Drawn By Hand
•
Sandia Red Team “White Board” attack tree from DARPA CC20008
Information battle space preparation experiment
Sandia Red Team “White Board” attack graph
from DARPA CC20008 Information battle space
preparation experiment
Attack Graphs
3
Jeannette M. Wing
Vulnerability Analysis by System Administrators
• Information-gathering
– What attacks is my system vulnerable to?
• Is a different configuration of my system less “attackable”?
– What is the likelihood of this attack?
– Is this on-going attack similar to any of the known attacks?
• Decision-making
– If I put this set of security measures in place, what attacks
can I prevent?
– Given the likelihood of certain attacks, deploying which
measures will increase the security of my system?
– What is the most cost-effective set of measures I should
deploy, to increase the security of my system?
Attack Graphs
4
Jeannette M. Wing
Problem Statement
• Problem: Generating attack graphs by hand is tedious,
error-prone, and impractical for large systems.
• Our Goal: Automate the generation and analysis of attack
graphs.
– Generation
• Must be fast and completely automatic
• Must handle large, realistic examples
• Should guarantee properties of attack graphs
– Analysis
• Must enable further security analysis by system administrators
• Should support incremental, partial specification
Attack Graphs
5
Jeannette M. Wing
Overview of Our Method
System Model
Security Property
Generator
Phase 1
Attack Graph
Annotations
Query: What actions are
Query: What is the likelihood
necessary for the intruder to
succeed?
Phase 2
Minimization
Analyzer
Attack Subgraph
Attack Graphs
that the intruder goes
undetected?
Reliability
Analyzer
…
Query: What is the cost
benefit of deploying this
security measure?
Cost
Analyzer
Probabilistic Attack Graph
6
Jeannette M. Wing
Why Model Checking?
• Pragmatic reasons
– Off-the-shelf technology
– Major verification success story
• Technical reasons
–
–
–
–
Fast, automatic
Large state spaces
Handles safety and liveness properties
Generates counterexamples
Attack Graphs
7
Jeannette M. Wing
Model Checking Primer
Finite State Machine
model M
Temporal Logic
property F
F = AG p
AF p, EG p, EF p
Model Checker
yes
counterexample
F is falsified here.
Attack Graphs
8
Jeannette M. Wing
Counterexample = Attack
F  AG p
single counterexample = violation of F
= path by which intruder succeeds
= attack
For example,
F  AG (intruder does not have admin access to host H)
Hence, an attack (violation of F) is an example of how
the intruder can gain unauthorized access to H.
Attack Graphs
9
Jeannette M. Wing
Definition of Attack Graph
• Given
– a finite state model, M, of network
– a security property F
• An attack is an execution of M that violates F.
• An attack graph is a set of attacks of M.
Attack Graphs
10
Jeannette M. Wing
Properties of Attack Graphs
• Exhaustive
– All possible attacks are represented in G.
• Succinct
– Only relevant states are contained in G.
– Only relevant transitions are contained in G.
The next two algorithms satisfy these properties.
Attack Graphs
11
Jeannette M. Wing
Symbolic-State Attack Graph Generation Algorithm
Inputs
– M = <S, S0  S, R  S X S>
 F = AG (~unsafe) (a safety property in CTL)
Output
–
Attack graph G = (Sunsafe, S0F, RF )
Algorithm
1. Sunsafe = modelCheck(S, S0, R, F)
(* Use an iterative algorithm derived from the fixpoint
characterization of AG operator. *)
2. S0F = S0  Sunsafe
3. RF = R  (Sunsafe X Sunsafe)
Attack Graphs
12
Jeannette M. Wing
Explicit-State Attack Graph Generation Algorithm
Inputs
– M
– F = LTL property (safety or liveness)
Output
- Attack graph G s.t. L(G) = L(M  ~F)
(request 
(response))
Algorithm
1. Interpret both network model M and security property F as
Buchi automata.
• M and F induce languages L(M ) and L(F).
2. Compute L(M )\L(F) = executions of M that violate F.
3. Construct M  ~F by computing intersection of Buchi
automata.
Attack Graphs
13
Jeannette M. Wing
Performance Charts
1200.00
1200.00
1000.00
1000.00
800.00
800.00
sec 600.00
sec 600.00
400.00
400.00
200.00
200.00
0.00
0.00
5
2
3
4
4
Actions
5
6
Hosts
3
7
3
4
4
Actions
8
Symbolic-state algorithm
Attack Graphs
5
2
14
5
6
Hosts
3
7
8
Explicit-state algorithm
Jeannette M. Wing
Performance
45
40
Generation Time (sec)
35
30
25
20
15
10
5
0
0
100000
200000
300000
400000
500000
600000
700000
800000
900000
Reachable Transitions (Edges)
Linear Regression R2 = 0.9967
Attack Graphs
15
Jeannette M. Wing
An Illustrative Example
IIS Web
Server
attacker
IDS
Windows
ftp
database
firewall
firewall
Linux
Action Arsenal
IIS buffer overflow:
remotely get root
Squid portscan:
port scan
LICQ remote-to-user: gain user privileges remotely
scripting exploit:
gain user privileges remotely
local buffer overflow: locally get root
Attack Graphs
16
Always Detected
Jeannette M. Wing
Modeling a Network and Intruder
• Set of hosts H
•
•
•
•
• Intruder
running services
CVE vulnerabilities
trust relationships
misc. configuration
•
•
• Set of networks N
•
•
each network n  N is a
subset of H
packet filter between each
pair of networks n1, n2
store of knowledge
privileges on each host
• Set of actions A
•
•
preconditions
postconditions
• Intrusion detection systems
•
•
Attack Graphs
placement: P  N  N
detectability per action
17
Jeannette M. Wing
Example Attack Graph
F = G (intruder.privilege(Linux) < root)
Begin
IIS buffer
overflow
CAN-2002-0364
Squid portscan
CVE-2001-1030
Local buffer
overflow
CVE-2002-0004
LICQ remoteto-user
CVE-2001-0439
Done!
Attack Graphs
18
Jeannette M. Wing
Overview of Our Method
System Model
Security Property
Generator
Phase 1
Attack Graph
Annotations
Query: What actions are
necessary for the intruder to
succeed?
Phase 2
Minimization
Analyzer
Reliability
Analyzer
…
Cost
Analyzer
Attack Subgraph
Attack Graphs
19
Jeannette M. Wing
Minimization Analysis
Scenario: The system analyst must decide
–
–
–
among several different firewall configurations, or
among several vulnerabilities to patch, or
among several intrusion detection systems to set up,
each of which prevents different subsets of actions.
What should he do?
Problem Question (Minimum Critical Set of Actions): What is a
minimum set of actions that must be prevented to guarantee
the intruder cannot achieve his goal?
Solution (Sketch):
1. Reduce MCSA to Minimum Hitting Set (MHS) Problem [JSW02].
2. Reduce MHS to Minimum Set Covering (MSC) Problem [ADG80].
3. Use textbook Greedy Approximation Algorithm to approximate
solution [CLR85].
Attack Graphs
20
Jeannette M. Wing
Minimum Critical Set of Actions
A = the set of actions available to the intruder
Def 1: A set of actions C is critical if the intruder cannot
achieve his goal using only actions in A \ C.
Def 2: A set of actions C is realizable if the intruder can
achieve his goal using only actions in C.
Def 3: A critical set of actions C is minimum if there
is no critical action set of smaller size.
Minimum Critical Set of Actions (MCSA):
Given a set of actions A and an attack graph G, find
a minimum critical action subset C  A
Finding a minimum set: NP-complete
Attack Graphs
21
Jeannette M. Wing
Reduction to Minimum Hitting Set Problem
Minimum Hitting Set (MHS):
Given a collection C of subsets of a finite set S, find a
minimum subset S’  S such that each subset in C contains
at least one element from S’.
MCSA and MHS are polynomially-equivalent.
MHS:
Collection of
subsets C
MCSA:
Collection of realizable
sets of actions
[JSW02b] Jha, Sheyner, Wing, “Two Formal Analyses of Attack Graphs,”
Computer Security Foundations Workshop, Nova Scotia, June 2002.
Attack Graphs
22
Jeannette M. Wing
Sketch of Reduction from MCSA to MHS
A
B
C
D
E
F
H
G
B
C
D
G
H
I
I
F
E
S1 = {G,H,I}
S2 = {C,E,F,H}
S3 = {B,D,E}
Attack Graphs
23
Jeannette M. Wing
Reduction of MHS to Minimum Set Covering
Minimum Set-Covering (MSC):
Given a collection C of subsets of a finite set S that
covers S, find a minimum sub-collection C’  C that
covers S.
MHS and MSC are polynomially-equivalent [ADP80].
Use textbook Greedy Approximation Algorithm for MSC
[CLR85, p. 975.]
Attack Graphs
24
Jeannette M. Wing
LICQ Coverage
F = G (intruder.privilege(Linux) < root)
Attack Graphs
25
Jeannette M. Wing
Other Minimization Analyses [JSW02b, S04]
Scenario: The system analyst has a set of measures,
each of which prohibits a subset of actions.
E.g., M = {packet filter firewall, application firewall, smart cards, one-time
passwords, authentication policy servers, VPNs, anti-virus software, email
filters, database encryption, host-based IDS, net-based IDS, network
monitors, auditing, key stroke replicator, log analysis, forensic software,
hardened O/S}
– Problem Question 1: If he deploys all measures, does the system
become safe? [JSW02b]
• Solution Approach (Naïve): Remove all edges from graph that are
“covered” by the measures. Reachability analysis is linear time in size
of graph.
– Problem Question 2: What is the smallest subset of measures he can
deploy to make the system safe? [S04]
• Solution Approach: Greedy algorithm with provable bounds. General
case is NP-complete (slightly more complex than minimum cover
problem).
Attack Graphs
26
Jeannette M. Wing
Overview of Our Method
System Model
Security Property
Generator
Phase 1
Attack Graph
Annotations
Query: What is the likelihood
that the intruder goes
undetected?
Phase 2
Minimization
Analyzer
Reliability
Analyzer
…
Cost
Analyzer
Probabilistic Attack Graph
Attack Graphs
27
Jeannette M. Wing
Reliability Analysis
Scenario: The system analyst must decide between installing a
network-based IDS between host 1 and host 2 or a host-based
IDS on host 2. Which increases the likelihood that he will
detect an intruder?
Problem Question: What is the probability of the intruder
succeeding? I.e., what is the worst-case probability of
reaching an unsafe state?
Solution Approach:
1. Annotate attack graph with probabilities.
2. Interpret annotated attack graph as a Markov Decision Process.
3. Run the standard MDP value iteration algorithm to compute the
optimal policy that results in maximum benefit/minimum cost for
system analyst (decision maker).
Attack Graphs
28
Jeannette M. Wing
Status of Tool Suite
Outpost
Server
SQL
database
Model
Builder
<XML/>
Host
Configuration
Data
System and Goal
Specification
Network
Configuration
Data
MITRE
Lockheed
Nessus
Attack Graph
Generators
Outpost
Clients
Library of
Actions
Attack Graph
Analyzers
Graphical
User Interface
Attack Graphs
29
Jeannette M. Wing
XML Specification of a Host
<host name=“lin" ip="192.168.0.4" network="internal">
<services>
<Squid/>
<LICQ/>
<database/>
</services>
<connectivity>
<remote id="ferrari"> <W3SVC/> </remote>
<remote id="smilla"> <ftp/> <sshd/> </remote>
</connectivity>
<cve>
<CVE_2002_0004/>
<CVE_2001_1030/>
<CVE_2001_0439/>
</cve>
</host>
Attack Graphs
30
Jeannette M. Wing
XML Specification of an Action
<action name=“licq_r2u" cve1=“CVE-2001-0439">
<local_preconditions>
<privilege host=“source” rel=“gte” value=“user”/>
<privilege host=“target” rel=“eq” value=“none”/>
<knowledge name=“scan” value=“TRUE”/>
</local_preconditions>
<global_preconditions>
<service host=“target” name=“LICQ”/>
<connectivity from=“source” service=“LICQ”/>
</global_preconditions>
<local_effects>
<privilege host=“target” value=“user”/>
</local_effects>
<global_effects>
<detectable mode=“yes”/>
</global_effects>
</action>
Attack Graphs
31
Jeannette M. Wing
Information Sources
• MITRE Corp. Outpost
– Host identification
– Vulnerabilities
– Services
<host name=“lin“ ip=|Outpost|>
<services source=|Nessus|>
<connectivity source=|ANGI|>
• Lockheed ATL Next Generation
<cve source=|Outpost|>
Infrastructure (ANGI)
</host>
– Network topology
– Connectivity
• Nessus vulnerability scan info
Attack Graphs
32
Jeannette M. Wing
Related Work
• Philips and Swiler 1998
– Tool constructs “attack graph” by forward exploration starting from
initial state. Also based on model checking.
• Our backward algorithm saves space (vulnerabilities not relevant are
not explored) and can handle liveness properties.
– Models only attacks
• Our modeling framework can handle arbitrary state transitions
(actions), not just actions.
• Dacier 1994, Orlato et al. 1999
– Privilege graphs: nodes = sets of user privileges, edges =
vulnerabilities. Explore privilege graphs to construct attack graphs.
– Defines a metric, Mean-Effort-To-Failure, based on attack graphs.
• Ritchey and Ammann 2001
– Also use model checking. Produces only one counter-example
(attack).
– No post-facto analysis.
Attack Graphs
33
Jeannette M. Wing
Limitations => Current and Future Work
• Input to graph generation
– Need a library of specifications of actions (with CMU students)
– CERT advisories, MSR security bulletins, Symantec, …
• Ontology for vulnerabilities and exploits
• Discover new attacks
• More analyses
– Reduction of “attack surface”
• Which configuration of my system is less “attackable”?
– Ongoing with Jon Pincus at MSR/Redmond and CMU students
– Cost-benefit analysis
• Exploit MDP theory further
Attack Graphs
34
Jeannette M. Wing
Recent References
[JSW02a] Jha, Sheyner, and Wing, “Minimization and Reliability Analyses
of Attack Graphs,” Carnegie Mellon technical report, CMU-CS-02-109,
February 2002.
[JSW02b] Jha, Sheyner, Wing, “Two Formal Analyses of Attack Graphs,
Computer Security Foundations Workshop, Nova Scotia, June 2002.
[SHJ+02] Sheyner, Haines, Jha, Lippmann, and Wing, “Automated
Generation and Analysis of Attack Graphs,” IEEE Symposium on
Security and Privacy, May 2002.
Attack Graphs
35
Jeannette M. Wing