/* ======================================================================== A COMPOSITIONAL NETWORK MODEL IN ALLOY: FORWARDING AND REACHABILITY The purpose of this model is to study routing and forwarding, and their effects on reachability. ======================================================================== */ /* ------------------------------------------------------------------------ BASIC TYPES ------------------------------------------------------------------------ */ sig Node, Bucket { } one sig Self { } sig Link { transmitter, acquirer: Node } sig Header { source, destination: Node, bucket: Bucket } fact Headers_are_records { all h0, h1: Header | (h0.source = h1.source && h0.destination = h1.destination && h0.bucket = h1.bucket) => h0 = h1 } /* ------------------------------------------------------------------------ NETWORK STATE Functional Semantics: If a packet with header h is acquired at node n on link i and... ...there is a single forwarding tuple (n->h->i->o), and o has not failed, then forward the packet on link o; ...there are two or more such tuples, then choose one and forward the message on its link o; ...there is no such tuple, then do not forward the message. Similar rules apply if the packet is sent by node n and the tuple pattern is (n->h->Self->o). ------------------------------------------------------------------------ */ sig NetworkState { -- necessary state nodes: set Node, links: set Link, failed: set links, forwarding: Header -> (links + Self) -> links, -- derived state allHops: Header -> (links + Self) -> links, reaches: Header -> nodes -> nodes, receives: Header -> nodes -> nodes, -- extra state for expressing requirements positiveReach: nodes -> nodes, negativeReach: nodes -> nodes, cluster: set nodes } { -- The endpoints of a link must be distinct member nodes. all k: links | (k.transmitter + k.acquirer) in nodes && k.transmitter != k.acquirer -- Forwarding is performed by a node. all k0, k1: links | (k0 -> k1) in Header.forwarding => (some n: nodes | n = k0.acquirer && n = k1.transmitter ) -- Derivation allHops. all h: Header | h.allHops = ^(h.(forwarding:>(links-failed))) -- Derivation of reaches. If (h -> n0 -> n1) is in reaches, then if n0 -- sends a packet with header h, it can reach n1 (and will reach n1, if -- routing is deterministic). reaches = { h: Header, n0, n1: nodes | some k0, k1: links | (h -> Self -> k0) in forwarding && k0.transmitter = n0 && (h -> Self -> k1) in allHops && k1.acquirer = n1 } -- Derivation of receives. If (h -> n0 -> n1) is in receives, then if n0 -- sends a packet with header h, it will be received at n1. receives = { h: Header, n0, n1: nodes | (h -> n0 -> n1) in reaches && h.destination = n1 } -- Positive and negative reachability requirements do not overlap. no (positiveReach & negativeReach) } /* ------------------------------------------------------------------------ POSSIBLE NETWORK PROPERTIES The hash field in headers allows us to model multipath routing. With multipath routing, it is best to assume Deterministic_routing and Nodes_ absorb_messages_destined_for_them. It would take more work and state to model multipath consistent path length or cost, but the idea is the same. Cluster locality could be extended to allow multiple clusters. ------------------------------------------------------------------------ */ pred Deterministic_routing [w: NetworkState] { all h: Header, k: (w.links + Self) | lone k.(h.(w.forwarding)) } pred Nodes_absorb_messages_destined_for_them [w: NetworkState] { all h: Header, k: w.links, n: w.nodes | h.destination = n && k.transmitter = n => no h.(w.forwarding).k } pred Headers_are_sent_authentic [w: NetworkState] { all h: Header, k: w.links, n: w.nodes | (h -> Self -> k) in (w.forwarding) && k.transmitter = n => h.source = n } pred No_routing_loops [w: NetworkState] { all h: Header | no k: w.links | (k -> k) in h.(w.allHops) } pred Positive_reach_requirements_satisfied [w: NetworkState] { all n0, n1: w.nodes | (n0 -> n1) in w.positiveReach => (n0 -> n1) in Header.(w.reaches) } pred Negative_reach_requirements_satisfied [w: NetworkState] { all n0, n1: w.nodes | (n0 -> n1) in w.negativeReach => (n0 -> n1) ! in Header.(w.reaches) } pred Multipath_consistent_reach [w: NetworkState] { all h0, h1: Header | ( h0.source = h1.source && h0.destination = h1.destination && h0.bucket != h1.bucket ) => h0.(w.reaches) = h1.(w.reaches) } pred Multipath_consistent_receives [w: NetworkState] { all h0, h1: Header | ( h0.source = h1.source && h0.destination = h1.destination && h0.bucket != h1.bucket ) => h0.(w.receives) = h1.(w.receives) } pred Intra_cluster_locality [w: NetworkState] { all h: Header, n0, n1: w.nodes | (n0 + n1) in w.cluster && (h -> n0 -> n1) in w.receives => n0.(h.(w.reaches)) in w.cluster } pred Receives_is_symmetric [w: NetworkState] { Header.(w.receives) = ~ (Header.(w.receives)) } pred Good_header_is_reversible [w: NetworkState] { all h: Header, n0, n1: w.nodes | (h -> n0 -> n1) in w.receives => some h': Header | ( h'.source = h.destination && h'.destination = h.source && (h' -> n1 -> n0) in w.receives ) } /* ------------------------------------------------------------------------ VALIDATION AND VERIFICATION Even if the theorems seem trivial, they help to validate the model. ------------------------------------------------------------------------ */ pred Good_network_exists [w: NetworkState] { some w.receives && some w.cluster some w.positiveReach && some w.negativeReach Deterministic_routing [w] Nodes_absorb_messages_destined_for_them [w] Headers_are_sent_authentic [w] No_routing_loops [w] Positive_reach_requirements_satisfied [w] Negative_reach_requirements_satisfied [w] Multipath_consistent_reach [w] Multipath_consistent_receives [w] Intra_cluster_locality [w] Good_header_is_reversible [w] Receives_is_symmetric [w] } run Good_network_exists for 1 but 4 Node, 4 Link, 2 Header, 2 Bucket assert Multipath_consistent_reach_implies_consistent_receives { all w: NetworkState | Multipath_consistent_reach [w] => Multipath_consistent_receives [w] } check Multipath_consistent_reach_implies_consistent_receives for 1 but 5 Node, 9 Link, 5 Header, 2 Bucket -- OK pred Multipath_consistent_receives_not_consistent_reach [w: NetworkState] { Multipath_consistent_receives [w] && ! Multipath_consistent_reach [w] } run Multipath_consistent_receives_not_consistent_reach for 1 but 3 Node, 3 Link, 2 Header, 2 Bucket -- OK assert Reversible_headers_imply_symmetric_receives { all w: NetworkState | Good_header_is_reversible [w] => Receives_is_symmetric [w] } check Reversible_headers_imply_symmetric_receives for 1 but 5 Node, 9 Link, 5 Header, 2 Bucket -- OK pred Symmetric_receives_not_reversible_headers [w: NetworkState] { Receives_is_symmetric [w] && ! Good_header_is_reversible [w] } run Symmetric_receives_not_reversible_headers for 1 but 3 Node, 3 Link, 2 Header, 2 Bucket -- OK -- instances show that a packet can be received with a spoofed source -- name, even when it would be blocked with an authentic source name /* ------------------------------------------------------------------------ NetworkState, Node, Link, Header, Bucket ------------------------------------------------------------------------ */