Transcript ss2

Network Security Architectures
Part 2 Formalization and Testing
Summer School on Software Security
Theory to Practice
Carl A. Gunter
University of Pennsylvania
Summer 2004
End-to-End Security and
Mandatory Tunnels
Client
Security
Gateway
First hop
encryption
Server
Second hop
encryption
Examples: WTLS, cdma2000, L2TP, Palm VII
Goals for a Security Protocol
1.
2.
3.
If client C receives content from
server S, then this is authorized by
the policies of S and all of the
security gateways between C and S
If C receives content from S, then
this content is encrypted and
authenticated from end-to-end
between C and S
Simple setup and low-overhead
enforcement
IPSec Strategy
Encapsulation


AH headers for authentication and
authorization of traversal. Use tunnel mode.
ESP header for authentication and
confidentiality of end-to-end communication.
Use transport mode.
IP
AH
IP
AH
IP
ESP
TCP
20
24
20
24
20
8
20
payload
ESP
16
Drawbacks to IPSec Solution




Requires complex configuration using
nested tunnels to establish security
associations between client, gateways
and server
Encrypts the TCP header limiting use of
VJC and other similar compression
techniques
Setup is relatively costly as session
keys must be exchanged
Nested headers introduce significant
bandwidth overhead
IP SEC Header Overheads for 576
Byte Packets
Security overhead
=
(4.50 + 7.61t)
(60.8 – 5.25t)
#
SGs
TCP
TCP +
VJC
0
7%
17%
1
22%
31%
2
39%
49%
3
61%
70%
4
88%
97%
Evidence of Problems
Experimental: FreeBSD IPSec showed
an overhead of 46% with two gateways
 Standards activity: secure L2TP
overheads were so severe a standard
was developed specifically to reduce
them. Default security with one
gatekeeper yielded this:

IP
ESP UDP L2TP PPP
IP
ESP TCP
Payload
A Goodloe, C Gunter, T Hiller, P McCann, M McDougall
ESP ESP
Case Study: Layer 3 Accounting
(L3A)
Motivating problem from wireless
security
 Solution by composing secure tunnels
 Maude model
 Problems
 Future work

A Goodloe, C Gunter, MO Stehr
Wireless Security

Why is wireless security any different
from wired security?
 Resource
constraints
 Increased risk to confidentiality
 Value of the network link
Wireless Security Efforts

Layer 1 (Physical)
 Spread

spectrum
Layer 2 (Link)
 802.11x
– 802.11(b) WEP, 802.11(g)
 CDMA 2000
 GPRS
802.11/WEP
SSL
WEP
Router/NAT
Network Layer Wireless Security


We propose that security be addressed at
the network layer
Advantages




Independent of underlying link layer
Overcomes many of the problems of layer 2
solutions
Leverages extensive experience, s/w, and h/w
support from Ipsec for VPNs
Disadvantage

Need set up protocols
Protocols for Tunnel Composition
We have been investigating protocols
for composing IPSec security tunnels
 Given a scenario we ask:

 What
tunnels should we establish?
 What properties should these tunnels
have?

Develop protocols that compose these
tunnels into a satisfactory solution
 Lots
of messy details to consider in order
to get the composition to work
Toward Layer 3 Security



Suppose we have three parties: client, server,
network access server (NAS)
The client wishes to securely access the
server
We will assume that the client has a
relationship with the NAS and the server,
but the NAS does not have a relationship to
the server

The Client will have to authenticate itself to both
the NAS and the server
Network Layer Wireless Security
Problem
Similar problem as before
 The NAS does not protect the client
from attacking incoming traffic
 Being forced to pay for service you
never used is worse than denial of
service

How About a Firewall?
Why Not a Firewall
A stateful firewall can be programmed
to allow only traffic from the address
to which a connection has been made
 The firewall can not see the contents of
the Ipsec traffic and cannot guarantee
origin of any traffic.

L3A Protocol Principles
The user’s traffic should travel in DOS
resistant IPSec tunnels
 These IPSec tunnels should be set up
using DOS resistant protocols
 The NAS should ensure that when the
