CS 219: Network Verification - Course Review

George is a fantastic teacher with very attractive lectures. I think his secret sauces include the following:

• Look at everything from different views: Zoe (ζωή, big picture) versus Bios (βίος, details).
• Selectively focus on the most important techniques and examples, ignoring unnecessary points. Students can feel that they learned a lot without remembering too much boring concepts.
• Have his own methodologies on creative process. Students can experience those "Aha" times when following his introduction.

The trade-offs may be as follows: (very biased personal view, don't take it serious)

• (+) Attending lectures is always pleasant.
• (+) Students can learn things quickly and apply to his own research.
• (-) His lectures may give the false image that creating things is as easy as the fusion of ideas. This is not true because one must have a broad view to know what to borrow, and there are boring times such as trials and errors, non-trivial adoptation and modification of existing methods. He omitted these in his lecture.

I would strongly recommend everyone interested in networking try his 216 and 219.

In this post I won't put all Bia unless interesting. Using those well-defined mathematical terms, Zoai are quite easy to state and thus very short.

Mathematical Preparation

Poset Topology

To understand a network we must have a language that describe sets of IP addresses. Though every paper we read in 219 uses its own notation, the idea behind is similar. To have a unified notation for this post, I use the concept of regular open algebra. (See also this book, Ch.10)

Suppose $P = (S, \leq)$ is a at most countable poset with a unique maximal $*$. Intuitively, $S$ should be the set of all prefixes of IP addresses or NDN names. We say $x$ refines or extends $y$ if $x\leq y$. Define the topology $\tau$ as the topology generated by principal ideal $\{y: y\leq x\}$ for all $x\in S$. Then,

• A set is open if and only if it is downward closed. For example, the set of all prefixes starting with 192.168.* or 10.0.* is open, which includes 192.168.0.1.
• A set is closed if and only if it is upward closed. For example, the set of all prefixes of 192.168.* is closed, which includes 192.*.
• For a set $A$, let $A^{\perp}$ denote the closure of its complementary set, $A^{\perp} = \overline{S\setminus A}$.
• An open set $A$ is called regular if $A^{\perp\perp} = A$.
  • If $A$ is open, $A^{\perp\perp}$ is the minimal regular set containing $A$.
  • For example, in a binary tree, the ideal generated by 0101* and 0100* is open but not regular. Include 010* will make it regular. In plain English, a regular set cannot include all children of $x$ but exclude $x$ itself.
• The meet $\wedge$ of two regular open sets is their intersection $\cap$.
• The join $\vee$ of two regular open sets is the minimal regular open set containing them. $A\vee B = (A\cup B)^{\perp\perp}$.
  • For example, 0101* joining 0100* gives 010*.
• The negation $\neg$ of a regular open set $A$ is $\neg A = A^{\perp}$.
• The boolean true and false are the whole set $S$ and the empty set $\varnothing$, resp.
• The topological space $(P, \tau)$ is countable T0, and complete.
• Note that $S$ is not necessarily being a tree.
  • For example, one can combine IP addresses and port numbers to make a space of packets. In this space, (192.168.*, 8080) refines both (192.*, 8080) and (192.168.*, *), which are incomparable.
• For incomparable $x, y$, if there exists $z\leq x, y$, $x,y$ are called compatible.

Every open set $A$ is a union of principal ideals $\{y: y\leq x\}$ for some $x$. Thus, we can use a minimal set of such $x$'s to represent $A$. It is easy to write a program which computes meet, join and negation using this principal representation. Depending on $S$, there will be a canonical algorithm and I don't think I need to describe the details.

This complete boolean algebra is sometimes called boolean-valued model, because it supports all operators of propositional logic.

Modal Logic

Modal logic includes modal operators to describe necessity $\Box$ and possibility $\Diamond$. In modal logic, we can transite from one state to another, and the truth values of propositions may change. Under different contexts there are different definitions of modal operators. Basically, $\Box P$ is true iff $P$ is true for all states that current state can transit to; $\Diamond P$ is true iff $P$ is true for some future state. One may define $\Diamond P := \neg\Box\neg P$.

Kripke semantics gives a way to model the semantics of all different modal logic systems. A Kripke model is a triple $\langle W,R,\Vdash \rangle$. $W$ is the set of possible states. $R$ is a relation on $W$ that defines transition. $\Vdash$ is the forcing relation, where $w\Vdash P$ if the proposition $P$ is true at $w$. Also, $w\Vdash \Box P$ iff $u\Vdash P$ for all $w R u$.

In Kripke model, modal axioms are related to the properties of $R$:

Name	Axiom	Condition
K	$\Box(A\to B)\to\Box A\to\Box B$	-
T	$\Box A\to A$	reflexive: $wRw$
4	$\Box A\to \Box\Box A$	transitive: $wRv\wedge vRu\to wRu$
D	$\Box A\to \Diamond A$	serial: $(\forall w)(\exists v)wRv$
H	$\Box(\Box A\to B)\vee\Box(\Box B\to A)$	$(wRu\wedge wRv)\to (vRu\vee uRv)$
G	$\Diamond\Box A\to \Box\Diamond A$	convergent: $(wRu\wedge wRv)\to \exists x(vRx\wedge uRx)$

Sometimes people uses $\bigcirc$ for holding at the next step, and $\Diamond$ for eventually holding (i.e. the closure of $R$).

Linear temporal logic (LTL) is a modal logic system frequently used in language design and networks.

Boolean Algebra and Forcing

Boolean-valued model and forcing relation can sometimes replace each other.

$$p\Vdash A \iff p\leq \|A\|$$

where $\|A\|$ is the truth value in some boolean-valued model.

An example is given in the Symmetry and Surgery section.

Introduction

If we take routers as programs

• Control plane: (Config * Env) -> FIB
• Data plane: (FIB * Packet) -> FwdResult

Data Plane Verification

Data plane static check requires a snapshot of current network. Its input is ACLs and FIBs at a specific timing.

Header Space Analysis (HSA)

A router can be abstracted as a transfer function that rewrites the packet and transfers it to the next hop. A function that rewrites a packet will map a regular open set to another. Therefore, we can simply track those sets.

• Compute reachability: Inject $*$ at a node A and then propagate.
• Finding loops: Let $T$ denote the function describing packets start from A, pass some nodes and come back to A. Check if the following descending chain is stationary at empty:

$$[A_0 = *] \supseteq [A_1 = A_0\cap T(A_0)] \supseteq \cdots \supseteq [A_{i+1} = A_i\cap T(A_i)] \supseteq \cdots$$

NetPlumber

If we keep necessary intermediate results, HSA can work incrementally. Assume the graph from node A to B is a DAG. We can push from the node that is modified.

This paper also presents a language that describes the graph.

Atomic Predicates

Regular open sets are generated by principal ideals via $\vee$. Those ideals intersect with each other, and not everyone is useful in a network. Compute a minimal set $M$ of principal ideals that can generates every regular open set used in HSA. Encode every element of $M$ with a number, and every regular open set with $\vee$ of elements from $M$. The arithmetic is clear.

NoD

NoD utilizes SMT solver. It adds new Select-Project operator and new ways of encoding. But it seems that the new encoding only works for binary strings with finite length.

Instead of outputs all reachability relations, NoD checks beliefs specified by operators. It can provide all violations.

Anteater

It reduces the problem to SAT. The same logic expression as boolean-valued logic can be used.

In implementation, it uses LLVM-IR. So the user can write programs in C++, compiles it with clang to IR and then with Anteater to SAT.

Symmetries and Surgeries

This is designed for fat-trees of data center networks. Since data center networks is symmetric, the network topology can be simplified. For example, if A1 and A2 are connected to exactly the same boxes and configured with exactly same rules, then they can be reduced to a single box A. Even if boxes are not perfectly symmetric, we can still reduce rules. For example, use a regular open set to "cut" the network.

Network logic

This work defines a modal logic similar to LTL, but specifically for network. This is interesting so I give a breif introduction here with slightly modified notation.

In this work, a state is a packet $h$ staying at a specific interface $i$ of a node $n$, denoted as $h@n.i$ or $h@p$ with $p=(n,i)$. $h\Vdash P$ abbreviates $(\forall p)h@p\Vdash P$ (globally true for a packet) and $\Vdash P$ abbreviates $(\forall h)h\Vdash P$ (tautology).

There are two kinds of transitions: internal and external. An internal transition $h@n.i\to h'@n'.i'$ holds iff $n$ rewrites $h$ to $h'$, and sends it to an interface connected to the next hop $n'.i'$. An external transition $h@n.i\twoheadrightarrow h'@n.i'$ holds iff $n$ rewrites $h$ to $h'$ and sends it to an external interface $i$. (The paper writes $n'$ which I believe is a typo)

