An automatic correctness and safety checker for network-wide forwarding policies VERMÓNT – VERifying MONiTor A watchdog for your network Eugene Chemeritskiy Victor Altukhov Vladislav Podymov Vladimir Zakharov Applied Research Center for Computer Networks Lomonosov Moscow State University Packet Forwarding Policy What is the intended behavior of a network? • • • • • • • No external flow reaches office mail server Outgoing flows have to pass a DPI server Any pair of hosts in office is connected Departments are isolated from each other Each route includes at most five hops No packet loops (reaches its original state) Host A is unable to connect host B until host B has tried to connect host A before How to ensure your network is configured to work in compliance with your expectation? VERMÓNT – VERifying MONiTor Checking a static network configuration Prerequisites Express your intentions to the behavior of a certain network with our PFP specification language Single-time work Benefits VERMONT checks the consistency of network configuration with formally specified invariants of network-wide Packet Forwarding Policies (PFPs). • Prevent network to violate any policies of network safety • Reveal the problems in your configuration • Provide sensible information about this problems Provide network topology and configuration files for your switches/routers This task might be automated VERMONT core operation principles Requirements to network behavior Network infrastructure Formal policy specifications Topology FlowTables Network model builder BDD relations Policy A holds Specification parser Abstract Syntax Tree Verification engine Policy B violated by packet set P Mathematical model of SDN • Space of packet headers: ℋ = 0,1 ℎ = 〈ℎ1 , ℎ2 , … , ℎ𝑁𝑁 〉 𝑙𝑙 • Space of port numbers: 𝒫𝒫 = 0,1 𝑝𝑝 = 〈𝑝𝑝1 , 𝑝𝑝2 , … , 𝑝𝑝𝑙𝑙 〉 • Space of switch numbers: 𝒲𝒲 = 0,1 𝑤𝑤 = 〈𝑤𝑤1 , 𝑤𝑤2 , … , 𝑤𝑤𝑘𝑘 〉 • Packet state space: 𝒮𝒮 = ℋ × 𝒫𝒫 × 𝒲𝒲 = 0,1 N 𝑘𝑘 𝑁𝑁+𝑙𝑙+𝑘𝑘 • Packet processing rules, network devices and links define two-argument relations over the space 𝒮𝒮: 𝑅𝑅: 𝒮𝒮 × 𝒮𝒮 → 0,1 A formal model of SDN {Data Plane abstraction} Data plane behavior may be completely specified by a single hop forwarding relation 𝑅𝑅𝑛𝑛𝑛𝑛𝑛𝑛 : 𝒮𝒮 × 𝒮𝒮 → 0,1 constructed as a composition of smaller relations State 1: Header h1 Port #1 Switch #1 h2 h1 A State 3: Header h3 Port #1 Switch #3 State 2: Header h2 Port #1 Switch #2 h3 h4 B State 4: Header h4 Port #2 Switch #3 Пример политики маршрутизации: запрет циклов по состоянию пакета aux: lead_to_cycle(x) := In(x) and Exist[y: R_tc(x,y) and Exist[z: R_tc(y,z) and y == z ] ]; x z y main: no_state_cycles() := Forall[x: not lead_to_cycle(x)]; 90 Mb router configuration files Fat Tree topology with 16 routers 757000 rules 48 tables Stanford University Backbone Network Stanford network verification Verdict Time spend (ms) - 3043.687 Packet cycles YES 166.191 Black holes NO 174.845 Routes <= 3 hops NO 293.522 Routes <= 4 hops YES 736.015 Rule insertion seq. / paral. - 100 / 0.3* Rule removal seq. / paral. - 70 / 1* Activity Initial model construction VERMÓNT – VERifying MONiTor Checking network configuration in dynamic Prerequisites Express your intentions to the behavior of a certain network with our PFP specification language Single-time work Benefits VERMONT checks the compliance of network configurations resulted by the application of a given sequenceof commands to an arbitrary set of packet forwarding policies • Prevent network to violate any policies of network safety • Reveal the problems in your configuration • Detect problems in application compatibility Интегрировать VERMONT в вашу программноконфигурируемую сеть Запустить несколько программ VERMONT deployment SDN controller switch messages controller commands Proxy Server switch messages controller commands OpenFlow Switches Initial network state Feeder Is command safe? Verifier verdict: PFP violated - block the command PFP holds - apply it to the network Verifier PFP specification VERMONT anticipates loading of the switches after a certain command of the controller is applied and blocks it, if it results into violation of the given PFP specifications A place of VERMONT Currently there exists several ways to ensure correct and safe network operation: 1. Apply formal method to controller application in the same manner it is applied to programs 2. Write controller application in a specialized language that finds all the mistakes during the compilation phase 3. Verify the application during its operation and detect policy violations in dynamic Other tool with the same approach Model constructing time (ms) Model modification time (ms) Policy specification language OpenFlow support VERMONT 3100 100 - 600 FO[TC] full NetPlumber 37000 2 - 1000 CTL partial >4000 68 - 100 A fixed set of properties minimal 1000 0.1 A fixed set of properties minimal 400000 ??? A fixed set of properties none 1200000 350 - 67000 CTL full Tool 2013 Stanford University 2013 VeriFlow University of Illinois 2013 AP Verifier University of Texas 2013 Anteater University of Illinois 2011 FlowChecker University of North Carolina 2010 VERMÓNT – VERifying MONiTor Our nearest goals and current results • Fast constructing of an initial model (1÷10 s) • Fast model modification (1÷10 ms) • Fast checking of the policy compliance (1÷10 ms) • Expressive language to specify policies (FO[TC]) • A possibility to localize the violation • Sensible information about the problem • Deeper integration with a controller • Monitoring the operation of the controller applications • Interpreting commands and preventing temporal violations • Application advising and synthesizing safe commands THANK YOU FOR YOUR ATTENTION!