Transcript The Rare Glitch Project

The Rare Glitch Project:
Scenario Graph Generation and
MDP-Based Analysis
Jeannette M. Wing
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA
The work on survivability analysis is funded by DARPA. It is done jointly
with Somesh Jha (University of Wisconsin) and Oleg Sheyner (CMU
graduate student).
Overview of Our Method
(Network) Model
Phase 1
(Survivability) Property
Checker
Scenario Graph
Reliability Query,
Cost Query, etc.
Analyzer
Phase 2
Scenario Set
Carnegie Mellon: The Rare Glitch Project
2
Jeannette M. Wing
Relation to ARO Proposal
 Hypothesis: Our two-phase method and tool suite
are applicable to analyzing embedded systems.
 Rationale
 Network
model is simpler (bus-based, not end-to-end).
 Reliability and cost are important factors in embedded
systems design.
 Our plan
 Enrich
and make current tool suite robust.
 Apply method to embedded systems examples.
 Pursue foundational issues wrt models for reliability
and cost analyses.
Carnegie Mellon: The Rare Glitch Project
3
Jeannette M. Wing
Survivable Systems
 What if
a
terrorist hacker brings down the nation’s power grid?
 an act of Mother Nature causes the international
financial network to fail?
 Critical infrastructures
 Utilities:
gas, electricity, nuclear, water, …
 Communications: telephone, networks, …
 Transportation: airlines, railways, highways, …
 Medical: emergency services, hospitals, …
 Financial: banking, trading, …
Carnegie Mellon: The Rare Glitch Project
4
Jeannette M. Wing
Survivability
 A system is survivable if it can continue to provide
end services despite the presence of faults.
Carnegie Mellon: The Rare Glitch Project
5
Jeannette M. Wing
Modeling for Survivability Analysis
 Our starting point
 Handle

both benign and malicious faults.
Throw out independence assumption.
 Incorporate

semantics of end service in model.
Do not necessarily treat nodes and links the same.
 Include
cost in the model from the start.
 Steps in our approach
 Model
general network topology (nodes and links)
 Analyze in two phases for


Functional behavior
Reliability, cost, etc.
Carnegie Mellon: The Rare Glitch Project
6
Jeannette M. Wing
Phase 1
Network Model =
Survivability Property =
A set of concurrently executing
Finite State Machines.
A predicate in CTL.
Model Checker =
(modified) NuSMV
Scenario Graph =
A set of related examples.
Carnegie Mellon: The Rare Glitch Project
7
Jeannette M. Wing
Simple Example: A Banking System
FRB 2
FRB 3
FRB 1
MC 2
MC 1
a1
b1
b2
MC 3
c1
a2
Bank A
Carnegie Mellon: The Rare Glitch Project
Bank B
8
Bank C
Jeannette M. Wing
Network Model
 Processes
 Nodes

and links are processes (i.e., FSMs)
banks, money centers, federal reserve banks, and links
 Communication
via shared variables (i.e., finite
queues)

representing channels, and hence interconnections.
 Failures
 Faults

fault:{normal, failed, intruded}
 Links


represented by special state variable
and banks can fail at any time
Failed link blocks all traffic.
Failed bank routes all checks to an arbitrarily chosen
money center.
 Money
centers and federal reserve banks do not fail.
Carnegie Mellon: The Rare Glitch Project
9
Jeannette M. Wing
Survivability Properties
 Fault-related
 Money
never deposited into wrong account.
 AG(error)
 Service-related
A
check issued eventually clears.
 AG(checkIssued
Carnegie Mellon: The Rare Glitch Project
 AF(checkCleared))
10
Jeannette M. Wing
Scenario Graphs
 Given a state machine, M, and a property, P, a
scenario graph is a concise representation of the set
of traces of M with respect to P.
P
= fault property

P
A fault scenario graph represents all system traces that
end in a state that does not satisfy P.
= service property

A service success (fail) scenario graph represents all
system traces in which an issued service successfully
finishes (fails to finish).
Carnegie Mellon: The Rare Glitch Project
12
Jeannette M. Wing
Fault Scenario Graph
Intuition:
• Each “counterexample” spit out by the
model checker is a scenario.
• Survivability property gives a slice of the
model.
Each path is a scenario of how a fault can occur.
Carnegie Mellon: The Rare Glitch Project
13
Jeannette M. Wing
Survivability Properties
 Fault-related
 Money
never deposited into wrong account.
 AG(error)
 Service-related
A
check issued eventually clears.
 AG(checkIssued
Carnegie Mellon: The Rare Glitch Project
 AF(checkCleared))
