fix header

Author: ratulm

_posts/2020-12-14-network-verification-2-0.md

@@ -35,13 +35,15 @@ Network verification tools are engineered as monoliths today. They have a custom
 We have witnessed this difficulty first hand with tools that we have helped develop. At Microsoft, our engineers have developed tools to verify the safety of changes to access control lists, network security groups, and forwarding table rules. Each time we had develop a new tool from scratch despite the similarity of these functionalities because extending the prior tool was no easier than building a new one. Similarly, extending Batfish over the years to support more network functionality or additional router vendors with slightly different semantics has required significant changes to the analysis pipeline. 
 
 The monolithic approach was helpful for the first generation of network verification tools because the tight integration between network functionality and analysis enabled faster iteration. However, this tight coupling is no longer necessary and we can decouple network modeling from analysis. Network functionality can be modeled in a common language and analysis engines can target the language instead of specific functionality. That way, extending verification to new functionality only requires modeling that functionality. Once that is done, one or more analysis engines become available to analyze that functionality.
-A linguistic approach
+
+## A linguistic approach
+
 There are multiple ways to tackle the Network Verification 2.0 challenges above, but a linguistic approach is particularly appealing (which we are exploring; see here and here). To make it easy for engineers to specify inputs, along with their networks’ unwritten assumptions, we should design an invariant language that can naturally express sets of values and set operations like unions and differences. We may consider a language that blends SQL-like queries over a data model of the network and regular expressions over path constraints. 
 
 A high-level invariant language over a well-defined data model also makes it easy to track which network elements (e.g., devices, interfaces, paths) are “covered” by an invariant. This basic capability can then be the basis for providing feedback to network engineers about how well their invariant set covers the network. This is similar to how test frameworks for software can quantify the extent of software coverage, though we will need custom measures for network coverage given the differences in the two domains (e.g., a network is not a sequence of statements or basic blocks, which is the model employed by software test frameworks). 
 
 Finally, we should look toward intermediate verification languages such as Rosette, Boogie, and Kaplan to engineer network verification tools to be easy to extend. These languages allow multiple source languages to be compiled to them and various analysis approaches then become accessible, without the need for inventing source language specific analysis tools. In a similar manner, we could translate different network functionalities into an intermediate language and develop a common set of analysis tools for this language. Then, verification can be easily extended to any functionality that can be translated to this intermediate language. Of course, for this approach to be practical, we need to design an expressive intermediate language for which engineers can develop efficient analyses.
 
-##Summary
+## Summary
 
 The next generation of network verification research must enable broad use of verification tools such that all networks are rigorously analyzed and they become indispensable to engineers like ping and traceroute are today.  We can achieve this goal by making the tools more accessible to engineers on the ground and easy to extend to adjacent functionality.  Solving these challenges will radically improve the security and reliability of the networking infrastructure that is critical to modern society.