List of Publications

Presentations

[ Liu07 ]

Likai Liu. Verification of Network Flows Using a Type System with Constrained Polymorphism. Presented at NEPLS, Tufts University, April 11, 2007 [PDF] [BibTeX] [Abstract]

Abstract

We propose a typed domain-specific language TRAFFIC(X) for the specification and analysis of end-to-end network flow configurations. TRAFFIC(X) is inspired by HM(X), a framework that augments the familiar Hindley-Milner polymorphic type system for ML-like functional languages with a constraint system X. In TRAFFIC(X), the constraint system X can be instantiated to different constraint-rewriting rules, corresponding to the verification of different properties of network flows. To illustrate our methodology, we examine two examples: (1) proper nesting of tunneled streams by means of lossy or lossless compression and encryption; and (2) computing round-trip time using linear-programming constraints.

[close]

[ Best06 ]

Azer Bestavros. Type-disciplined, Scalable, Practical Composition of Networked Services. Presented at NRG, BU CS Department, March 13, 2006 [PDF] [BibTeX]

Papers

[ BUCS-TR-2006-029 ]

Likai Liu and Assaf Kfoury. Safe Compositional Specification of Network Systems With Polymorphic, Constrained Types. Technical Report BUCS-TR-2006-029, Computer Science Department, Boston University, Boston, MA, October 25, 2006 [PDF] [PS] [BibTeX] [Abstract]

Abstract

In the framework of iBench research project, our previous work created a domain specific language TRAFFIC [BUCS-TR-2005-015] that facilitates specification, programming, and maintenance of distributed applications over a network. It allows safety property to be formalized in terms of types and subtyping relations. Extending upon our previous work, we add Hindley-Milner style polymorphism [Milner:JCSS-1978-v17] with constraints [Odersky:TPOS-1999-v5] to the type system of TRAFFIC. This allows a programmer to use for-all quantifier to describe types of network components, escalating power and expressiveness of types to a new level that was not possible before with propositional subtyping relations. Furthermore, we design our type system with a pluggable constraint system, so it can adapt to different application needs while maintaining soundness.

In this paper, we show the soundness of the type system, which is not syntax-directed but is easier to do typing derivation. We show that there is an equivalent syntax-directed type system, which is what a type checker program would implement to verify the safety of a network flow. This is followed by discussion on several constraint systems: polymorphism with subtyping constraints, Linear Programming, and Constraint Handling Rules (CHR) [Fruhwirth:JLP-1998-v37]. Finally, we provide some examples to illustrate workings of these constraint systems.

[close]

[ BUCS-TR-2005-034 ]

Yarom Gabay, Assaf Kfoury, Likai Liu, Azer Bestavros, Adam Bradley, and Ibrahim Matta. Type Systems for a Network Specification Language With Multiple-Choice Let. Technical Report BUCS-TR-2005-034, Computer Science Department, Boston University, Boston, MA, December 28, 2005 [PDF] [PS] [BibTeX] [Abstract]

Abstract

When analysing the behavior of complex networked systems, it is often the case that some components within that network are only known to the extent that they belong to one of a set of possible “implementations”—e.g., versions of a specific protocol, class of schedulers, etc. In this report we augment the specification language considered in [BUCS-TR-2004-021], [BUCS-TR-2005-014], [BUCS-TR-2005-015], and [BUCS-TR-2005-033], to include a non-deterministic multiple-choice let-binding, which allows us to consider compositions of networking subsystems that allow for looser component specifications.

[close]

[ BUCS-TR-2005-033 ]

Likai Liu, Assaf Kfoury, Azer Bestavros, Yarom Gabay, Adam Bradley, and Ibrahim Matta. Safe Compositional Specification of Networking Systems: A Compositional Analysis Approach. Technical Report BUCS-TR-2005-033, Computer Science Department, Boston University, Boston, MA, December 28, 2005 [PDF] [PS] [BibTeX] [Abstract]

Abstract

We present a type inference algorithm, in the style of compositional analysis, for the language TRAFFIC—a specification language for flow composition applications proposed in [BUCS-TR-2005-014]—and prove that this algorithm is correct: the typings it infers are principal typings, and the typings agree with syntax-directed type checking on closed flow specifications. This algorithm is capable of verifying partial flow specifications, which is a significant improvement over syntax-directed type checking algorithm presented in [BUCS-TR-2005-015]. We also show that this algorithm runs efficiently, i.e., in low-degree polynomial time.

[close]

[ BUCS-TR-2005-015 ]

Likai Liu, Assaf Kfoury, Azer Bestavros, Adam Bradley, Yarom Gabay, and Ibrahim Matta. Safe Compositional Specification of Networking Systems: {TRAFFIC} The Language and Its Type Checking. Technical Report BUCS-TR-2005-015, Computer Science Department, Boston University, Boston, MA, May 12, 2005 [PDF] [PS] [BibTeX] [Abstract]

Abstract

This paper formally defines the operational semantic for TRAFFIC, a specification language for flow composition applications proposed in [BUCS-TR-2005-014], and presents a type system based on desired safety assurance. We provide proofs on reduction (weak-confluence, strong-normalization and unique normal form), on soundness and completeness of type system with respect to reduction, and on equivalence classes of flow specifications. Finally, we provide a pseudo-code listing of a syntax-directed type checking algorithm implementing rules of the type system capable of inferring the type of a closed flow specification.

[close]

[ BBKM:ICNP05 ]

Azer Bestavros, Adam Bradley, Assaf Kfoury, and Ibrahim Matta. Typed Abstraction of Complex Network Compositions. In Proceedings of ICNP\'05: The 13th IEEE International Conference on Network Protocols, Boston, MA, November, 2005 [PDF] [PS] [BibTeX] [Abstract]

Abstract

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.

[close]

[ BUCS-TR-2004-021 ]

Azer Bestavros, Adam Bradley, Assaf Kfoury, and Ibrahim Matta. Safe Compositional Specification of Networking Systems. Technical Report BUCS-TR-2004-021, Computer Science Department, Boston University, Boston, MA, May 14, 2004 [PDF] [PS] [BibTeX] [Abstract]

Abstract

The Science of Network Service Composition has clearly emerged as one of the grand themes driving many of our research questions in the networking field today [NeXtworking 2003]. This driving force stems from the rise of sophisticated applications and new networking paradigms. By “service composition” we mean that the performance and correctness properties local to the various constituent components of a service can be readily composed into global (end-to-end) properties without re-analyzing any of the constituent components in isolation, or as part of the whole composite service. The set of laws that would govern such composition is what will constitute that new science of composition. The combined heterogeneity and dynamic open nature of network systems makes composition quite challenging, and thus programming network services has been largely inaccessible to the average user. We identify (and outline) a research agenda in which we aim to develop a specification language that is expressive enough to describe different components of a network service, and that will include type hierarchies inspired by type systems in general programming languages that enable the safe composition of software components. We envision this new science of composition to be built upon several theories (e.g., control theory, game theory, network calculus, percolation theory, economics, queuing theory). In essence, different theories may provide different languages by which certain properties of system components can be expressed and composed into larger systems. We then seek to lift these lower-level specifications to a higher level by abstracting away details that are irrelevant for safe composition at the higher level, thus making theories scalable and useful to the average user.

In this paper we focus on services built upon an overlay management architecture, and we use control theory and QoS theory as example theories from which we lift up compositional specifications.

[close]