Transcript motorola-review-May0.. - Computer Science Division

Automatic Vulnerability Analysis
and Intrusion Mitigation
Systems for WiMAX Networks
Yan Chen, Hai Zhou
Motorola Liaisons
Northwestern Lab for Internet Gregory W. Cox, Z. Judy Fu,
and Security Technology (LIST)
Philip R. Roberts
Dept. of Electrical Engineering
Motorola Labs
and Computer Science
Northwestern University
http://list.cs.northwestern.edu
The Spread of Sapphire/Slammer Worms
Outline
•
•
•
•
Threat Landscape and Motivation
Our approach
Accomplishment
Ongoing Work
The Current Threat Landscape and
Countermeasures of WiMAX Networks
• WiMAX: next wireless phenomenon
– Predicted multi-billion dollar industry
• WiMAX faces both Internet attacks and wireless
network attacks
– E.g., 6 new viruses, including Cabir and Skulls, with 30
variants targeting mobile devices
• Goal of this project: secure WiMAX networks
• Big security risks for WiMAX networks
– No formal analysis about WiMAX security vulnerabilities
– No WiMAX intrusion detection/mitigation
product/research
Existing WLAN Security Technology
Insufficient for WiMAX Networks
• Cryptography and authentication cannot prevent
attacks from penetrating WiMAX networks
– Viruses, worms, DoS attacks, etc.
• 802.16 IDS development can potentially lead to
critical gain in market share
– All major WLAN vendors integrated IDS into products
• Limitations of existing IDSes (including WIDS)
– Mostly host-based, and not scalable to high-speed
networks
– Mostly simple signature based, cannot deal with unknown
attacks, polymorphic worms
– Mostly ignore dynamics and mobility of wireless networks
Our Approach
• Adaptive Intrusion Detection and Mitigation for
WiMAX Networks (WAIDM)
– Focus of the first year
• Vulnerability analysis of 802.16e specs and WiMAX
standards
– Systematical and automatic searching through formal
methods.
– First specify the specs and potential capabilities of
attackers in a formal language TLA+ (the Temporal Logic
of Actions)
– Then model check for any possible attacks
– The formal analysis can also help guide fixing of the flaws
Deployment of WAIDM
User
s
802.16
BS
802.16
BS
802.16
BS
User
s
Internet
Users
Inter
net
scan
port WAIDM
system
• 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
Switch/
BS controller
Switch/
BS controller
802.16
BS
Users
(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 completed)
Integrated approach for false positive reduction
– Automatic Polymorphic Worm signature generation
(Hamsa)
– Network element fault Diagnostics with Operational
Determinism (ODD)
WAIDM
Architecture
Remote
aggregated
sketch
records
Sent out for
aggregation
Normal flows
Reversible
sketch
monitoring
Streaming
packet
data
Filtering
Local
sketch
records
Sketch based
statistical anomaly
detection (SSAD)
Keys of suspicious flows
Part I
Sketchbased
monitoring
& detection
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
Hamsa Signature Generator
Normal
Traffic Pool
Token
Identification
Core
Signature
Refiner
Signature
Suspicious
Traffic Pool
Token
Extractor
NO
Pool size
too small?
Tokens
Filter
YES
Quit
• Evaluated with real Internet worms and traffic
– Three pseudo polymorphic worm based on real exploits (Code-Red
II, Apache-Knacker and ATPhttpd).
– Two polymorphic engine from Internet (CLET and TAPiON).
Results on Signature Quality
Worms
Code-Red II
CLET
•
Training
FP
Evaluation
FN
Evaluation
FP
Binary
evaluation FP
Signature
0
0
0
0
0
{'.ida?': 1, '%u780': 1, ' HTTP/1.0\r\n': 1, 'GET /': 1, '%u': 2}
0
0.109%
0
0.06236%
{'0\x8b': 1, '\xff\xff\xff': 1,'t\x07\xeb': 1}
0.268%
Single worm with noise
–
–
–
–
•
Training
FN
Suspicious pool size: 100 and 200 samples
Noise ratio: 0%, 10%, 30%, 50%
Noise samples randomly picked from the normal pool
Always get above signature and accuracy
Multiple worms with similar results
Accomplishments
•
Motorola Interactions
–
–
–
•
Patents being filed through Motorola
–
•
The first two components of WAIDM are ready for
field test on Motorola WiMAX networks or testbed
Product teams interested to use as differentiator
(Networks security service director: Randall Martin)
Close collaboration/interaction with Motorola Labs
(Judy Fu, Phil Roberts, Steve Gilbert)
Reverse Hashing for High-speed Network Monitoring:
Algorithms, Evaluation, and Applications.
Students involved
–
–
Three Ph.D. students: Yan Gao, Zhichun Li, & Yao Zhao
One M.S. student: Prasad Narayana
Accomplishments on Publications
• Five conference papers and two journal papers
– Towards Deterministic Overlay Diagnosis, to appear in Proc. of ACM
SIGCOMM 2006 (10%).
– Reversible Sketches: Enabling Monitoring and Analysis over Highspeed Data Streams, to appear in ACM/IEEE Transaction on
Networking.
– A DoS Resilient Flow-level Intrusion Detection Approach for
High-speed Networks, to appear in IEEE International
Conference on Distributed Computing Systems (ICDCS), 2006
(14%).
– Hamsa: Fast Signature Generation for Zero-day Polymorphic
Worms with Provable Attack Resilience, to appear in IEEE
Symposium on Security and Privacy, 2006 (9%).
– Reverse Hashing for High-speed Network Monitoring:
Algorithms, Evaluation, and Applications, Proc. of IEEE
INFOCOM, 2006 (18%).
– IDGraphs: Intrusion Detection and Analysis Using Stream
Compositing, to appear in IEEE Computer Graphics &
Applications, special issue on Visualization for Cyber Security,
2006.
» An earlier version also in Proc. of the IEEE Workshop on
Visualization for Computer Security (VizSEC), 2005
Ongoing Work
• 802.16 Vulnerability Analysis Through Formal
Methods (poster presentation this afternoon)
– Many control messages are not (or cannot be)
authenticated or encrypted
– Use formal verification methods to automatically
search for vulnerabilities in 802.16 specs
– Completeness and correctness
• Semantics Aided Signature Generation for Zeroday Polymorphic Worms
– Some stealthy worms may not have any content
invariant
– Incorporate semantic information for more accurate
detection
802.16 Vulnerability Analysis
Through Formal Methods
• TLA: a logic designed for specifying and reasoning
about concurrent systems.
– TLA+: a complete spec language based on TLA
• First translate the natural language spec into a
TLA+ spec, sys, and formulate security as prop
• Normal security as sys → prop can be checked
automatically by model checker TLC
• A generic attacker will be specified as Attk
• Vulnerability can be discovered by checking
Attk  sys → prop, also automatically by TLC
Case Studies
• First step, verify the initial ranging stages
– Specify the protocol in 19-page TLA+ language
– Assume certain capabilities of attackers
» Eavesdrop and store messages
» Corrupt messages on the channel by causing collisions
» Replay old / Inject spoofed messages
– Prove that ranging protocol is in general secure except
one DoS attack
DL Subframe
UL Subframe
Contention-based Initial
Ranging slots
Attacker fills all slots, making its requests collide with requests from other
SS, thereby denying all new SS a chance to complete ranging
Case Studies (II)
• Verify the authentication protocol
– No real attacks found
• Future work
– Consider other attack capabilities
– Verify other protocols of 802.16
TEK invalid/
Key Request
Operational
Key Reply
TEK invalid/
Key Request
Op Wait
Timeout/
Key Request
Rekey Wait
Auth Pend
Op Reauth
Wait
Conclusions
• Adaptive Intrusion Detection and Mitigation for
WiMAX Networks (WAIDM)
• Vulnerability analysis of 802.16e specs and WiMAX
standards
Thank You !
Formal Vulnerability Analysis
Research Challenges
• Use abstraction to model infinite state
system in finite states for model checking
(state explosion)
– Random nonces -> constant
– Different processing orders
• Model generic attackers with appropriate
capabilities
– Need to be general and realistic