Transcript motorola-NUworkshop0.. - Northwestern University

Lab for Internet and Security
Technology (LIST) in Northwestern
Yan Chen
Northwestern University
1<#>
Introduction
• Work on network security, measurement and
monitoring
• Five Ph.D. students and two M.S. students
• Collaborate widely
– NU colleagues: Peter Dinda, Ming-Yang Kao, Aleksandar
Kuzmanovic, Gokhan Memik, and Hai Zhou (and their
students)
– Other industry & academia researchers, e.g., Judy Fu,
Phil Robert and Pete McCann in Motorola.
2<#>
Automatic Vulnerability Checking
of Wireless Protocols through
TLA+
Published in Workshop of Network Protocol
Security 2006
3<#>
TLA+ Vulnerability Checking
Flow
TLA+
Protocol
Specification
Stop
No
Attacker
TLA+
Specification
TLC
Model
Checking
Found
Vulnerability ?
Yes
Property
TLA+
Specification
Weaken
Attacker
Analyze
Severity
• Avoid state space explosion in property checking
• Model attackers’ capabilities for finding realistic
4<#>
attacks
Case Studies
• Initial ranging
• Authentication process
• Choices based on the criticality of
function and the probability of
vulnerability
5<#>
Initial Ranging Process
• Initial ranging: the first step
an SS communicates with a
BS via message exchanges.
• An SS acquires correct timing
offset and power adjustments
• The request-response
communication happens until
the BS is satisfied with the
ranging parameters.
• ’Actual’ data communication
can happen only if the initial
ranging is successful.
6<#>
Property to Check
• SS can get service (getting into “Done”
state) infinitely often
[]<>(SSstate = “Done”)
– Need to make sure that such a property is true
even without an attacker (weakest attacker
model)
7<#>
DOS during Initial Ranging
(found by TLC Model Checking)
DL Subframe
UL Subframe
Contention-based
Initial Ranging Slots
REQ
REQ
8<#>
Conclusions
• First step towards automatic vulnerability
checking of WiMAX protocol with
completeness and correctness guarantees
• Use TLA+/TLC to model malfunction DoS
attacks
– Avoid state space explosion in property
checking
– Model attackers’ capabilities for finding
realistic attacks
• Analyzed initial ranging and authentication
process in 802.16 protocols
9<#>
Ongoing Work
• Development of a rigorous process in
protocol specification using TLA+
• Check vulnerabilities in other parts of
802.16 standards such as mobility
support and handoff procedures
• Examination of WiMAX upper layer
protocols: Proxy Mobile IPv4, Mobile
IPv6, etc.
10<#>
Intrusion Detection and Mitigation
for WiMAX Networks (WAIDM)
Published in IEEE Symposium on
Security and Privacy, ACM SIGCOMM,
IEEE/ACM Transaction on Networking,
IEEE Infocom, ACM SIGCOMM IMC,
IEEE ICDCS
The Spread of Sapphire/Slammer Worms
12
How can it affect cell phones?
• Cabir worm can infect a cell phone
– Infect phones running Symbian OS
– Started in Philippines at the end of 2004, surfaced in
Asia, Latin America, Europe, and US
– Posing as a security management utility
– Once infected, propagate itself to other phones via
Bluetooth wireless connections
– Symbian officials said security was a high priority of the
latest software, Symbian OS Version 9.
• With ubiquitous Internet connections, more
severe viruses/worms for mobile devices will
happen soon …
13
Adaptive Intrusion Detection and Mitigation
for WiMAX Networks (WAIDM)
• Attached to a switch connecting BS as a black box
• Enable the early detection and mitigation of global scale
attacks
• Could be differentiator for Motorola’s 802.16 products
Internet
Users
Inter
net
802.16
BS
802.16
BS
scan
port WAIDM
system
User
s
Switch/
BS controller
Switch/
BS controller
802.16
BS
802.16
BS
Users
User
s
(a)
Original configuration
(b)
WAIDM deployed
Features of WAIDM
• Scalability (ready for field testing)
– Online traffic recording
» Reversible sketch for data streaming computation
» Record millions of flows (GB traffic) in a few hundred KB
» Infer the key characteristics (e.g., source IP) of culprit
flows for mitigation
– Online sketch-based flow-level anomaly detection
» Adaptively learn the traffic pattern changes
• Accuracy (initial design & evaluation done)
Integrated approach for false positive reduction
– Automatic polymorphic worm signature generation(Hamsa)
– Network element fault Diagnostics
WAIDM
Architecture
Normal flows
Reversible
sketch
monitoring
Streaming
packet
data
Filtering
Remote
aggregated
sketch
records
Sent out for
aggregation
Local
sketch
records
Part I
Sketch based
statistical anomaly
detection (SSAD)
Sketchbased
monitoring
& detection
Keys of suspicious flows
Keys of normal flows
Suspicious flows
Per-flow
monitoring
Signature
-based
detection
Polymorphic
worm detection
(Hamsa)
Network fault
diagnosis (ODD)
Intrusion or
anomaly alarms
Data path
Control path
Modules on
the critical
path
Modules on
the non-critical
path
Part II
Per-flow
monitoring
& detection
Hamsa: First Network-based Zero-day
Polymorphic Worm Signature Generation System
• Fast: in the order of seconds
• Noise tolerant and attack resilient
• Detect multiple worms in one protocol
Network
Tap
TCP
25
Protocol
Classifier
TCP
53
TCP
80
. . .
TCP
137
UDP
1434
Suspicious
Traffic Pool
Known
Worm
Filter
Worm
Flow
Classifier
Normal traffic
reservoir
Normal
Traffic Pool
Hamsa
Signature
Generator
Real time
Policy driven
Signatures
Thanks
18<#>
TLA+ Protocol Specification
• Protocol specification in TLA+ can be
easy or difficult
– FSM easily translate to TLA+
– Tricky from English description to TLA+
spec: ambiguity, re-design, etc.
• Process of protocol specification:
– Identify principals
– Modularize principal behaviour using TLA+
– Combine principal specs to form a protocol
spec
19<#>
TLA+ Protocol Specification
Challenges
• Challenge: Vagueness in English
specification and the correctness in its
translation to TLA+.
• Common problem for all approaches
• Solutions:
– No easy solution exists!
– Best designing protocols in TLA+
– Consult standards committee, product
implementation teams among other
things
20<#>
Attacker Modelling
Attacker capability model similar to
Dolev-Yao model:
• Basically, attackers can:
– Eavesdrop on and store messages.
– Replay old messages.
– Inject or spoof unprotected messages.
– Corrupt messages on the channel by causing
collisions.
• Assume the ideal cryptography:
unforgeable signatures, safe encryption,
21<#>
and safe digest
Attacker Modelling Challenges
• Challenge: How to find all realistic attacks?
– Model too strong: hide stealthy attacks
– Model too weak: missing vulnerabilities
• Our solution:
– Start with a relatively strong attacker model
» TLC model-checks may yield unrealistic attacks.
– Then weaken the attacker model
» E.g.: the attacker can continuously corrupt a response from
the BS.
» Add restrictions on attacker to exclude such attacks.
• This dynamic modification of attacker model will
end up with
– a complete robustness proof OR
– report of all attacks
22<#>
Property Spec
• Focus on malfunction DoS attacks
currently
– Client needs to reach a termination
<>[] (\A i\in PartySet:
Party[i].state=ObjState)
– Client may not terminate
[]<>(\A \in PartySet:
Party[i].state=ObjState)
23<#>
Property Spec Challenges
•
Challenge: TLC cannot check all
properties expressible in TLA+
•
Our Solution: Specify properties
in restricted format
24<#>
Model Checking by TLC
• TLC is a model checker for TLA+
• Has both simulation mode and model
checking mode
– We run simulations before a complete
model checking
• Terminate w/o violation: robustness
proved
• Produce violation sequence: attack
trace
25<#>
Model Checking Challenges
• Challenge: State space explosions
• Our Solutions
– Combine similar states without loss of
functionality into one state
– Identify symmetry in system, which will
treat the different states as one common
state.
– Replace some random numbers with
constants having some additional properties
to simulate the effects of randomness
26<#>
Outline
•
•
•
•
•
Motivation
Our approach
Background on TLA+
General methods and challenges
Results on WiMAX initial ranging
and authentication
• Conclusions and future work
27<#>
PKMv2 Authentication Process
• SS and BS mutually
authenticate each other and
exchange keys for data
encryption
• PKMv2 is directed by two state
machines in the SS
– Authentication State Machine
– TEK State Machine
• PKMv2 employs a SATEK
three-way handshake for the
BS and the SS to exchange
security capabilities
BS
SS/MS
uest
q
e
R
h
t
u
A
Auth Respons
e
Auth ACK
SATEK Challe
nge
quest
e
R
K
E
T
SA
SATEK Respo
nse
est
Ke y R e q u
Key Response
28<#>
Authentication – TLA Model
• Each key has a life time, so the SS needs to get
authorized from time to time
– SS will reach the “Authorized” state infinite times
[]<>(SSstate =”Authorized”)
• TLC encounters space explosion problem
– We restrict the SS to reach “Authorized” state
at most a given # of times.
• With our attacker model, TLC model checking
completed w/o violation
• Hence, authentication process is resistant to any
attempt under the given attacker model
29<#>