There are two kinds of atomic propositions: $\alpha$ is a proposition describing $h$ and irrelevant to $p$: $h@p\Vdash \alpha$ iff $h\Vdash\alpha$. $@p$ is a proposition holds for all packets at $p$: $h@p\Vdash @p$. The three modal operators are applied to different relations: $\Box$ and $\Diamond$ are applied to internal transitions, but $\bigcirc$ is applied to external only. That is

• $\Diamond P$ iff $P$ is currently true or true after the packet is forwarded to some internal port.
• $\Box P$ iff $P$ is currently true and always true in the internal network.
• $\bigcirc P$ iff the packet is going to be forwarded to an outgoing face, and $P$ is true there.

For example:

• $\Vdash \alpha\wedge @p \to \Box @p$ means packets satisfying $\alpha$ is dropped at $p$.
• $h \Vdash @p \to \Diamond(\neg @p \wedge\Diamond @p)$ means $h$ loops back to $p$, with header possibly rewritten.
• $\Vdash \alpha\wedge @p\to \Diamond(\neg @p \wedge\Diamond (\alpha\wedge @p))$ can detect infinite loops.

$\Vdash$ is specific for a network. The paper proves for some specific $N, N', P$ $\Vdash_{N} P$ iff $\Vdash_{N'} P$. Under this circumstance $N'$ can replace $N$.

