Projects

Current Projects

NetSketch

Students: Vatche Ishakian, Nate Soule, Saber Mirzaei
Postdocs: Andrei Lapets
PIs: Azer Bestavros, Assaf Kfoury

NetSketch is a tool that enables the specification of network-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system so as to retain sufficient enough details to enable future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing trade-offs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis approach based on a strongly typed, Domain-Specific Language (DSL) to specify network configurations at various levels of sketchiness along with invariants that need to be enforced thereupon.

A web based implementation of a subset of NetSketch is available here: http://csr.bu.edu/netsketch/.

Software Inspection and Certificate Service (SICS)

Postdocs: Mark C. Reynolds
PIs: Azer Bestavros, Assaf Kfoury

The SICS project uses formal methods to search for security vulnerabilities in bytecode languages such as Java, Flash and Dalvik (Android). A formal security model is created for each language using either Alloy or Isabelle/HOL. A piece of software under test is then translated into model statements in the corresponding language. When the security specification and code-specific model fragments are combined, a model checker can then be used to search for counterexamples. Such counterexamples always represent violations of the security rules.

aartifact

Postdocs: Andrei Lapets
PIs: Assaf Kfoury, Azer Bestavros

The aartifact project is an effort to construct an infrastructure for quickly developing accessible integrated formal reasoning environments that incorporate multiple underlying algorithms and formal reasoning, analysis, and verification tools. The website for the project is available here: http://www.aartifact.org.

Past 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.


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

SlurpCast is a media streaming server that is written in O'Caml, a type-checked, memory-safe functional language. O'Caml is chosen because it  offers the choice of functional-style programming and imperative-style  programming, and partly also because O'Caml is well-supported by its  community. This project is an attempt to see how much functional  programming constructs can be used to model a network server architecture. Combinator functions are designed and used extensively in SlurpCast to accommodate the extensibility and flexibility needs of a modular server. SlurpCast also adopts synchronized queue and thread communication from imperative programming concepts.
Comments