Reasoning about VPN Integrity
Tim Griffin *
Intel Research Lab
Virtual Private Networks (VPNs) should provide
users with the isolation and security associated with private
networks, but at a lower cost made possible by the use of
a shared infrastructure. One type of VPN currently enjoying wide
deployment is described in RFC 2547. From the customer's point of view,
RFC 2547 VPNs represent an outsourcing of routing to Internet Service
Providers (ISPs). From the ISP's perspective, this represents (at
long last) a chance to "add value" to IP services. However, it also
represents a network configuration nightmare. I'll talk about one
attempt to tame the complexity of these VPNs using network invariants
- maintained by bits of implementation - that can be composed to
reason about the global correctness of VPN various
implementations. The approach quickly reveals some rather nasty
problems with RFC 2547 VPNs. I'll mention these and a few possible
fixes.
* Dr Tim Griffin has recently joined the Intel Research Laboratory at
Cambridge. He previously worked at AT&T research investigating
network management. He also has research interests in databases and
programming languages.