accounting system logs traffic as being
from a user it is actually from that
user: viz. it must authenticate incoming
traffic

L3A Protocol Components
L3A protocol sets up three bidirectional
tunnels
 SIKE Key Exchange protocol (X509 +
DoS protection)

 Very
simple: does not use two party key
generation
 No guarantee of perfect forward secrecy.
 Assumes existence of public key
infrastructure
L3A Architecture
Methodology
An English language description
resembling an IETF RFC is produced
 A formal specification is written in
Maude
 Systems are modeled using membership
equational logic and rewriting logic
 Symbolic simulation has been our main
debugging aid
 We feel the design is now relatively
stable

IPSec SA & SPD

Security Associations define a set of
cryptographic transformations that are
applied to each packet.
 Authentication
 SAD

w/ HMAC. Encrypt w/3DES.
Security Policies filter traffic and
define what SAs apply to what traffic.
 CS
 SPD
goes into tunnels CS and CN
SIKE
A
B
rA, SPI(n,0)
rA,rB, SPI(n,m), certB, cookieA
Where CookieA = VersionSecret | Hash([rA,rB,IPA, SPI(n,m)],Secret)
certA,cookieA, DA, Ps(a,DA)
Where DA = [rA, IPB, SPI(n,m)]
Update SADB/SPD AB
DB, Ps(b,DB)
Where DB = [rB, IPA, rA, SPI(n,m), Pe(A, K)]
Update SADB/SPD AB
Update SADB/SPD BA
Update SADB/SPD BA
L3A Protocol Overview
Client
Server
NAS
SPD CS:(CN)
Req(cred)
SPD C->S:(C->N)
SPD SC:(SN)
Ack(cred)
SPD:SC:(SN)
Fin
Abstractions


Getting the right level of abstraction
Modeled the various components and layers



IP, IPSec, L3A, …..
We found that we didn’t need to model details
of IPSec authentication and encryption since
we are interested in the set up of tunnels
We discovered that our model of IP
send/receive was too abstract.

Introduced messy concurrency problems
Overview of Module Interaction
L3A
SIKE
setkey
PKI
Ipsec
IP
SIKE Test
Setkey
L3A Test
Concrete
L3A Test
Abstract
L3A
L3A
Abstract
PKI
SIKE
Security Policy
Ipsec
Security Assoc
IP
Routing Table
State
IP Message
Message
Modeling Uncovered Problems
Problems arose from interactions among
the components
 Numerous iterations were required to
resolve problems resulting from when
the Ipsec databases are updated
 Maude
here

search feature was of great help
When things are not done right packets
can slip into partially set up tunnels
We Didn’t Model
Timers
 Lost Messages
 Periodic updates to the secret used to
generate the cookie
 Fragmentation

 Can

be the source of DOS attacks
UDP layer: Ports not mentioned at all in
the model
Implementation
Under development at this moment
 Platform. X86 running FreeBSD w/
IPSec.

C
with Open SSL crypto libraries
 Radius server to be used for accounting
Will demonstrate that our protocol can
be implemented using available
technology
 Hope to get some useful benchmarks

A Goodloe, C Gunter, M Jacobs, G Shah
Future Work
Continue work on verifying composition
of security tunnels
 We are currently thinking about attacks
 Do such compositions introduce new
vulnerabilities?
 Add the capability to reuse tunnels

 Seemed
easy at first, but may require
some major restructuring of the design

Figure out what theorems need to be
proven
Simulators

Maude “logical
simulations”





Exhaustive breath
first search.
Model checking.
Must abstract things
like packet size.
Not good with
timers.
Not really useful for
performance
modeling.

OPNET, NS-2
discrete event
simulation.




Good at modeling
details (time, etc).
Often used to
estimate network
performance
Not good at finding
the extreme cases
Probably wouldn’t
have found several of
our concurrency
problems
Summary
Complex problems arise when composing
high-level security protocols such as
Ipsec tunnels
 Wireless networks pose some new
challenges but can leverage general
solutions
 Symbolic simulation can provide a
powerful tool for the design of network
security protocols
