Transcript ppt
Discovery and Traversal of Security Gateways Alwyn E. Goodloe University of Pennsylvania Contessa NS Protocol eXchange June 10, 2005 History of Routing Protocols In early days of ARPANet Few nodes Routing tables manually configured at each node by local system admin Centralized Management an Alternative Network manager knows topology and handles everything Tools can help, but still difficult Drawbacks Managers must know topology Managers control who gets to play Can not just go and add or delete a node Hard to see how the Internet would have grown to present size had either of these schemes been adopted. Dynamic Routing Protocols Routing tables are updated as part of protocol Adapts to changing topology and growth Theory Convergence in the face of changes Correctness Efficiency of underlying protocols Security Gateways Located at cutpoints in the network Possess an inside and an outside Nodes on the inside constitute its domain Gateways control what traffic can enter and leave a domain Single Gateway r1 g a c r2 r3 b Network Network as Graph Gateway Hierarchy A A’ D’ D Traversing Gateways High-level policies at the gateways determine which users can communicate with members of its domain To enforce policies, gateways authenticate packets using cryptographic tunnels Security Associations (IPsec) Packet filters determine which packets go in which association Industrial Practice Gateways are usually configured using command line interfaces Moving to centralized management Tool support: Solsoft Policy server Drawbacks same as for routers Inflexible in the face of changing topology Want protocols to dynamically find gateways and set up associations Set Up Protocol Requirements Discover gateways along path Send out distinguished control packets Negotiate trust relationship based on high-level policy Set up associations using some key-exchange protocol (IKE, JFK) Install packet filters (low-level policies) on the gateways that are derived from/compatible with high-level policies Discovery protocols are a special class of signaling protocol Do People Really Want This Cisco’s Tunnel Endpoint Discovery (TED) Protocol performs discovery Limited. Assumes two gateways. Built into high-end security gateways Indicates industrial demand IETF’s IP Security Policy (IPSP) group Charter says they will develop a discovery protocol Need For Theory We have designed several protocols for setting up collections of IPsec tunnels Sectrace, L3A (WITS 05) Each had subtle flaws that were uncovered by formal analysis Want a formalism and theory for developing such signaling protocols Like SPI-Calculus and MSR for crypto protocols Tunnel Calculus Key-Exchange as abstract building-block Not concerned with the cryptography Terminates with associations and policies properly set up Captures essential details of the network Contrasts with process algebras that abstract away from network Built in layers Layers Discovery Establishment Trust Negotiation Security Processing Packet Routing Example a g b Establishment Authenticate Negotiate Discovery Discovery Negotiation Establishment Authenticate Establishment Encryption Establishment Layer A B Req(spi-a, request) SADB AB SPDB Rep(spi-a, spi-b, request) SADB AB SPDB SADB BA SPDB SADB BA SPDB Trust Negotiation When discovery packet destined for node B arrives at a gateway G, how does G know if it should allow the set up The initiator know that B is inside of G’s domain These questions need to be settled by high-level policy This must be known before establishment begins Trust Management Need to discover, access, process high level policy Work in progress Related works Security Policy Protocol (SSP) IETF IPSP SPKI/SDSI PolicyMaker/KeyNote QCM/SD3 …. Borrow ideas and abstract away details Security Processing Layer Abstraction of IPsec Security Associations (SA) – Define cryptographic transforms Abstract away the cryptography Tunnel mode Packet P(a,b,y) in association cd:I P(c,d,S(I,P(a,b,y)) Association Database (SADB) Security Processing Layer Contd Packet filters called security policies direct traffic into SAs Security Policy Database (SPDB) SPDB-IN and SPDB-Out Must model the processing of packets! Headers added and removed in accordance with policy Each packet that enters the system must undergo processing Outgoing packets processed before sent down to routing layer IPsec example i1 i2 G A B i3 P(A,B,y) AB:[(AB)(AG)] AB:[(AG)] P(A,B,S(i3,P(A,B,y))) P(A,G,S(i1,P(A,B,S(i3,P(A,B,y))))) AB:[(GB)] AB:[(AB)(GB)] P(A,B,y) P(G,B,S(i2,P(A,B,S(i3,P(A,B,y)) Routing Layer Network topology induced by forwarding tables Routers only route Packet p arrives @ r. Lookup next hop in table. Send packet to next hop Secure nodes do IPsec processing All packets that arrive are sent up to be processed by security layer Formalism Based on multiset rewriting and equational logic Very basic logic Control flow must be explicit Each rule may execute concurrently unless constrained State must be explicitly passed among rules MSR’s L-Predicates Our resumption terms <…..> Routing Grammar Routing Layer Rules Security Processing Grammar Nesting a packet Output Rule Safety/Liveness Properties Safety:If a tunnel if formed, then a proper set of credentials exist Liveness: Given some global policy, the two parties should be able to communicate assuming everything is in the right place Still working on formalizing these Future Work Dissertation will flush out the details of each layer Executable models in Maude Proofs of properties Work on the theorems Trust negotiation layer Contessa NS People Carl A. Gunter Mark-Oliver Stehr Alwyn Goodloe Matthew Jacobs Gaurav Shah Michael McDougall Gual Agha Michael Greenwald Sanjeev Khanna Jose Meseguer Koushik Sen Prasanna Thati