The heterogeneity and open nature of network systems make analysis of compositions of components quite challenging, making the design and implementation of robust network services largely inaccessible to the average programmer. We propose the development of a novel type system and practical type spaces which reflect simplified representations of the results and conclusions which can be derived from complex compositional theories in more accessible ways, essentially allowing the system architect or programmer to be exposed only to the inputs and output of compositional analysis without having to be familiar with the ins and outs of its internals. Toward this end, we present the TRAFFIC (typed representation and analysis of flows for interoperability checks) framework, a simple flow-composition and typing language with corresponding type system. We then discuss and demonstrate the expressive power of a type space for TRAFFIC derived from the network calculus, allowing us to reason about and infer such properties as data arrival, transit, and loss rates in large composite network applications

Documentation of the HTTP protocol includes precise descriptions of the syntax of the protocol, but lacks similarly precise specification of the semantics of messages and message bodies. Semantics are stated in English prose; while this makes the document more intuitively accessible, it makes any sort of formal claims of correctness or interoperability difficult to derive from the specification itself. We propose "layered types", a formal description of the interpretive semantics of HTTP message bodies based upon the stacked type syntax. This model allows us to formally declare semantics for content-related HTTP headers and offers a precise way of characterizing interoperability between current and future protocol revisions and extensions.

Formal correctness of complex multi-party protocols can be difficult to verify. While models of specific sign constraints, protocols which lend themselves to arbitrarily many compositions of agents -such as the chaining of proxies or the peering of routers- are more difficult to verify because they represent potentially infinite state spaces and may exhibit emergent behaviors which may not materialize under particular fixed compositions. We address this challenge by developing an algebraic approach that enables us to reduce arbitrary compositions of network agents into a behaviorally-equivalent (with respect to some correctness property) compact, conical representation, which is amenable to mechanical verification. Our approach consists of an algebra and a set of property-preserving rewrite rules for the canonical homomorphic abstraction of infinite network protocol composition (CHAIN). Using CHAIN, an expression over our algebra (i.e., a set of configurations of network protocol agents) can be reduced to another behaviorally-equivalent expression (i.e., a smaller set of configurations). Repeated applications of such rewrite rules produce a canonical expression which can be checked mechanically. We demonstrate our approach by characterizing deadlock-prone configurations of HTTP agents, as well as establishing useful properties of an overlay protocol for scheduling MPEG frames, and of a protocol for Web intracache consistency.

With Web caching and cache-related services like CDNs and edge services playing an increasingly significant role in the modern Internet, the problem of the weak consistency and coherence provisions in current Web protocols is drawing increasing attention. Toward this end, we differentiate definitions of consistency and coherence for Web-like caching environments, and then present a novel Web protocol we call "basis token consistency" (BTC). This protocol allows compliant caches to guarantee strong consistency of content retrieved from supporting servers. We then compare the performance of BTC with the traditional TTL (time to live) algorithm under a range of synthetic workloads in order to illustrate its qualitative performance properties.