Provably Correct Networks and Network Verification

Network verification without policy specification Costin Raiciu Dragos Dumitrescu, Radu Stoenescu, Matei Popovici, Lorina Negreanu University Politehnica of Bucharest CORNET H2020 Thanks to

CORNET: Provably Correct Networks ERC Starting Grant 2017 January 2018 December 2022 Talk is based on: Debugging P4 programs with Vera Sigcomm 2018 Ongoing work at UPB in the Netsys group.

Network verification is badly needed Southwestern and United had router outages that lead to thousands of cancelled flights Potential sources of network errors Configuration errors ( fat fingers ) Bugs (in routing protocols or dataplane) Equipment failures Networks becoming more programmable (SDN,P4) More bugs expected!

Network operation overview Config ... ... Admin Policy Dean must have Internet connectivity Exit? router? Cluster? Lab? ? M1? ? ? ? Office? ? M2? Aggrega on? ? ? ASA?

Network verification [HSA, NOD, Veriflow, Symnet, Batfish, etc.] Config ... ... Admin Policy Dean must have Internet connectivity DATA PLANE MODEL Verify

Writing policies is tedious and limits uptake of network verification Policy is either incomplete reachability / isolation rules (e.g. iptables format) Or very complicated to write Datalog ([NOD, FML]) Computation tree logic [NetCheck] Stepwise specification and refinement: [Cocoon]

GOAL: network verification without policy specification

Two main directions Find bugs in dataplane programs. Dataplane equivalence as a proxy for specification.

P4 enables custom dataplanes High speed, customized packet processing Removes reliance on equipment vendors to add new functionality Available in switches today.

P4 is surprisingly difficult to use Language features very close to hardware Debugging is manual no traps Program is seemingly incomplete Table rules available only at runtime Implicit behaviour Dropped packets are processed

P4 by example: route and encapsulate Ingress Pipeline Egress Pipeline IN OUT DEPARSER Buffers encap ipv4_lpm PARSER TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 Control program what sequence of M/A tables is applied to a packet Match-action (M/A) tables - how a P4 switch can tranform packets What packets the switch accepts and outputs 11

P4 by example: route and encapsulate Ingress Pipeline Egress Pipeline IN OUT DEPARSER Buffers encap ipv4_lpm PARSER TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 parser start { extract(eth); return select(eth.type){ 0x800 : parse_ipv4; default: ingress; }} parser parse_ipv4 { extract(ipv4); return ingress; } Deparsing uses the same parser specification. Common problem: forget to parse output packets. 12

P4 by example: route and encapsulate Ingress Pipeline Egress Pipeline IN OUT DEPARSER Buffers encap ipv4_lpm PARSER TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 parser start { extract(eth); return select(eth.type){ 0x800 : parse_ipv4; default: ingress; }} parser parse_ipv4 { extract(ipv4); return select(ipv4.protocol){ 0x5E : parse_inner_ipv4; default: ingress; }} parser parse_inner_ipv4 { extract(inner_ipv4); return ingress; }} 13

P4 by example: route and encapsulate parser start { Ingress Pipeline Egress Pipeline extract(eth); return select(eth.type){ 0x800 : parse_ipv4; default: ingress; }} parser parse_ipv4 { extract(ipv4); return select(ipv4.protocol){ 0x5E : parse_inner_ipv4; default: ingress; }} parser parse_inner_ipv4 { extract(inner_ipv4); return ingress; }} IN OUT DEPARSER Buffers encap ipv4_lpm PARSER TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 control ingress(){ if (ipv4.TTL>0) } apply(ipv4_lpm); Reading unparsed header fields will return undefined values 14

P4 by example: route and encapsulate Ingress Pipeline Egress Pipeline IN OUT DEPARSER Buffers encap ipv4_lpm PARSER valid(ipv4) &&TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 control ingress(){ if (valid(ipv4) and ipv4.TTL>0) apply(ipv4_lpm); } Non IPv4 packets will be sent directly to buffering resulting in undefined behavior because the egress_spec is not set 15

P4 by example: route and encapsulate Ingress Pipeline Egress Pipeline IN OUT DEPARSER Buffers encap ipv4_lpm PARSER valid(ipv4) &&TTL>0 *1.2.3.4 5.6.7.8 10.0.0.0/8 Ge0 Re-adding existing header fields: undefined behavior 16

Vera design goals Easy to use high bug coverage with no policy specification General policy verification for more complex properties Scalable comparable to compilation times 17

How Vera works P4 table entries P4 program P4 to SEFL Compiler Implicit bug checks Symnet verification engine[Sigcomm 16] Network Policy For each possible path: full instruction trace, header field values, constraints and, if needed, bug type 18

