Safe compositional network sketches: NetSketch tool implementation

Date
2011-02-08
DOI
Authors
Soule, Nate
Bestavros, Azer
Kfoury, Assaf
Lapets, Andrei
Version
OA Version
Citation
Soule, Nate; Bestavros, Azer; Kfoury, Assaf; Lapets, Andrei. "Safe Compositional Network Sketches: NetSketch Tool Implementation", Technical Report BUCS-TR-2011-004, Computer Science Department, Boston University, February 8, 2011. [Available from: http://hdl.handle.net/2144/11361]
Abstract
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 tradeoffs 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. In this paper we discuss a first implementation of the NetSketch system. We begin with a brief introduction to the NetSketch concept and formalism, and then discuss the methodology behind the type generation process as well as the technical implementation of the overall system. In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch’s user interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity.
Description
License