Validating Arbitrarily Large Network Protocol Compositions with Finite Computation

Formal tools like finite-state model checkers have proven useful in verifying the correctness of systems of bounded size and for hardening single system components against arbitrary inputs. However, conventional applications of these techniques are not well suited to characterizing emergent behaviors of large compositions of processes. In this paper, we present a methodology by which arbitrarily large compositions of components can, if sufficient conditions are proven concerning properties of small compositions, be modeled and completely verified by performing formal verifications upon only a finite set of compositions. The sufficient conditions take the form of reductions, which are claims that particular sequences of components will be causally indistinguishable from other shorter sequences of components. We show how this methodology can be applied to a variety of network protocol applications, including two features of the HTTP protocol, a simple active networking applet, and a proposed web cache consistency algorithm. We also doing discuss its applicability to framing protocol design goals and to representing systems which employ non-model-checking verification methodologies. Finally, we briefly discuss how we hope to broaden this methodology to more general topological compositions of network applications.

Lightweight Formal Methods for the Development of High-Assurance Networking Systems

We survey several of the research efforts pursued by the iBench and snBench projects in the CS Department at Boston University over the last half dozen years. These activities use ideas and methodologies inspired by recent developments in other parts of computer science -- particularly in formal methods and in the foundations of programming languages -- but now specifically applied to the certification of safety-critical networking systems. This is research jointly led by Azer Bestavros and Assaf Kfoury with the participation of Adam Bradley, Andrei Lapets, and Michael Ocean.

Changes in Web Client Access Patterns: Characteristics and Caching Implications

Understanding the nature of the workloads and system demands created by users of the World Wide Web is crucial to properly designing and provisioning Web services. Previous measurements of Web client workloads have been shown to exhibit a number of characteristic features; however, it is not clear how those features may be changing with time. In this study we compare two measurements of Web client workloads separated in time by three years, both captured from the same computing facility at Boston University. The older dataset, obtained in 1995, is well-known in the research literature and has been the basis for a wide variety of studies. The newer dataset was captured in 1998 and is comparable in size to the older dataset. The new dataset has the drawback that the collection of users measured may no longer be representative of general Web users; however using it has the advantage that many comparisons can be drawn more clearly than would be possible using a new, different source of measurement. Our results fall into two categories. First we compare the statistical and distributional properties of Web requests across the two datasets. This serves to reinforce and deepen our understanding of the characteristic statistical properties of Web client requests. We find that the kinds of distributions that best describe document sizes have not changed between 1995 and 1998, although specific values of the distributional parameters are different. Second, we explore the question of how the observed differences in the properties of Web client requests, particularly the popularity and temporal locality properties, affect the potential for Web file caching in the network. We find that for the computing facility represented by our traces between 1995 and 1998, (1) the benefits of using size-based caching policies have diminished; and (2) the potential for caching requested files in the network has declined.

BU Computer Science 1998 Proxy Trace: Release Notes

In a recent paper (Changes in Web Client Access Patterns: Characteristics and Caching Implications by Barford, Bestavros, Bradley, and Crovella) we performed a variety of analyses upon user traces collected in the Boston University Computer Science department in 1995 and 1998. A sanitized version of the 1995 trace has been publicly available for some time; the 1998 trace has now been sanitized, and is available from: http://www.cs.bu.edu/techreports/1999-011-usertrace-98.gz ftp://ftp.cs.bu.edu/techreports/1999-011-usertrace-98.gz This memo discusses the format of this public version of the log, and includes additional discussion of how the data was collected, how the log was sanitized, what this log is and is not useful for, and areas of potential future research interest.

Typed Abstraction of Complex Network Compositions

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.

Safe Compositional Specification of Networking Systems: TRAFFIC The Language and Its Type Checking

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.

Safe Compositional Specification of Networking Systems: A Compositional Analysis Approach

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 [2]—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 [3]. We also show that this algorithm runs efficiently, i.e., in low-degree polynomial time.

Type Systems for a Network Specification Language With Multiple-Choice Let

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

Inferring Intersection Typings that are Equivalent to Call-by-Name and Call-by-Value Evaluations

We present a procedure to infer a typing for an arbitrary λ-term M in an intersection-type system that translates into exactly the call-by-name (resp., call-by-value) evaluation of M. Our framework is the recently developed System E which augments intersection types with expansion variables. The inferred typing for M is obtained by setting up a unification problem involving both type variables and expansion variables, which we solve with a confluent rewrite system. The inference procedure is compositional in the sense that typings for different program components can be inferred in any order, and without knowledge of the definition of other program components. Using expansion variables lets us achieve a compositional inference procedure easily. Termination of the procedure is generally undecidable. The procedure terminates and returns a typing if the input M is normalizing according to call-by-name (resp., call-by-value). The inferred typing is exact in the sense that the exact call-by-name (resp., call-by-value) behaviour of M can be obtained by a (polynomial) transformation of the typing. The inferred typing is also principal in the sense that any other typing that translates the call-by-name (resp., call-by-value) evaluation of M can be obtained from the inferred typing for M using a substitution-based transformation.

An investigation of innovation and knowledge creation in virtual worlds