Note: boolean-valued model

This can be turned into a boolean valued model. For example, given the following network (address is 3 bit $a_0a_1a_2$)

                   0* P1
                 +------
  P0   +-----+   |
-------| Box |---+
       +-----+   | 1* P2
                 +------

And proposition $A = (a_0\oplus a_1)\wedge @P_1$. Then, we have $001@P1\Vdash \neg A$ and $010@P1\Vdash A$.

On the other hand, we can define a boolean-valued model and let

$$\|A\| = (01*\vee 10*)\wedge P_1 = \langle 01*,P_1\rangle \vee \langle 10*,P_1\rangle$$

And we have $h@p\Vdash A$ iff $h@p$ in the regular open set $\|A\|$.

The operator $\Diamond$ now becomes a function on boolean values. For example, we have $010@P0\Vdash \Diamond A$ before. In the boolean-valued model,

$$\|\Diamond A\| = \Diamond(\|A\|) = \langle 01*,P_1\rangle \vee \langle 10*,P_1\rangle \vee \langle 01*,P_0\rangle$$

However, $\Diamond$ can be very hard to compute, so boolean-valued model is not as useful as it is in HSA.

Data Plane Testing

Data plane testing is to send packets with specific header in the deployed network, and verify whether it works as expected.

ATPG

This work uses HSA to generate an all-pairs reachability table {Header Space, Ingress Port, Egress Port, Rule History}. In this table there are equivalent classes of packets (with ports). It picks one packet from each equivalent class. To further reduces the number of packets, it selects a subset of those packets that covers all rules in the network. The idea of rule coverage comes from path coverage in software verification. If packets are test cases, then rules are exactly if-branches.

I think Atomic Predicate should also work here. We can pick one packet from each principal ideal, and then select a covering subset.

Software Dataplane Verification

This work only verifies the implementation of a software router Click. Nothing special related to networking. I think it should be submitted to a software engineering or a compiler design conference.

Control Plane

BGP-RCC

