Safe Compositional Network Sketches: Tool & Use Cases
Azer Bestavros, Assaf J. Kfoury, Andrei Lapets, Michael J. Ocean · 2009
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 stronglytyped, 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 overview NetSketch, highlight its salient features, and illustrate how it could be used in applications, including the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications). In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch’s userinterface when used in “sketch mode”, and prove its soundness relative to appropriately-defined notions of validity. I. MOTIVATION AND SCOPE Traditionally, the design and implementation of trustworthy systems follows a bottom-up approach, enabling system designers and builders to certify (assert and assess) desirable safety invariants of the entire system in a wholistic manner. For example, the development of applications with predictable timing properties necessitated the use specialpurpose, real-time kernels so that timing properties at the application layer (top) could be established through knowledge and/or tweaking of much lower-level kernel details (bottom), such as worst-case context switching times, specific scheduling parameters, among many others. While justifiable in some instances, this bottom-up, vertical approach to establishing trust does not lend itself well to current practices in the assembly of complex, large-scale systems – namely, the integration of various subsystems into a whole by “system integrators” who may not necessarily possess the requisite expertise (or knowledge of) the internals of the subsystems they rely on. This horizontal approach to system design and development has significant merits with respect to scalability and modularity, but at the same time it poses significant challenges with respect to aspects of trustworthiness – namely, certifying that the system as a whole will satisfy specific invariants (e.g., related to safety, security, and timeliness). While it is possible to reason about and/or automatically infer the exact (tight) conditions under which safety constraints are satisfied for small-scale (toy), fully-specified subsystems, the same cannot be expected for large-scale, complex systems. Thus, in that context, we recognize three specific challenges that the work we present in this paper aims to mitigate. Exposing Tradeoffs: The environments and tools supporting large-scale system integrators must expose the inherent tradeoff between the exactness of safety analysis with respect to the specifity of the underlying subsystems, and the computational complexity necessary for automated analysis. For example, it should be possible for a system integrator to under-specify, or sketch whatever guarantees or constraints are expected to hold in a subsystem, and yet expect a level of support for system-wide safety analysis that is commensurate with the provided details. Such a capability would enable system integrators to establish “minimal” subsystem requirements for system-wide safety properties to hold. Similarily, it should be possible for a system integrator to escalate the automated analysis of safety properties based on the computational cost of such an analysis, perhaps opting for sketchier but cheaper analysis for less critical functionalities (or early on in the design phase). Lowering the Bar: Support for safety analysis in design and/or development environments must be based on sound formalisms that are not specific to (and do not require deep knowledge of) particular domain expertise. As we alluded earlier, while acceptable and perhaps expected for verticallydesigned, smaller-scale (sub)systems, deep domain expertise cannot be assumed for designers of horizontally-integrated, large-scale systems. Not only should the underlying formalism be domain-agnostic, but also it must be possible for the formalism to act as a unifying glue across multiple theories and calculi. In particular, such a formalism should enable system integrators to manipulate results obtained through multiple, less accessible domain-specific expertise (e.g., using network calculus to obtain worst-case delay envelopes, using scheduling theory to derive upper bounds on resource utilizations, or using queuing theory to derive steady-state average delays). In doing so, we lower the bar of expertise required to take full advantage of such domainspecific results at the small (subsystem) scale, while at the same time enabling scalability of safety analysis at the large (system) scale. Enabling Compositional Network Flow Analysis: Most large-scale systems are modeled/viewed as interconnections of subsystems, or gadgets, each of which is a producer, consumer, or otherwise a regulator of flows that are characterized by a set of variables and a set of constraints thereof, reflecting inherent or assumed properties or rules for how the gadgets operate (and what constitutes safe operation). In a way, we argue that system integration can be seen primarily as a network flow management exercise, and consequently that tools developed to assist in modeling and/or analysis recognize and leverage this view by enabling compositional analysis of networks of gadgets to allow for checking of safety properties or for the inference of conditions or constraints under which safe operation can be guaranteed. Towards the above-mentioned goals, in this paper we propose a methodology for the specification and analysis of large network flow systems. In section II, we highlight the prominent features of this methodology and of the formalism upon which it is based. Next, in Section III, we present a design (modeling and analysis) tool, called NetSketch, which we have developed in support of this methodology. In Sections V and VI, we present two illustrative use cases of the tool for shaping vehicular traffic networks and streaming video networks, respectively. We conclude the paper with a review of the related literature in Section VII and with a summary of current and future work in Section VIII. II. THE NETSKETCH FRAMEWORK AND FORMALISM In this section, we overview the salient features and the formal underpinnings of NetSketch. A significantly more detailed treatment of the formalism underlying NetSkecth (including proof of its soundness) is presented in a companion paper [1]. Compositional Analysis in NetSketch: As a tool, NetSketch supports compositional (in contrast to whole-system) analysis, which is additionally incremental (distributed in time) and modular (distributed in space). Schematically and somewhat simplistically, we can constrast whole-system and compositional analyses according to Figure 1, where “ [ [x ] ] ” denotes “the analysis of object x”, “⌦” an associative operation for connecting two components of a larger network, and “?” an associative operation for combining two analyses. Here it is important to note that for an analysis to be compositional, it must allow inter-checking of gadgets to happen in any order, thus enabling more flexible patterns of development and update. This stands in sharp contrast to modular analysis, which may prescribe a particular order in which the modules have to be analyzed.1 Analysis of Incomplete or Sketchy Specifications: By its nature, whole-system analysis cannot be undertaken if a gadget (such as B in Figure 1) is missing or if it breaks down (indicated by the double question marks “??”). Moreover, if the missing gadget is to be replaced by a new one (B0 in Figure 1), whole-system analysis must be delayed until the new gadget becomes available for examination and then the entire network must be re-analyzed from scratch. If we are interested in certifying that a particular invariant is preserved throughout the network without running into the limitations of whole-system analysis – specifically, inability to deal with 1A good example of the difference between modular and compositional analysis is provided by type inference for ML-like functional languages. Type inference is a particular way of analyzing programs statically, one of several closely related approaches available today. ML-like type inference is modular but not compositional. Gadgets Whole-system vs Compositional analysis A [ [ A ] ] = [ [ A ] ] A ⌦ B [ [ A ⌦ B ] ] = [ [ A ] ] ? [ [ B ] ] A ⌦ B ⌦ C [ [ A ⌦ B ⌦ C ] ] = [ [ A ] ] ? [ [ B ] ] ? [ [ C ] ] A ⌦ h i ⌦ C [ [ A ⌦ h i ⌦ C ] ] ?? ? = [ [ A ] ] ? [ [ h i ] ] ? [ [ C ] ] A ⌦ B ⌦ C [ [ A ⌦ B ⌦ C ] ] = [ [ A ] ] ? [ [ B ] ] ? [ [ C ] ]