14
Jeannette M. Wing
A Service Success Scenario Graph
issueCheck(A, C)
up(a2)
down(a2) & up(a1)
send(A, MC-2)
send(A, MC-1)
send(MC-2, FRB-1)
send(MC-1, FRB-2)
send(FRB-1, FRB-3)
send(FRB-2, FRB-3)
send(FRB-3, MC-3)
up(c1)
send(MC-3, C)
debitAccount
Carnegie Mellon: The Rare Glitch Project
15
Jeannette M. Wing
A Service Fail Scenario Graph
issueCheck(A, C)
down(A)
pick(MC-2)
up(A)
pick(MC-1)
down(c1)
FAIL
up(a2)
down(a2)
down(a1)
send(A, MC-2)
down(c1)
send(A, MC-1)
FAIL
FAIL
Carnegie Mellon: The Rare Glitch Project
up(a1)
down(c1)
FAIL
16
Jeannette M. Wing
Overview of Method
Network Model
Phase 1
Survivability Property
Checker
Scenario Graph
Reliability Query,
Cost Query, etc.
Annotations
(e.g., probabilities,
cost)
Analyzer
Phase 2
Scenario Set
Carnegie Mellon: The Rare Glitch Project
17
Jeannette M. Wing
Phase 2: Reliability Analysis (in a Nutshell)
 Annotations = Probabilities
 Use
Bayesian Networks to model dependence of
events.
 Symbolic
 Use

symbolic probabilities
high, medium, low
 Use
NDFA theory to compute scenario set.
 Continuous
 Use

numeric probabilities
[0.0, 1.0]
 Use
Markov Decision Processes to model both
nondeterministic and probabilistic transitions.
Carnegie Mellon: The Rare Glitch Project
18
Jeannette M. Wing
Phase 2: Continuous Analysis
 Use real values for probabilities.
 May leave probabilities of some events unspecified.
 Markov Decision Processes

Mix of nondeterministic and probabilistic transitions
 Why? System is not closed.
 Hard
to assign probabilities to some faults (e.g.,
intrusions).
 Environment makes choice (i.e., decision) and can be
demonic!
Carnegie Mellon: The Rare Glitch Project
23
Jeannette M. Wing
Reliability Analysis
Goal of (malicious) environment: Devise an optimal
policy to minimize reliability.
 Assign to each state, s, a value, V(s), computed
using a standard policy iteration algorithm from MDP
literature.
 Let V* be the value function after convergence.
Then, for initial state of scenario graph, s0, V*(s0)
computes worst-case probability of service
eventually finishing.
Carnegie Mellon: The Rare Glitch Project
24
Jeannette M. Wing
A Typical Example
0.65
0.6
0.7
0.6
0.7
0.4
0.6
0.3
Good
Bad
V(Good) = 1.0
V(Bad) = 0.0
Carnegie Mellon: The Rare Glitch Project
25
Jeannette M. Wing
Bayesian Network for Bank
Example
P(c1) = 1/2
P(a1) = 1/2
a1
c1
P(b1) = 1/2
b1
P(a2 | a1) = 1/2
P(a2 | a1) = 1/4
Carnegie Mellon: The Rare Glitch Project
a2
P(b2) = 1/2
b2
26
Jeannette M. Wing
A Service Success Scenario Graph
3/8
issueCheck(A, C)
up(a2)
1/4
down(a2) & up(a1)
send(A, MC-2)
send(A, MC-1)
send(MC-2, FRB-1)
send(MC-1, FRB-2)
send(FRB-1, FRB-3)
send(FRB-2, FRB-3)
1/2
send(FRB-3, MC-3)
up(c1)
The worst case probability that a check
send(MC-3, C) issued by Bank A on Bank C is
(1/2 * 3/8) + (1/2 * 1/4) = 5/16
debitAccount
Carnegie Mellon: The Rare Glitch Project
27
Jeannette M. Wing
Cost-Benefit Analysis
Goal: Choose a set of links to upgrade to achieve
higher reliability, given my cost constraints (e.g.,
fixed budget).
 Identify new actions that correspond to decisions an
architect needs to make (e.g., upgrade a1).
 Associate a cost with each action.
 Define constraints on costs.
Carnegie Mellon: The Rare Glitch Project
28
Jeannette M. Wing
Upgrade Links in Banking System
FRB 2
FRB 3
FRB 1
MC 1
?
?
a1
MC 2
b1
b2
MC 3
?
c1
a2
Bank A
Carnegie Mellon: The Rare Glitch Project
Bank B
29
Bank C
Jeannette M. Wing
Cost Constraint Example
 Assume:
 If