The Internet and World Wide Web have had, and continue to have, an incredible impact on our civilization. These technologies have radically influenced the way that society is organised and the manner in which people around the world communicate and interact. The structure and function of individual, social, organisational, economic and political life begin to resemble the digital network architectures upon which they are increasingly reliant. It is increasingly difficult to imagine how our ‘offline’ world would look or function without the ‘online’ world; it is becoming less meaningful to distinguish between the ‘actual’ and the ‘virtual’. Thus, the major architectural project of the twenty-first century is to “imagine, build, and enhance an interactive and ever changing cyberspace” (Lévy, 1997, p. 10). Virtual worlds are at the forefront of this evolving digital landscape. Virtual worlds have “critical implications for business, education, social sciences, and our society at large” (Messinger et al., 2009, p. 204). This study focuses on the possibilities of virtual worlds in terms of communication, collaboration, innovation and creativity. The concept of knowledge creation is at the core of this research. The study shows that scholars increasingly recognise that knowledge creation, as a socially enacted process, goes to the very heart of innovation. However, efforts to build upon these insights have struggled to escape the influence of the information processing paradigm of old and have failed to move beyond the persistent but problematic conceptualisation of knowledge creation in terms of tacit and explicit knowledge. Based on these insights, the study leverages extant research to develop the conceptual apparatus necessary to carry out an investigation of innovation and knowledge creation in virtual worlds. The study derives and articulates a set of definitions (of virtual worlds, innovation, knowledge and knowledge creation) to guide research. The study also leverages a number of extant theories in order to develop a preliminary framework to model knowledge creation in virtual worlds. Using a combination of participant observation and six case studies of innovative educational projects in Second Life, the study yields a range of insights into the process of knowledge creation in virtual worlds and into the factors that affect it. The study’s contributions to theory are expressed as a series of propositions and findings and are represented as a revised and empirically grounded theoretical framework of knowledge creation in virtual worlds. These findings highlight the importance of prior related knowledge and intrinsic motivation in terms of shaping and stimulating knowledge creation in virtual worlds. At the same time, they highlight the importance of meta-knowledge (knowledge about knowledge) in terms of guiding the knowledge creation process whilst revealing the diversity of behavioural approaches actually used to create knowledge in virtual worlds and. This theoretical framework is itself one of the chief contributions of the study and the analysis explores how it can be used to guide further research in virtual worlds and on knowledge creation. The study’s contributions to practice are presented as actionable guide to simulate knowledge creation in virtual worlds. This guide utilises a theoretically based classification of four knowledge-creator archetypes (the sage, the lore master, the artisan, and the apprentice) and derives an actionable set of behavioural prescriptions for each archetype. The study concludes with a discussion of the study’s implications in terms of future research.

Molecular analysis of virulence mechanisms associated with adherent-invasive Escherichia coli (AIEC)

Crohn's Disease (CD) is a chronic inflammatory bowel disease of unknown etiology. Recent work has shown that a new pathotype of Escherichia coli, Adherent Invasive E. coli (AIEC) may be associated with CD. AIEC has been shown to adhere to and invade epithelial cells and to replicate within macrophages (together this is called the AIEC phenotype). In this thesis, the AIEC phenotype of 84 E. coli strains were determined in order to identify the prevalence of this phenotype within the E. coli genus. This study showed that a significant proportion of E. coli strains (approx. 5%) are capable of adhering to and invading epithelial cells and undergoing intramacrophage replication. Moreover, the results presented in this study indicate a correlation between survival in macrophage and resistance to grazing by amoeba supporting the coincidental evolution hypothesis that resistance to amoebae could be a driving force in the evolution of pathogenicity in some bacteria, such as AIEC. In addition, this study has identified an important regulatory role for the CpxA/R two component system (TCS) in the invasive abilities of AIEC HM605, a colonic mucosa-associated CD isolate. A mutation in cpxR was shown to be defective in the invasion of epithelial cells and this defect was shown to be independent of motility or the expression of Type 1 fimbriae, factors that have been shown to be involved in the invasion of another strain of AIEC, isolated from a patient with ileal CD, called LF82. The CpxA/R TCS responds to disturbances in the cell envelope and has been implicated in the virulence of a number of Gram negative pathogens. In this study it is shown that the CpxA/R TCS regulates the expression of a potentially novel invasin called SinH. SinH is found in a number of invasive strains of E. coli and Salmonella. Moreover work presented here shows that a critical mechanism underpinning AIEC persistence in macrophages is the repair of DNA bases damaged by macrophage oxidants. Together these findings provide evidence to suggest that AIEC are a diverse group of E. coli and possess diverse molecular mechanisms and virulence factors that contribute to the AIEC phenotype. In addition, AIEC may have gone through different evolutionary histories acquiring various molecular mechanisms ultimately culminating in the AIEC phenotype. The gastrointestinal (GI) tract harbors a diverse microbiota; most are symbiotic or commensal however some bacteria have the potential to cause disease (pathobiont). The work presented here provides evidence to support the model that AIEC are pathobionts. AIEC strains can be carried as commensals in healthy guts however, when the intestinal homeostasis is disrupted, such as in the compromised gut of CD patients, AIEC may behave as opportunistic pathogens and cause and/or contribute to disease by driving intestinal inflammation.