Current Projects

TRAFFIC

Students: Likai Liu
PIs: Azer Bestavros, Assaf Kfoury, and Ibrahim Matta

In this project we introduce a novel type system and associated type spaces, which constitute accessible representations of the results and conclusions that are derivable using complex compositional theories. These representations allow a networking 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 propose TRAFFIC (Typed Representation and Analysis of network Flows For Interoperability Checks) framework, a simple flow-composition and typing language. TRAFFIC could be incorporated with one or more underlying theory for the purpose of establishing safety properties of large compositions. An example theory that we have incorporated with TRAFFIC is  the Network Calculus, which allows us to reason about and infer such properties as data arrival, transit, and loss rates in large composite network applications. The TRAFFIC compositional analysis framework is put in action through a prototype implementation of a type checking and inference engine, which is available for demonstration purposes using a web interface.

snBench

Students: Michael Ocean
PI: Azer Bestavros and Assaf Kfoury

The snBench project aims to design and implement the programming and run-time infrastructure necessary for developers to specify and deploy truly distributed applications over a heterogeneous network of Sensing Elements (SEs) and of Computing Elements (CEs). snBench offers the means via which applications may (1) locate, monitor, and query SEs and CEs for services they support, and (2) initiate, control, or otherwise use such SE and CE services. In addition to supporting these functionalities, the snBench will provide basic run-time resource management services for QoS support, including real-time scheduling and admission control functionalities. While the architecture of the system and most of its services will be targeted at generic sensing modalities, our immediate target will be the Sensorium infrastructure--namely a network of fixed video cameras of various capabilities used for monitoring and tracking purposes. To that end, the basic set of SE services to be made available to distributed applications will include 'atomic' video operations (e.g., video frame capture, blob counting, motion detection, tracking, among others) whereas the basic set of CE services to be made available to distributed applications will include in-network stream aggregation services (e.g., concasting coordinates of detected features, real-time stitching of frames from multiple vantage points, among others). One of the salient features of snBench is extensibility. To that end, snBench will provide a type-disciplined framework for defining and adding new services--both atomic services at SEs and compositional services at CEs.

Past Projects

itmBench

PIs: Ibrahim Matta and Azer Bestavros

Internet Traffic Managers (ITMs) are special machines placed at strategic places in the Internet. itmBench is an programming interface that allows users (e.g. network managers, service providers, or experimental researchers) to register different traffic control functionalities to run on one ITM or an overlay of ITMs. Thus itmBench could be viewed as a tool that is extensible and powerful yet easy to maintain. ITM traffic control applications could be developed either using a kernel API so they run in kernel space, or using a user-space API so they run in user space. We have demonstrated the flexibility of itmBench by showing the implementation of both a kernel module that provides a differentiated network service, and a user-space module that provides an overlay routing service. Other uses of itmBench for prototyping overlay routing services and overlay traffic management are also on-going.  Our itmBench Linux-based prototype is free software and can be obtained from http://www.cs.bu.edu/groups/itm/.

StaXML

Student: Adam Bradley
PIs: Azer Bestavros and Assaf Kfoury

STAXML is a type system for the static verification of imperative script output to ensure it conforms to XML (or to particular XML applications). The StaXML type systems allow program expressions to be statically typed with respect to their role in the structure of XML-based output languages. Unlike similar projects which support strong XML-typing of program output, StaXML does not impose a functional programming style upon the programmer; thus, it supports traditional web scripting idioms in which document content is progressivelt written to the output stream as a sequence of strings. By typing strings using the stacked type syntax and transforming the XML language's syntax into normalizations which can be applied to those stacks, we are able to capture several degrees of XML well-formedness in a compile-time type system; by further specializing these normalizations to particular XML schemata, we are also able to enforce correct element structure for particular applications of XML such as the XHTML language. This project includes "StaXML for PHP", an implementation of the various StaXML type systems for the popular PHP4 scripting language. We have a working pre-compiler which supports application of several StaXML type systems to most of the core features of the PHP language, and is available for public use via a web gateway.

CHAIN

Students: Adam Bradley
PIs: Azer Bestavros and Assaf Kfoury

Formal correctness of complex multi-party network protocols can be difficult to verify. While models of specific fixed compositions of agents can be checked against design 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 that 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, canonical 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 compositions (CHAIN). Using CHAIN, an expression over our algebra (i.e., a set of configurations of network protocol agents) could be reduced to another behaviorally-equivalent expression (i.e., a smaller set of configurations). Repeated applications of such rewrite rules produces a canonical expression which can be checked mechanically. CHAIN has been applied successfully to the verification of a number of network protocols, including  the characterizing of deadlock-prone configurations in HTTP, the establishment of useful properties of an overlay network protocol for scheduling MPEG frames, and the verification of a protocol for Web intra-cache consistency.

SlurpCast

Student: Likai Liu
PIs:  Assaf Kfoury, and Hongwei Xi