we upgrade a1 and c1 then P(a1) and P(c1)
both increase to 3/4 .
 If a2 is upgraded, then P(a2) is:


P(a2|a1) = 3/4
P(a2| a1) = 3/8
 Aim: Maximize the worst-case reliability subject to the
constraint that at most two links can be upgraded. Solve this
non-linear integer programming problem:

xa1 + xa2 + xc1 < 2
 Best option: Upgrade a1 and c1.
xa1 = 1 and xa2 = 1 7/16
xa1 = 1 and xc1 = 1 39/64
xa2 = 1 and xc3 = 1 9/16
Carnegie Mellon: The Rare Glitch Project
30
Jeannette M. Wing
Constrained Markov Decision
Processes
<S, A, P, c, d>
 S is a finite state space.
 A is a finite set of actions.
 P are transition probabilities. Psas’ is the probability
of moving from state s to s’ if action a is chosen.
 c: (S x A)   is the immediate cost. c(s, a) is the
cost of choosing action a at state s.
 d: (S x A)  k is a k-dimensional vector of
immediate costs, captures additional cost
constraints.
Carnegie Mellon: The Rare Glitch Project
31
Jeannette M. Wing
Survivability Case Studies
 Somesh Jha
 Trading
floor model of major investment bank (being
“sanitized”)






10K lines of NuSMV
half-million nodes in scenario graph
50 threat scenarios
45 found by system
5 new threat scenarios found
With independence assumption, too many misses.
 B2B


e-commerce NYC start-up (Jha)
50K lines of Statecharts
2 million NuSMV beyond capability of tool
 Oleg Sheyner

Intrusion detection (ongoing)
Carnegie Mellon: The Rare Glitch Project
32
Jeannette M. Wing
Intrusion Detection System Case
Study
 Done by Oleg Sheyner and Lincoln Labs.
 Motivated by hand drawn poster of attack scenarios.
 Illustrates only first part of method.
Carnegie Mellon: The Rare Glitch Project
33
Jeannette M. Wing
Example of Attack Tree Developed by
a Professional Red Team
 Sandia Red Team “White Board” attack tree from DARPA
CC20008
Information
battle 35
space preparation experiment
Carnegie Mellon:
The Rare Glitch
Project
Jeannette M. Wing
Phase 1 Example:
Multistage Network Penetration
IDS
adversary
ipa
firewall
ip1
ftp
sshd
database
router
ip2
ftp
Goal: Root access to host ip2
Attack Arsenal
•
•
•
•
Detected
Sshd buffer overflow - remotely get root
Ftp .rhosts file - establish trust between hosts
Remote login - exploit trust between hosts
Local buffer overflow - locally get root
Carnegie Mellon: The Rare Glitch Project
36
Jeannette M. Wing
NuSMV Encoding
 Network
 1 attack host, 2 target hosts
with services
 3x3 connectivity matrix



 NuSMV Statistics
 82 bits of state (282
states)
<40K representation nodes
~7000 reachable states
existence of routing path
ability to connect to ftp and
ssh services
2 sec runtime on 1GHz
Pentium III
 8MB of memory used

3x3 trust matrix
 Adversary
 Privilege levels for each
host
 Attacks
 4 attacks
 some have multiple flavors
Carnegie Mellon: The Rare Glitch Project
38
Jeannette M. Wing
Scenario-Generating Properties
 Don’t care about detection
 AG
(adversary.privilege[2] < root)
 Want stealth
 AG
((adversary.privilege[2] < root) or (IDS.detected))
Carnegie Mellon: The Rare Glitch Project
39
Jeannette M. Wing
The Rare Glitch Tool Suite
Checkers and Provers
Specification and
Modeling
Languages
Specification
XML
Analysis Engines
Checkmate
Reliability and
Cost Analyzers
Prism
XML2nuSMV
nuSMV
Scenario
graph
Counterexamples
Explanation
Generator
Model
PVS
Abstraction/
Refinement
Processor
Symp
…
…
Carnegie Mellon: The Rare Glitch Project
43
Jeannette M. Wing
Plan in Relationship to The Rare
Glitch Project
 Enrich and make current tool suite robust.
 Integrate
with other existing project tools.
 Apply method to embedded systems examples.
 Work
with Clarke to add reliability analysis to
automotive example.
 Pursue foundational issues wrt models for reliability
and cost analyses.
 Understand
relationship to other probabilistic models,
hybrid models, etc.
Carnegie Mellon: The Rare Glitch Project
44
Jeannette M. Wing