This work does static checking of BGP. I don't fully understand this work. In very abstract, they parse router configurations, and check whether some beliefs (such as route validity and path visibility) hold.

Batfish

Batfish works as follows:

1. Parse OSPF and BGF configuration from routers.
2. Compute a data plane result from configuration.

• LogiQL, a Datalog variant, is used here.

3. Analysis the data plane.
4. Report the result.

Efficient Network Reachability Analysis (ERA)

Data plane reachability depends on route reachability. A packet cannot reach B from A unless on every node in the path:

• There is a route from B reaches A.
  • Route is an abstract of route advertisement, encoded as a bitvector.
• There is no ACL drops this packet.

How a router handles routes is a program that works on bitvector. We can model routes with BDD/ZDD, and let routers act on it.

Synthesis: Propane

Propane takes user input describing network topology and policies, compiles it into state machines, and generates BGP configuration of every router. Propane enables centralized configuration and distributed implementation simultaneously.

Verification: Minesweeper

Minesweeper parses router configuration and encodes routing protocols with SMT. Then, it can check whether user-specified beliefs are violated. Minesweeper scales but only returns 1 counterexample.

Lessons Summarized

As introduced in CS 216, an idea arises when an impacting steam hits the main stream. Through these works, we can clearly see the influences (or similarities) from other fields on networking:

• Programming languages and formal verification
  • Use of automated proof tools (Datalog, SMT)
  • Logical modeling (boolean-valued model, LTL)
  • Use of existing compiler (LLVM-IR)
  • Use of existing data structures (BDD)
• Software testing
  • Branch coverage -> rule coverage
  • Source-code annotation -> beliefs
• Hardware design
  • EDA -> Synthesis
  • Programmable hardware (FPGA) -> SDN, P4
• Algebra
  • Exploiting symmetries

More methods, tools and concepts from all different fields will be applied to networking. Algorithms and data structures can be used to develop routers. Dynamical systems and graph theory can be utilized to research packet dynamics. Software architecture has similarities with cloud/distributed architecture. Cryptography influences cyber security. I believe networking field is still far from mature, and it will not stop growing as well as borrowing from other fields.

References

• Givant, S., and P. R. Halmos, 2009: Introduction to Boolean Algebras. Springer.
• Kazemian, P., G. Varghese, and N. McKeown, 2012: Header Space Analysis: Static Checking for Networks. 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12).
• Kazemian, P., et al., 2013: Real Time Network Policy Checking Using Header Space Analysis. 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13).
• Yang, H., and S. S. Lam, 2013: Real-time verification of network properties using Atomic Predicates. 2013 21st IEEE International Conference on Network Protocols (ICNP).
• Lopes, N. P., et al., 2015: Checking Beliefs in Dynamic Networks. 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15).
• Mai, H., et al., 2011: Debugging the data plane with anteater. SIGCOMM Comput. Commun. Rev. 41, 4 (August 2011), 290–301.
• Plotkin, G. D., et al., 2016: Scaling network verification using symmetry and surgery. SIGPLAN Not. 51, 1 (January 2016), 69–83.
• Zeng, H., P. Kazemian, G. Varghese, and N. McKeown, 2012: Automatic test packet generation. In Proceedings of the 8th international conference on Emerging networking experiments and technologies (CoNEXT '12), 241–252.
• Dobrescu, M. and K. Argyraki, 2014: Software Dataplane Verification. 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14).
• Feamster, N. and H. Balakrishnan, 2005: Detecting BGP configuration faults with static analysis. In Proceedings of the 2nd conference on Symposium on Networked Systems Design & Implementation - Volume 2 (NSDI'05), 43–56.
• Fogel, A., et al., 2015: A General Approach to Network Configuration Analysis, 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15).
• Fayaz, S. K., et al., 2016: Efficient Network Reachability Analysis Using a Succinct Control Plane Representation, 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16).
• Beckett, R., et al., 2016: Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations, SIGCOMM 2016.
• Beckett, R., et al., 2017: A General Approach to Network Configuration Verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM '17), 155–168.