diff --git a/_config.yml b/_config.yml index e1219a0..87d4cd0 100644 --- a/_config.yml +++ b/_config.yml @@ -107,6 +107,19 @@ authors: avatar: /assets/images/aaron-gember-jacobson.jpg bio: "Aaron Gember-Jacobson is an Assistant Professor of Computer Science at Colgate University. Aaron's research focuses on network configuration verification and synthesis. Aaron enjoys teaching Introduction to Computing, Operating Systems, Computer Networks, and a First Year Seminar entitled 'The Unreliable Internet.' Aaron received a Ph.D. and Master of Science in Computer Science from the University of Wisconsin-Madison and a Bachelor of Science in Computer Science from Marquette University. During his Ph.D., Aaron was awarded the Internet Engineering Task force (IETF) Applied Networking Research Prize (2015) and an IBM Ph.D. Fellowship." + jrex: + name: Jennifer Rexford + site: https://www.cs.princeton.edu/~jrex/ + avatar: /assets/images/jennifer-rexford.jpg + bio: "Jennifer Rexford is the Gordon Y.S. Wu Professor of Engineering and the Chair of Computer Science at Princeton University. Before joining Princeton in 2005, she worked for eight years at AT&T Labs--Research. Jennifer received her BSE degree in electrical engineering from Princeton University in 1991, and her PhD degree in electrical engineering and computer science from the University of Michigan in 1996. Jennifer received the ACM SIGCOMM award for lifetime contributions and the IEEE Internet Award." + twitter: jrexnet + + pamela: + name: Pamela Zave + site: http://pamelazave.com/ + avatar: /assets/images/pamela-zave.jpg + bio: "Pamela Zave is a researcher in the Computer Science Department of Princeton University. She received a PhD degree in computer sciences from the University of Wisconsin--Madison and an AB degree in English from Cornell University. She spent 36 years in the research divisions of Bell Labs and AT&T Labs, doing interdisciplinary work at the intersection of formal methods and network services. Dr. Zave is an ACM Fellow, an AT&T Fellow, and the 2017 recipient of the IEEE Harlan D. Mills Award for the development of sound software-engineering theory and sustained, impactful applications to practice. In addition to her research publications, she holds 32 patents." + # Defaults defaults: diff --git a/_pages/author-jennifer-rexford.html b/_pages/author-jennifer-rexford.html new file mode 100644 index 0000000..03e10cb --- /dev/null +++ b/_pages/author-jennifer-rexford.html @@ -0,0 +1,26 @@ +--- +title: "Jennifer Rexford" +layout: default +permalink: "/author-jennifer-rexford.html" +--- +
+
+
+
+
+

{{page.title}} View

+

{{ site.authors.jennifer.bio }}

+
+
+ {{ site.authors.jennifer.name }} +
+
+

Posts by {{page.title}}

+ {% for post in site.posts %} + {% if post.authors contains "jennifer" %} + {% include main-loop-card.html %} + {% endif %} + {% endfor %} +
+
+
\ No newline at end of file diff --git a/_pages/author-pamela-zave.html b/_pages/author-pamela-zave.html new file mode 100644 index 0000000..ceab326 --- /dev/null +++ b/_pages/author-pamela-zave.html @@ -0,0 +1,26 @@ +--- +title: "Pamela Zave" +layout: default +permalink: "/author-pamela-zave.html" +--- +
+
+
+
+
+

{{page.title}} View

+

{{ site.authors.pamela.bio }}

+
+
+ {{ site.authors.pamela.name }} +
+
+

Posts by {{page.title}}

