change headings to bold

Author: Ryan Beckett

_posts/2020-04-06-current-state-of-research.md

@@ -20,7 +20,7 @@ This article presents our view of the state of research in this domain.  Our vie
 
 We realize that perspective is inherently biased by our experiences and inherently incomplete. We also realize that we risk irking research colleagues who do not agree with our characterization (or whose work we failed to categorize). We invite those researchers to share their own perspectives.
 
-###The first wave: data plane verification
+**The first wave: data plane verification**
 
 Some of the earliest work on network verification was adopted for network “data planes”. The data plane refers to the part of the network responsible for forwarding packets from point A to point B. In general, network forwarding is performed by a collection of “switches” that each maintain a forwarding table that matches a packet entering the switch and determines which port(s) the packet should go out of.
 
@@ -31,7 +31,7 @@ and later made more scalable with the [Header Space Analysis](https://www.usenix
 
 Later approaches to data plane verification improved upon HSA in one dimension or another, such as making the analysis incremental with [Veriflow](https://www.usenix.org/system/files/conference/nsdi13/nsdi13-final100.pdf), making the analysis faster with [AP](https://www.cs.utexas.edu/users/lam/Vita/Cpapers/Yang_Lam_AP_Verifier_2013.pdf), leveraging the network [topology structure](https://dl.acm.org/doi/10.1145/3341302.3342094), and so on.
 
-###The second wave: control plane verification
+**The second wave: control plane verification**
 
 While data plane verification involves analyzing how packets are forwarded according to the tables present at every switch, in real networks these tables are themselves populated by other protocols or software. This “control plane” typically comes in two flavors: (1) distributed routing protocols, or (2) a centralized orchestrator.
 
@@ -41,21 +41,21 @@ As a result, arguably researchers have had more success with (1). For example, [
 
 As with data plane verification, much of the later work in this area is focused on improving these techniques along one dimension or another, such as improving [performance](https://arxiv.org/pdf/1906.02043.pdf), or leveraging network [symmetry](https://ratul.org/papers/sigcomm2018-bonsai.pdf).
 
-###The third wave: programmable networks
+**The third wave: programmable networks**
 
 Programmable network devices such as [Barefoot’s Tofino switch](https://barefootnetworks.com/products/brief-tofino/) have recently come to the market with the promise of replacing fixed-function network ASICs with programmable switches. The capability to program new functionality into the switch itself enables exciting new opportunities and holds promise to allow networks to evolve more quickly.
 
 However, programmable switches also make verification more challenging since the data plane can now perform arbitrary logic. An important paper in this space is [p4v](https://www.cs.cornell.edu/~jnfoster/papers/p4v.pdf), which leverages [verification condition generation](https://en.wikipedia.org/wiki/Verification_condition_generator) to reason about such programs with assumptions about the control plane. Fortunately, the absence of loops or recursion in data plane programs (since they must forward at line-rate) allows tools like p4v to be fully automatic.
 
-###Network synthesis
+**Network synthesis**
 
 In contrast to verification, network synthesis has received relatively less attention. In the data plane, there is some early work such as [NetGen](http://madhu.cs.illinois.edu/sosr15-netgen.pdf). For the control plane, a notable example of synthesis is [Propane](https://ratul.org/papers/sigcomm2016-propane.pdf), which generates configurations for the BGP routing protocol from a high-level specification. Researchers have also recently explored the related problem of [repairing](https://aaron.gember-jacobson.com/docs/gember-jacobson2017cpr.pdf) the control plane.
 
-###So what problems have been solved?
+**So what problems have been solved?**
 
 In hindsight, perhaps the most clearly “solved” problem in network verification is that of stateless data plane verification, which also happens to be the earliest work in this space. Stateless data plane verification tools today can already scale to handle large networks with millions of forwarding table rules and thousands of routers, all at human time scales. Further work in this area has also revealed additional optimizations that make such tools even more scalable. These tools have been successful enough to find their way into practical use at various companies such as [Microsoft](https://dl.acm.org/doi/10.1145/3341302.3342094)
 
-###So what problems remain open?
+**So what problems remain open?**
 
 Although verifying stateless data planes is largely a solved problem. The closely related problem of verifying stateful data planes -- for instance those networks with stateful firewalls that retain state across packets -- remains hard today. There is some [early work](https://www.usenix.org/system/files/nsdi20spring_yuan_prepub_0.pdf) in this space, but many problems remain.
 
@@ -67,7 +67,7 @@ Programmable networks remain another large open area in the field. While it is c
 
 Finally, research into network synthesis in general remains in its infancy. However, the idea has taken off in practice under the terminology of [Intent-Based Networking](https://www.cisco.com/c/en/us/solutions/intent-based-networking.html). While there is currently a lot of marketing hype around Intent-Based Networking, there has been little work in this area to understand its theoretical underpinnings to date.
 
-###Summary
+**Summary**
 
 Network verification and synthesis are timely and exciting technologies that hold the promise of increasing the reliability of our critical network infrastructure. We summarized the current state of the art in these two areas and detailed our observations after teaching a course on the topic at the University of Washington in 2019.