Transcript No Slide Title

Survivability Analysis via
Model Checking
Oleg Sheyner
Jeannette Wing
Carnegie Mellon University
Carnegie Mellon University
7/18/2015
Model Checking: Overview
Finite Model
Property to be Checked
• States and Transitions
• Temporal Logic
• Abstract Automaton
• Specification Language
Does the model satisfy
the property?
Model Checker
• Explicit State
• Symbolic
No
Yes
Counterexample
Trace
Carnegie Mellon University
7/18/2015
Survivability
• A system is survivable if it can continue to provide a
acceptable level of service despite the presence of faults.
• Faults
– Accidental or malicious
– Not necessarily independent
• Acceptable levels of service precisely defined
• Cost must be included in the equation
Carnegie Mellon University
7/18/2015
Survivability Analysis: Overview
System Model
Phase 1
Survivability Property
Checker
Simple examples done
Scenario Graph
Reliability Query,
Cost Query, etc.
Annotations
(e.g., probabilities,
cost)
Phase 2
Analyzer
Initial efforts under way
Scenario Set
Carnegie Mellon University
7/18/2015
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 University
7/18/2015
Model
•
Network
–
–
–
–
•
Attacks
–
hosts
services
connectivity
trust relationships
Preconditions
Local (adversary)
Global (network-wide)
–
–
Traces
Effects
Local (adversary)
Global (network-wide)
–
•
Different flavors
Adversary
–
–
Knowledge about the
network
Privilege levels on hosts
•
Intrusion detection system
–
–
Network (inter-host)
Host-based (local)
Carnegie Mellon University
7/18/2015
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
• 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
Detected
Number
0
1
2
3
Carnegie Mellon University
7/18/2015
Scenario-Generating Properties
• These define secure operation - we look for counter examples
• Two cases
1) Don’t care about detection
– AG (adversary.privilege[ip2] < root)
– along all paths, it is always the case that the privilege of
the adversary is less than root
2) Want stealth
– AG ((adversary.privilege[ip2] < root) or (IDS.detected))
– As above or the ids detects the act that leads to privilege
elevation
Carnegie Mellon University
7/18/2015
!
Yeah!
noroot
access
root
IDS
adversary
ip1
ftp
sshd
rsh trust
ipa
firewall
rsh trust
Ftp .rhosts
on ip2
database
router
ip2
noroot
user
access
Rsh from
ipa to ip2
..
.
Sshd buffer
overflow on ip1
Ftp .rhosts
on ip2
ftp
Local buffer
overflow on ip2
Rsh from
ip1 to ip2
Carnegie Mellon University
7/18/2015
NuSMV Encoding
•
Network
–
–
1 attack host, 2 target hosts
with services
3x3 connectivity matrix
 existence of routing path
 ability to connect to ftp and
ssh services
–
•
•
3x3 trust matrix
Adversary
–
•
Privilege levels for each
host
NuSMV Statistics
82 bits of state (282 states)
<40K representation nodes
~7000 reachable states
•
2 sec runtime on 1GHz
Pentium III
•
8MB of memory used
Attacks
–
–
4 attacks
some have multiple flavors
Carnegie Mellon University
7/18/2015
Goal: Get Root, Avoiding Detection
Carnegie Mellon University
7/18/2015
Issues
• Metrics and Reliability Analysis
– What is the worst case probability of failure?
– What is the worst case probability that a service will ‘work’?
• Scalability
• Integration in a Vigilant System
Carnegie Mellon University
7/18/2015
Online and Offline Responses
Online
• What is the least restrictive firewall configuration that
thwarts the intruder?
Offline
• Where do we install an additional IDS to maximize chances
of detection?
• What is the smallest set of vulnerabilities we need to fix to
thwart the attacker?
Carnegie Mellon University
7/18/2015
Scalability
•
Expanded case study




5 hosts
4 new attacks
legitimate users
background traffic
 high priority
 low priority
 multiple firewall
configurations
•
NuSMV runtime: 4.5 hours
•
~ 6000 nodes in scenario
graph
•
Scalability remains a problem
•
Would like performance linear
in size of the reachable state
•
Alternative approach: explicitstate model checking
Carnegie Mellon University
7/18/2015
Tool Support
Scenario
Modeling
Generation
Analysis
Analyze
High-Level
Domain-Specific
Description
Scenario Set
Network
spec
(XML)
.
.
.
NuSMV
Modified
model
NuSMV
Most
reliability
effective fix
etc.
Raw
PRISM
Compiler
Worst-case
Scenario
PRISM
model
.
.
.
Graph
Decompile
&
.
.
.
Annotate
Carnegie Mellon University
7/18/2015
XML Fragment
<attack name="local_u2r" local="yes">
<local_preconditions>
<privilege host="target" eq="user"/>
</local_preconditions>
<global_preconditions>
<vulnerability host="target" name="vul_perl"/>
</global_preconditions>
<trace>
</trace>
<local_effects>
<privilege host="target" value="root"/>
</local_effects>
<global_effects>
</global_effects>
<detectable mode="both"/>
</attack>
Carnegie Mellon University
7/18/2015
Bottom Line
• Model checking technology can contribute to online
vigilance
– Complete graphs describing what can go wrong enable the
system to analyze the threat and pick the appropriate
response
• Scale is a problem
– Model checking cannot do the job alone
– Should be part of an integrated system employing multiple
techniques
Carnegie Mellon University
7/18/2015