+ {% for post in site.posts %} + {% if post.authors contains "pamela" %} + {% include main-loop-card.html %} + {% endif %} + {% endfor %} +
+
+
\ No newline at end of file diff --git a/_posts/2021-01-04-compositional-network-architecture.md b/_posts/2021-01-04-compositional-network-architecture.md new file mode 100644 index 0000000..1461b21 --- /dev/null +++ b/_posts/2021-01-04-compositional-network-architecture.md @@ -0,0 +1,58 @@ +--- +layout: post +title: "Compositional Network Architecture" +authors: [pamela, jrex] +categories: [research, network, architecture] +image: assets/images/cnaPic.png +tags: [] +--- + +Compositional Network Architecture is a new descriptive model of networking, possibly the first since the "classic" Internet architecture of the late 1980s. You all know the classic architecture: it has physical, link, network, transport, and application layers. + +This article will talk about two reasons why CNA is worth your attention: + +- It provides precise and comprehensive descriptions of how the Internet works today. In doing so, it solves a mystery of Internet evolution. +- It helps us identify recurring patterns in networking. These are problems that occur in many different, but predictable, contexts, along with a range of solutions to them. We are so excited about this way of teaching networking that we are writing a textbook based on it. + +A third reason, modular verification, is the most relevant to this site, so it will be covered in a follow-up article. + +## Describing today's Internet + +CNA is different from the "classic" model of Internet architecture in several important ways, but in this article we'll talk about just one: the definition of _layering._ + +Layering in the classic model is layering in the ordinary software-engineering sense: the overlay depends on the underlay, while the underlay is independent of the overlay and incorporates no knowledge of it. There is a fixed number of layers, each with a different function to perform. Just as each layer can be completely different from the others, the interface between two adjacent layers can be different from other interfaces. + +CNA, on the other hand, is based on the idea that the module of networking is a _network._ Each _network_ is a microcosm of networking, with all the basic mechanisms including a namespace, nodes, links, routing, forwarding, session protocols, and directories (although some parts can be vestigial in some networks). In this model the Internet is a flexible composition of many networks; these networks differ from each other in purpose, geographical span, membership scope, and level of abstraction. Networks are composed with two operators, _bridging_ (with the obvious meaning) and _layering_. + +In any network, a _session_ is an instance of one of the services provided by that network. At a minimum, it is a set of packets that network users group together. According to the CNA definition of layering, one network is layered on another network if a link in the overlay network is implemented by a session in the underlay network. This means that the overlay link is virtual, while the links in the underlay network can be virtual or physical. + +As a consequence, layers in the new model are bigger than layers in the classic Internet architecture--for example, the classic network and transport layers of the Internet together make one CNA layer composed of IP networks bridged together. The advantage is that a bigger module is more complete, so a network's interface to an overlay network is the same as the interface of an underlay network to it. In other words, we have made networks composable like Lego bricks. + +![](/assets/images/cnaPic.png) + +The picture shows the headers of a typical packet in the AT&T backbone network. The packet is traveling through 6 layered networks simultaneously, 3 of which are IP networks. Each IP network is revealed by an IP header for forwarding and one or more session-protocol headers. + +At other observation points, packets would likely have similar complexity, but with different layers, because there is no need for global agreement on compositional architecture. As explained in detail in our Communications of the ACM paper [1], this and many other observations solve a mystery of Internet evolution: how the Internet has evolved since 1993 to meet many difficult new challenges, despite the fact that there has been no major change in the IP protocol since then. + +## Patterns in networking + +Because CNA defines many ways in which all networks and network interfaces are similar, it also points to problems that most networks or compositions of networks will have to solve. The word is "most" rather than "all" because the restricted purposes of some networks, or the extra similarities between some composed networks, can simplify some problems out of existence. + +Viewed with enough abstraction, each predictable problem has a suite of common solutions. The problem and the solutions make a recurring pattern. Teaching these patterns seems much more meaningful and memorable than teaching detailed instances of the patterns without linking them together. We are so excited about this way of teaching networking that we are writing a textbook based on it. + +On the way, we have written two survey articles based on CNA, which will become chapters of the textbook. + +Mobility is the network function that maintains network connectivity to a machine, despite the fact that the machine is moving its attachment to the network. "The design space of network mobility" [2] explains that there are exactly two patterns for providing mobility. + +- In one pattern, the named machine simply moves from one access link of the network to another, and routing is updated dynamically so that the machine can still be reached under the same name. For example, MAC learning in an Ethernet can find a machine by its MAC address after it has moved. +- In the other pattern, layering is involved. The mobile machine retains its name and links in the overlay, despite the fact that it is moving. In the underlay network that is implementing these links, the mobile machine has a location-dependent name, which necessarily changes as it moves. The session protocol implementing an overlay link signals the change from one session endpoint to the other, so that the stable endpoint starts sending session packets to the new name. Most proposals for adding mobility to IP networks use this pattern. + +These patterns had never been recognized before our paper, and it was CNA that enabled us to see them. + +Our other survey article takes on the subject of network security [3]. It illustrates an extremely important point, which is that CNA-based teaching of networking offers a solution to an otherwise insoluble problem, which is the explosion of topics to be covered in a networking course. The paper frames the subject of network security, presents a practical classification of security attacks, and divides all defense mechanisms into four patterns. We have planned a tutorial on this material, covering the patterns in 3 hours of lecturing. The same lectures would work in a networking course, especially supplemented by reading the article. The students might not get all the details, but they would have an easy-to-remember framework in which to fit any new security attack or defense they encounter. + +[1] Pamela Zave and Jennifer Rexford, "The compositional architecture of the Internet," _Communications of the ACM_ 62(3):78-87, March 2019 (http://www.pamelazave.com/cnaCACM19.pdf). + +[2] Pamela Zave and Jennifer Rexford, "The design space of network mobility," Olivier Bonaventure and Hamed Haddadi, editors, _Recent Advances in Networking_ (http://www.sigcomm.org/content/ebook/SIGCOMMeBook2013v1_chapter8.pdf), ACM SIGCOMM, 2013. + +[3] Pamela Zave and Jennifer Rexford, "Patterns and interactions in network security," _ACM Computing Surveys_ 53(6):118, 2020, to appear. A version with more explanation, examples, and references is available at https://arxiv.org/abs/1912.13371. diff --git a/_posts/2021-01-11-modular-verification-cna.md b/_posts/2021-01-11-modular-verification-cna.md new file mode 100644 index 0000000..b25cefd --- /dev/null +++ b/_posts/2021-01-11-modular-verification-cna.md @@ -0,0 +1,76 @@ +--- +layout: post +title: "Modular Verification in Compositional Network Architecture" +authors: [pamela] +categories: [research, network, verification] +image: assets/images/cnavPic.png +tags: [] +--- + +In our first article on Compositional Network Architecture, we emphasized its value as a descriptive model. This article considers its uses as a prescriptive model of network architecture. + +As a prescriptive model, the goal of CNA is to allow maximum design freedom inside networks (the modules in our architecture), while ensuring that networks of all designs are composable. In keeping with this goal, the formal semantics of CNA (in Alloy) constrains intra-network mechanisms such as session protocols and routing loosely, requiring only certain data in the network state. The operators for network composition, on the other hand, are formalized completely. + +The semantics of a network is expressed in terms of reachability, and the semantics of a composition operator defines reachability in a composition of multiple networks. Reachability represents both end-to-end and path properties, which are frequently important for security (see below). Reachability is defined at the granularity of packet headers, so it encompasses session properties. There is a form of reachability dependent only on infrastructure (what the network "is willing" to do), and another form that includes a traffic model (what the users want the network to do). Comparing these, it is possible to verify that a network satisfies all legitimate user requirements. + +To realize the benefits of composability, networks should be built with external interfaces that conform recognizably to CNA. With such networks, composition can be implemented automatically and verified correct simply by checking known consistency properties at the interfaces. We now have an implementation of CNA composition in P4 [1], and are using it to explore the benefits of composability in building networks with programmable data planes. These benefits include implementation reuse and--most interesting to the readers of this site--easier verification. + +The Alloy model of networking (on which the semantics is based) can be used as a tool for describing classes of networks and verifying their properties. In parallel with implementation activities, experiments with Alloy modeling and verification are yielding many insights into modular verification of networks. Some of these insights are summarized below. + +## Modular Verification of Layered Networks + +From one perspective, layering is "just tunneling." It's true that an overlay link is implemented by an underlay session with the mechanisms of encapsulation and decapsulation, but this reductive view misses a major truth about verification: The whole overlay network matters, because it is the whole overlay network that defines the purposes, properties, and packet traffic of its links, while the links just happen to be implemented as tunnels in some other network. + +To see how this works, we have investigated numerous examples in which IP networks offering enhanced services are layered on the bridged IP networks of the public Internet. The figure shows an example, a Virtual Private Network, from [1]. The enhanced services of the VPN ensure a variety of security properties. Other examples explore correctness properties for multicast, mobility, and reliability services. + +![](/assets/images/vpn.png) + +In all these examples, layering enables very successful modularity in verification. In fact, in these experiments _every property_ I looked at could be proved exclusively in one network or the other. These properties fall into two categories, in a roughly even split: + +- Because layering enforces a separation of concerns, some properties only need to hold in one network. + +- Some properties are hierarchical. It is required or assumed that they are true of the links of an overlay network. To satisfy this requirement or support this assumption, they must be true of the underlay sessions that implement these links. As a result, they are proved in the underlay network and used as axioms in the verification of the overlay network. + +Verifying one layer/network at a time is much easier than verifying their composition as one monolithic network, for three major reasons: + +- Each network is smaller! One usually has fewer nodes than the other, and in the nodes common to both networks the forwarding rules of the monolithic version will be partitioned between the two layers. Sometimes the benefit of modularity is even greater, because the number of forwarding rules in the monolithic version is the product of the number of rules in modular layers. + +- Each network is more focused and specialized, and has more structure that can be exploited by verification. As a simple example, consider the VPN. An employee of the enterprise is in a coffee shop, with laptop connected to the Internet through WiFi. Its Internet address is in the coffee shop's block, and is largely meaningless for filtering. At the same time, in the overlay VPN, it has an authenticated IP address that indicates the employee's department, rank, and access privileges. As a result, filtering in the VPN, based on source IP address, can have pinpoint precision. + +- There is no need whatsoever to verify the composition of the networks, which might be buried in the details of the monolithic version. In the modular version, layering composition is performed by a verified operator with well-known properties. As an important bonus, network forwarding never alters packets, so invariant forwarding can be used as an axiom in intra-network verification. Invariant forwarding holds because a router's usual functions of adding/deleting headers and changing header fields are all subsumed by the layering operator, and are viewed as part of composition. + +A short paper on network verification [1] uses the the VPN example to explain how a number of security properties could be verified. This verification can take advantage of many existing tools for network verification, as most of the properties are familiar combinations of filtering and forwarding properties in IP networks. Verification also combines results from different proof techniques, as follows: First, mathematical proofs establish the properties of cryptographic session protocols. These session protocols implement secure overlay links. Next, path analysis in the overlay verifies that a designated path through the network consists of only secure links and trusted nodes. + +## A Subtle Form of Layering: Subduction + +In CNA, _subduction_ is a third network-composition operator. It is a combination of bridging and layering, with an extra verification condition to make it work as expected. Although subduction may be new as a concept, it is common in networking. Roughly speaking, pure layering on the public Internet requires the participation of both session endpoints (as in the VPN example). Whenever one or both endpoints does not participate in the overlay, there is likely to be subduction. So it usually occurs whenever a special-purpose IP network is bridged with the public Internet, because only one endpoint is a user of the special-purpose network. + +(For the curious, "subduction" is a geological term. Find a picture, and you will see that one tectonic plate both abuts and slides under another plate, just as the public Internet is bridged with a special-purpose network, and also implements its links by means of layering.) + +In our work with the P4 implementation of CNA, one case study includes some network services requiring flow affinity--all the packets of a designated flow must pass through a single stateful filter. For example, in the figure below, the blue packet in _flow(A)_ does not require flow affinity, and it is simply routed through the network from one gateway to another. The red packet, in contrast, is in _flow(B)_ and needs to pass through the filter _filter(B)_. Both packets enter and leave the network at the same gateways, and we do not want the difficulty of altering normal routing to include location-dependent filtering. To keep the enforcement of flow affinity independent of normal routing, we implement it as an overlay with subduction. In this figure, the solid black lines are physical links, while the dashed black line is a virtual overlay link. + +![](/assets/images/provider-network.png) + +The figure below shows the architecture of this solution, superimposed on the _physical_ path of a packet in _flow(B)_. It enters the overlay through a bridging link from gateway to filter. In the overlay, it is routed to the filter responsible for _flow(B)_. As it travels on a virtual link through the overlay, it is also traveling through the physical links of the underlay, because the overlay is layered on it. The packet exits the overlay through a bridging link from _filter(B)_ to _router2_. + +![](/assets/images/subduction.png) + +There is a fair amount of detail to be managed for the bridging and layering to work right, but this detail is all supplied automatically by our composition operators. There is also an extra constraint because of the subtlety of subduction--the two links marked with asterisks are exactly the same physical link, connecting gateway and filter machines. The two "filters" are members of different networks on the same machine, again implemented automatically by our P4 mechanisms. + +Finally we can get to the topic of verification! Working with models of a flow-affinity-preserving network, a general network, and subduction, I have found a set of constraints on the general network that guarantee correctness. Here correctness consists of two properties: + +- The overlay and general network, composed by subduction, enforce flow affinity on all selected flows. + +- If the overlay has no other added functions (e.g., it does not filter packets), end-to-end reachability in the composed networks is exactly the same as in the original general network. + +In practice the overlay will have added functions and will alter reachability, but the flow-affinity mechanism itself should be neutral. + +The result is a theorem that if a general network satisfies the constraints, then its composition with the overlay has the specified properties. These constraints are not easy find. Yet once we know what they are, they make sense and are satisfied by normal networks. Then, with only these known constraints to check, verified session affinity can be added painlessly to most networks. + +Correctness of a flow-affinity overlay is not something to be verified on a real network--it is far too complex, and even if it were accomplished, the effort that went into the proof could not be reused. As this example shows, the sensible approach is to prove the theorem with an abstract model, then verify that the real network satisfies the straightforward assumptions in the proof. + +## Network Properties + +In summary, the common theme of these verification experiments is that they reveal a much richer set of network properties than usually seen in the literature on network verification. This is because the structure and modularity of CNA make it possible to get closer to the purposes and specializations of each network, without having them obscured by the overall complexity of a set of composed networks. Access to this kind of design detail provides understanding, not only of the many properties that make designs work, but also of the practical constraints that make the properties hold. + +[1] Pamela Zave, Jennifer Rexford, John Sonchack, "The remaining improbable: Toward verifiable network services," https://arxiv.org/abs/2009.12861, 2020. diff --git a/assets/images/cnaPic.png b/assets/images/cnaPic.png new file mode 100644 index 0000000..3dac57d Binary files /dev/null and b/assets/images/cnaPic.png differ diff --git a/assets/images/cnavPic.png b/assets/images/cnavPic.png new file mode 100644 index 0000000..6518ae0 Binary files /dev/null and b/assets/images/cnavPic.png differ diff --git a/assets/images/jennifer-rexford.jpg b/assets/images/jennifer-rexford.jpg new file mode 100644 index 0000000..4b49e57 Binary files /dev/null and b/assets/images/jennifer-rexford.jpg differ diff --git a/assets/images/pamela-zave.jpg b/assets/images/pamela-zave.jpg new file mode 100644 index 0000000..9639c4c Binary files /dev/null and b/assets/images/pamela-zave.jpg differ diff --git a/assets/images/provider-network.png b/assets/images/provider-network.png new file mode 100644 index 0000000..84a4b90 Binary files /dev/null and b/assets/images/provider-network.png differ diff --git a/assets/images/subduction.png b/assets/images/subduction.png new file mode 100644 index 0000000..a6516c7 Binary files /dev/null and b/assets/images/subduction.png differ diff --git a/assets/images/vpn.png b/assets/images/vpn.png new file mode 100644 index 0000000..c82aa4a Binary files /dev/null and b/assets/images/vpn.png differ