Transcript Formal Methods for Intrusion Detection - MSU CSE

Formal Methods for Intrusion Detection
Presented by Brian Kellogg
CSE 914: Formal Methods for Software Development
Michigan State University
December 11th, 2002
Purpose and Method




Find intrusion detection methods that utilize
formal methods
Analyze strengths and weaknesses of each
method
Compare the methods and see if they can be
combined in such a way to improve one
another
Found three research papers on intrusion
detection that used formal methods for
different purposes
Intrusion Detection Quickie


The SANS institute defines intrusion detection as “the art of
detecting inappropriate, incorrect, or anomalous activity”
Two types:



Host-based: detects intrusions on a specific host
Network-based: detects intrusions on a network
Two (main) methods:

Knowledge-based




Determine vulnerabilities and attempts to detect vulnerabilities
Low false alarm rate
Attacks not specified are not detected
Behavior-based



Determines normal system activity
High false alarm rate
Able to detect many intrusions (even ones not previously known)
Intrusion Detection Continued

Why use intrusion detection, why not just prevent the
attacks?



Firewalls can prevent many attacks, but have no power over
the internal network
Certain network activities that have legitimate uses can also
signify an attack (e.g. port scans)
What should an intrusion system do when it detects
an attack?



Responses range from e-mails to reconfiguring the network
Just because the system detects an intrusion, may be
legitimate
Severe (or even simple) responses can be utilized by
attackers to create new attacks
Yasinsac Paper (Motivation)




“An Environment for Security Protocol
Intrusion Detection”
Traditional methods of protocol analysis not
fool proof or complete
Different protocols running concurrently can
create new exploits
Shift to “tunneling” paradigm in networks


Sensitive data sent over same links as nonsensitive data
Cryptographic techniques must be applied at
higher layer (application layer)
Yasinsac Paper (Method)


Take knowledge gained from formal analysis
of security protocols and make them in to
intrusion signatures
Uses both knowledge-based and behaviorbased intrusion detection



Knowledge-based: signature an ordering of
activity traces
Behavior-based: surveys taxonomies and protocol
principles to determine profile strategies and
behavior recognition
State-based attack recognition
Yasinsac Paper (Method)
IKE protocol:



AB: HDR1, SAA, KEA, NA, A
BA: HDR2, SAB, KEB, NB, B, {prf(KAB, (KEB, KEA, KEB, KEA, B))}KB
Exploit:




AB: HDR1, SAA, KEA, NA, A
IB: HDR1, SAA, KEA, NA, I
BI: HDR2, SAB, KEB, NB, B, {prf(KAB, (KEB, KEA, KEB, KEA, B))}KB
Yasinsac Paper (Architecture)

Central monitor, each principal communicates with
monitor through secure channel
Principal A
Knowledge
base
Network
Principal C (Intruder)
Monitor
Principal B
Pouzol Paper

Motivation:




Algorithm that detects attacks in a declarative IDS is a black
box
Partial instances of attacks can choke an IDS
Wants to give more power to security officer to choose
which attack instances are important
Method:



Formally specify intrusion signatures and detection rules
Create a lattice used to define equivalence classes that
defines a signature
Choose an equivalence relation that can reduce the number
of instances reported
Pouzol Lattice
Т
U1U2T3: In this equivalence
class, every instance that has a
unique pair of users and a third
time stamp will be reported.
This is an example of a good
choice. This class will resist the
choking attack, and will report
all completed instances of an
attack. Having the final
timestamp means that the last
part of the attack occurred,
thus only a completed attack is
being reported.
{U1, U2, T1, T2, T3}
{U1, U2, T3}
{U2, T3}
{U1, U2}
{U1}
{U2}
{}
{T3}
NetSTAT Paper (Motivation)




“NetSTAT: A Network-based Intrusion
Detection Approach”
Motivated by the increase of network reliance
and attacks
Host-based intrusion detection fails to detect
these attacks
Firewalls do an excellent job of preventing
external intrusions, but internal threats are
left unchecked
NetSTAT Paper (Method)


NetSTAT is a network-based intrusion detection
system
Wants to solve:






Networks generate large amounts of data
Some attacks occur only in a certain portion of a network
Too much communication between IDS components can clog
a network
Networks can grow very large
Able to work with host-based methods
Four components:




A network fact base
A state transition scenario database
Many general purpose probes
An analyzer
NetSTAT Paper (Method)

Network fact base





Stand alone application that describes network
topology and network services
Contains interfaces, hosts, and links
Represented as a hypergraph
Interfaces are nodes, hosts and links are edges
This is a formal model, adds benefits:



Well defined semantics
Supports reasoning and automation
Topological properties described in expressive way
NetSTAT Paper (Method)

State transition scenario database



Contains signatures of attacks
Attacks are sequences of states (snapshots)
States are described by assertions that return Boolean
values


Example: i.link.type==”ATM”;
Probes


Sensors that are strategically placed in a network but are
also full blown intrusion detection system
Made up of:



Filter that only collects data of interest
Inference engine contains attack scenarios
Decision engine issues response according to information
collected in the inference engine, or reports info to the analyzer
NetSTAT Paper (Method)

Analyzer




Takes as input a network fact base and a state
transition scenario
Tells security officer where probes are needed
Sets up the probes
It determines:



Events to be monitored,
The network topology
State information it requires to verify state assertions
NetSTAT Paper (Architecture)
Network Fact
Base
probe
Scenario
Database
probe
Analyzer
Gateway
Internet
Router
probe
Security Officer
Analysis: Yacinsac

Advantages




Able to find flaws in protocols that get past formal analysis
Able to detect flaws in concurrently running protocols
Architecture is cheap and versatile
Disadvantages



How do you choose the sources for signatures?
How many signatures is too many?
Architecture



Every single principal required to run software to report to
central authority
Intruders can disable software
Network attacks can still occur unnoticed
Analysis: Pouzol

Advantages



Allows security officer to specify an equivalence
relation to prevent choking attacks on the IDS
Formal specification of signatures and detection
rules proven sound and complete
Disadvantages



Has not been implemented in any IDS
Complexity of algorithm may create choking
attacks
Equivalence relations can be dangerous if
configured incorrectly
Analysis: NetSTAT

Advantages:




Can detect intrusions on multiple sub-networks
and total network
Scalable to large networks
Formal methods allow expressiveness and
automation
Disadvantages


Not yet fully implemented
Analyzer does ad hoc configuring of probes
Combination


Pouzol’s technique to prevent choking
attacks can be used by Yasinsac (and
NetStat)
Two full intrusion detection architecture


Which one is best? NetSTAT!
Yasinsac’s knowledge base can be used
by NetSTAT (and all IDS)
Conclusion




Formal methods and intrusion detection can
work together to make networks more secure
There are many different areas where formal
methods can be applied
Neither is a silver bullet to network security
Attackers are always evolving new techniques
to attack a network, and as security experts,
so must we
Main References



A. Yasinsac. An Environment for Security Protocol
Intrusion Detection. Special edition of the Journal of
Computer Security, 2001
J. Pouzol and M. Ducassé. Formal Specification of
Intrusion Signatures and Detection Rules. 15th IEEE
Computer Security Foundations Workshop, June 2002
G. Vigna and R. Kemmerer. NetSTAT: A Networkbased Intrusion Detection Approach. Computer
Security Applications Conference, 1998