Vera at work deparser parser.start control.ingress table.lpm.0 * eth.type ==0x800 ipv4.TTL>0 ipv4.dst==10/8 eth,ipv4 ipv4.TTL<=0 deparse error buffer.in implicit drop

Vera at work Applied Vera to all public P4 programs we could find Found multiple bugs in each of them Runtime: 1-10s with concrete table entries

Evaluation summary

Equivalence checking

Dataplane equivalence is an implicit way to specify policy Admin Policy The network works fine now. Must behave in the same way after config change. Exit? router? Cluster? Lab? ? M1? ? ? Office? ? M2? Aggrega on? ? ? ASA?

Dataplane equivalence is an implicit way to specify policy 192.168.1.0/24 R2 A Tenant Cloud interface Router Instance 10.9.0.0/24 Private Public 10.9.0.15 C B Instance Instance 192.168.1.2 10.9.0.14 Must be equivalent Cloud net driver IPtables rules Openflow rules ACLs FIBs Cloud dataplane

What is dataplane equivalence? A dataplane is a program where the memory is the packet and associated metadata (mostly). Two dataplanes are equivalent iff they produce the same output packets when receiving the same input packet, for all possible inputs.

Checking dataplane equivalence scalably with symbolic execution Assume exhaustive symbolic execution finishes in reasonable time on both programs. Need to decide from the sets of paths resulting from symbolic execution if the two programs are equivalent.

Equivalence by example: router Basic router dst in 10.10.0.1/32&&TTL>=0 in: dst in 10.10.0.0/16&&TTL>=0 && dst not in 10.10.0.1/32 if0 in TTL-- if1 dst in 10.0.0.0/8 && TTL>=0 dst not in 10.10.0.0/16 && dst not in 10.10.0.1/32 TTL==0 X X dst not in 10/8 && dst not in 10.10/16 && dst not in 10.10.0.1/32 Optimized router in: dst in 10.10.0.0/16 && TTL >=0 if0 in TTL-- if1 dst in 10.0.0.0/8 && TTL>=0

Checking equivalence Output equivalence For every packet header, check that the possible output values are the same for the two programs, for each equivalent port. TTL>=0 && dst in 10.10.0.1/32 TTL>=0 && dst in 10.10.0.0/16 && dst not in 10.10.0.1/32 Basic router if0 TTL >=0 && dst in 10.10.0.0/16 if0 Optimized router TTL>=0 && dst in 10.0.0.0/8 && dst not in 10.10.0.0/16 &&dst not in 10.10.0.1/32 if1 Basic router Optimized router if1 TTL>=0 && dst in 10.0.0.0/8

Output equivalence is not enough Basic router Allows only packets with TTL>0 in: if (TTL>0) TTL--; else Fail; in: TTL--; Constrain(TTL>=0); Allows all packets (TTL is unsigned) Optimized router On output, the possible values for TTL are the same!

Checking equivalence Input equivalence For every packet header, check that the constraints applied on the values at program input are the same for the two programs.

Input and output equivalence are still not enough Program 1 in: NoOp; in: TTL = 255-TTL; Program 2 On input, the allowed values for TTL are the same. On output, the possible values for TTL are the same.

Checking equivalence Functional equivalence For every packet header and every port, check that the header fields take exactly the same value in all points.

EQ: putting it all together Input: P1, P2, port equivalence map. Output: OK, or Paths for which the outputs of P1 and P2 differ.

EQ operation Prog1 Symbolic packet Output, functional equivalence check with SMT solver Input equivalence check by design Prog2

Verifying Openstack Neutron Check for equivalence between tenant view and implemented dataplane Translate tenant view to SEFL Snapshot dataplane (ovs and iptables) and translate to SEFL. Compare snapshots with EQ.

Verifying Openstack Neutron Six tenants, 16VMs, three VLANs per tenant. 1600 Openflow rules in dataplane snapshot Verification runtime: 200s 250s Bugs caught: 5 Neutron software bugs (1 unknown) 2 configuration bugs 1 tenant-level misconfiguration.

Policy specification is hard Symbolic execution finds bugs in P4 programs. Equivalence checking finds bugs in Openstack Neutron, P4 programs, etc. Open question: what properties can we always verify in enterprise networks?

Backup slides

Comparing two router implementations

Dataplane equivalence at work Implemented in Scala in a tool we call sdiff Uses our Symnet symbolic execution engine [Sigcomm 2016] Translates all dataplane code to the SEFL language

Isnt equivalence undecidable? Equivalence is decidable for programs that are guaranteed to finish. Trivial algorithm: enumerate all possible inputs, run both programs, check outputs are the same.