Search

When machine learning (ML) models are used in safety-critical or mission-critical applications (e.g., self driving cars, cyber security, surgical robotics), it is important to ensure that they provide some high-level guarantees (e.g., safety, liveness). We introduce a paradigm called Trusted Machine Learning (TML) for making ML models more trustworthy. We use Markov Decision Processes (MDPs) as the underlying dynamical model and outline three TML approaches: (1) Model Repair, wherein we modify the learned model directly; (2) Data Repair, wherein we modify the data so that re-learning from the modified data results in a trusted model; and (3) Reward Repair, wherein we modify the reward function of the MDP to satisfy the specified logical constraint. We show how these repairs can be done efficiently for probabilistic models (e.g., MDP) when the desired properties are expressed in some appropriate fragment of logic such as temporal logic (for example PCTL, i.e., Probabilistic Computation Tree Logic), first order logic or propositional logic. We illustrate our approaches on case studies from multiple domains, e.g., car controller for obstacle avoidance, and a query routing controller in a wireless sensor network.

Experimenting with futuristic computer workstation design and specifically tailored application models can yield useful insights and result in exciting ways to increase efficiency, effectiveness, and satisfaction for computer users. Designing and building a computer workstation that can track a user’s gaze; sense proximity to the touch surface; and support multi-touch, face recognition etc meant overcoming some unique technological challenges. Coupled with extensions to commonly used applications to report user interactions in a meaningful way, the workstation will allow the development of a rich contextual user model that is accurate enough to enable benefits, such as contextual filtering, task automation, contextual auto-fill, and improved understanding of team collaborations. SRI’s bRIGHT workstation was designed and built to explore these research avenues and investigate how such a context model can be built, identify the key implications in designing an application model that best serves these goals, and discover other related factors. This paper conjectures future research that would support the development of a collaborative context model that could leverage similar benefits for groups of users.

We formalize the Dolev-Yao model of security protocols, using a notation based on multiset rewriting with existentials. The goals are to provide a simple formal notation for describing security protocols, to formalize the assumptions of the Dolev-Yao model using this notation, and to analyze the complexity of the secrecy problem under various restrictions. We prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP-complete class when the number of nonces is restricted, and an NP-complete class when both the number of nonces and the number of roles is restricted. We point out a remaining open complexity problem, and discuss the implications these results have on the general topic of protocol analysis.

The goal of the BioSPICE program is to create a framework that provides biologists access to the most current computational tools. At the program midpoint, the BioSPICE member community has produced a software system that comprises contributions from approximately 20 participating laboratories integrated under the BioSPICE Dashboard and a methodology for continued software integration. These contributed software modules are the BioSPICE Dashboard, a graphical environment that combines Open Agent Architecture and NetBeans software technologies in a coherent, biologist-friendly user interface. The current Dashboard permits data sources, models, simulation engines, and output displays provided by different investigators and running on different machines to work together across a distributed, heterogeneous network. Among several other features, the Dashboard enables users to create graphical workflows by configuring and connecting available BioSPICE components. Anticipated future enhancements to BioSPICE include a notebook capability that will permit researchers to browse and compile data to support model building, a biological model repository, and tools to support the development, control, and data reduction of wet-lab experiments. In addition to the BioSPICE software products, a project website supports information exchange and community building.

Natural language (supplemented with diagrams and some mathematical notations) is convenient for succinct communication of technical descriptions between the various stakeholders (e.g., customers, designers, implementers) involved in the design of software systems. However, natural language descriptions can be informal, incomplete, imprecise and ambiguous, and cannot be processed easily by design and analysis tools. Formal languages, on the other hand, formulate design requirements in a precise and unambiguous mathematical notation, but are more difficult to master and use. We propose a methodology for connecting semi-formal requirements with formal descriptions through an intermediate representation. We have implemented this methodology in a research prototype called Automatic Requirements Specification Extraction from Natural Language (ARSENAL). The main novelty of ARSENAL lies in its ability to generate a fully-specified complete formal model automatically from natural language requirements. ARSENAL extracts relations from text using semantic parsing and progressively refines them over multiple stages to create a final composite model. Currently, ARSENAL generates formal models in linear-time temporal logic (LTL), but the approach can be adapted for other models, e.g., probabilistic relational models like Markov Logic Networks (MLN). The formal models of the requirements can be used to check important design and system properties, e.g., consistency, satisfiability, realizability. ARSENAL has a modular and flexible architecture that facilitates porting it from one domain to another. We evaluated ARSENAL on complex requirements from two real-world case studies: the Time-Triggered Ethernet (TTEthernet) communication platform used in space, and FAA-Isolette infant incubators used in NICU. We systematically evaluated various aspects of ARSENAL -- the accuracy of the natural language processing stage, the degree of automation, and robustness to noise.

The development of new classes of distributed applications such as telephony, remote video, and virtual reality introduces new quality requirements that make inadequate even the current best-effort service model provided by international networks. Recent research activity has proposed new approaches to accommodate these new application requirements. While exploiting the resource needs of different applications to use the network resources efficiently, these approaches require the maintenance of a considerable amount of state information at the network nodes. Correctness and availability of such information are the basic requirements for the proper working of the network. In this paper we present a system, called Global Infrastructure Protection System (GIPS), to control improper modifications to this state information. We illustrate the GIPS's architecture and identify topology conditions to guarantee the distributed fault tolerant detection of anomalies. The system is based on the use of a hierarchical structure to organize and maintain the information at each node. Improper network states are described through rules that characterize state information updates that may result anomalous (or uncommon) with respect to the network status, past events occurred, or statistical measures. We introduce a notation to represent state information coming from heterogeneous protocols, and statistical operators to examine the history of state updates accumulated during operation. Finally, we present some examples using our notation to express heuristical rules detecting anomalous operations in a network.

This paper introduces the basic concepts of the rewriting logic language Maude and discusses its implementation. Maude is a wide-spectrum language supporting formal specification, rapid prototyping, and parallel programming. Maude's rewriting logic paradigm includes the functional and object-oriented paradigms as sublanguages. The fact that rewriting logic is reflective leads to novel metaprogramming capabilities that can greatly increase software reusability and adaptability. Control of the rewriting computation is achieved through internal strategy languages defined inside the logic. Maude's rewrite engine is designed with the explicit goal of being highly extensible and of supporting rapid prototyping and formal methods applications, but its semi-compilation techniques allow it to meet those goals with good performance.

An emerging generation of mission-critical systems employs distributed, dynamically reconfigurable open architectures. These systems may include a variety of devices that sense and affect their environment and the configuration of the system itself. We call such systems Networked Cyber-Physical Systems (NCPS). NCPS can provide complex, situation-aware, and often critical services in applications such as distributed sensing and surveillance, crisis response, self-assembling structures or systems, networked satellite and unmanned vehicle missions, or distributed critical infrastructure monitoring and control. In this paper we lay out research directions centered around a new paradigm for the design of NCPS based on a notion of software fractionation that we are currently exploring which can serve as the basis for a new generation of runtime assurance techniques. The idea of software fractionation is inspired by and complementary to hardware fractionation -- the basis for the fractionated satellites of DARPA's F6 program. Fractionated software has the potential of leading to software that is more robust, leveraging both diversity and redundancy. It raises the level of abstraction at which assurance techniques are applied. We specifically propose research in just-in-time verification and validation techniques, which are agile -- adapting to changing situations and requirements, and efficient -- focusing on properties of immediate concern in the context of locally reachable states, thus largely avoiding the state space explosion problem. We propose an underlying reflective architecture that maintains models of itself, the environment, and the mission that is key for adaptation, verification, and validation.

A new generation of mission-critical systems is emerging that employs distributed, dynamically reconfigurable open architectures. These systems may include a variety of devices that sense and affect their environment and the configuration of the system itself. We call such systems Networked Cyber- Physical Systems (NCPS). NCPS can provide complex, situation-aware, and often critical services in applications such as distributed sensing and surveillance, crisis response, self-assembling structures or systems, networked satellite and unmanned vehicle missions, or distributed critical infrastructure monitoring and control. NCPS are of special interest to the Navy in view of the increasing need for coordination of a wide spectrum of maritime sensing and information gathering technologies, ranging from smart mobile buoys to autonomous underwater vehicles and their integration into a global network with maritime, space, and ground domains. NCPS must be reactive and maintain an overall situation, location, and time awareness that emerges from the exchange of knowledge. They must achieve system goals through local, asynchronous actions, using (distributed) control loops through which the environment provides essential feedback. They must deal with uncertainty and partial knowledge, and be capable of a wide spectrum of operations between autonomy and cooperation to adapt to resource constraints and disruptions in communication. General principles and tools are needed for building robust, effective NCPS. A key observation is that the current level of abstraction at which software and systems are designed is a barrier to innovation at the hardware and networking level and at the same time is not suitable to enable rapid design/deployment or distributed control of large-scale distributed software systems and in particular the flexibility, dynamically reconfigurable, mission-critical NCPS of the future.

The continued scaling of device dimensions is leading toward devices where only a handful of dopant atoms or charges can make the difference between a one and a zero in the of state of represented bit, by enhancing or depleting channel conduction. Thus very minor static imperfections in dopant distribution, dielectric properties, or device geometry, and dynamic conditions associated with heat, radiation, or aging can perturb a device out of specification and cause electrical errors. Thus we might expect to soon see devices with millions of static defects and thousands of soft errors in very short time periods. Both static defects and dynamic faults at these scales present huge challenges. Classical methods for fault or defect tolerance at a higher level of architecture (eg. N-modular-redundancy) can be impractically expensive, and some approaches to diagnosis and reconfiguration require immense reliable memories or impractical test and reconfiguration times. Efficient and effective means are needed that exploit structure inherent in one layer of architecture to provide key properties to enable reliable execution at other levels.

This chapter gives an overview of some application areas of rewriting logic and Maude, with pointers to papers and web sites where more information can be found. Some of the material is adapted, with some modifications and extensions, from [199, 3, 217]. Since Maude is a general-purpose declarative programming language, there is in principle no limit to the applications that could be developed using it. Therefore, the areas discussed, although quite diverse, are only a sample of types of applications for which Maude seems particularly well suited. But there are many others. For example, the availability of built-in internet sockets in Maude 2.2 (see Section 11.4.1) opens up interesting possibilities for a new style of declarative internet programming which have already begun to be exploited (see Chapter 16).

Technologies are now emerging to construct molecular-scale electronic wires and switches using bottom-up self-assembly. This opens the possibility of constructing nanoscale circuits and memories where active devices are just a few nanometers square and wire pitches may be on the order of ten nanometers. The features can be defined at this scale without using photolithography. The available assembly techniques have relatively high defect rates compared to conventional lithographic integrated circuits and can only produce very regular structures. Nonetheless, with proper memory organization, it is reasonable to expect these technologies to provide memory densities in excess of 10/sup 11/ b/cm/sup 2/ with modest active power requirements under 0.6 W/Tb/s for random read operations.

How do living cells compute and control themselves, and communicate with their environment? We describe the modeling and analysis of dynamic and reactive biological systems involving both discrete and continuous behaviors, to help begin to answer that question. Continuous components arise as differential equations specifying how the concentrations of various molecular species evolve over time. Discrete components of models of biological systems arise from state transitions (eg. from healthy to abnormal states), abstractions and approximations, nonlinear effects, and the presence of inherently discrete processes, often observed in systems governed by one or a few molecules. Once a hybrid model is obtained, analysis techniques such as those described in this and previous HSCC workshops can be usefully applied to help uncover structure in the dynamics of biological systems of interest.

A scalable and expressive peer-to-peer (P2P) networking and computing framework requires efficient resource discovery services. Here we propose NEVRLATE, for Network-Efficient Vast Resource Lookup At The Edge, an efficient organization of directories or directory mirrors, providing a scalable distributed resource discovery service. NEVRLATE organizes directory servers in an approximate two-dimensional grid, or a set of sets of servers, for registration to occur in one 'horizontal' dimension, and lookup to occur in the other 'vertical' dimension. The payoff of organizing n servers into a structure like this is to achieve O(pn) message complexity for registration, and nearly constant complexity lookup. At extra cost NEVRLATE can provide fault tolerance, high availability and security, anonymity, and privacy. The protocol described can be seen as a way to organize Gnutella supernodes, or as a performance extension of Freenet's architecture. In addition, it supports expressive lookup mechanisms, and may provide a basis for a truly scalable worldwide infrastructure for the semantic and the extended web.

We present ANCORS, an adaptable network control and reporting system that merges technology from network management and distributed simulation to provide a unified paradigm for assessing, controlling, and designing active networks. ANCORS introduces a framework to assist in managing the substantial complexities of software reuse and scalability in active network environments. Specifically, ANCORS provides an extensible approach to the dynamic integration, management, and runtime assessment of various network protocols in live network operations. We present some of the advantages that can be obtained by merging technology from network management, distributed simulation, and active networking, and describe how ANCORS leverages complementary elements of each. We describe ANCORS's network engineering support to enable efficient, high-fidelity distributed simulation of networking software. We then use ANCORS to perform a quantitative study of the Random Drop SYN attack defense mechanism.

Exponential growth in digital information gathering, storage, and processing capabilities for biological data herald a new age of biology, when entire biological systems can potentially be understood. In order to facilitate human understanding of electronic components, the electronic design automation (EDA) industry has developed clean abstractions and design rules, enabling pervasive design reuse. We conjecture that design reuse arises as an emergent property in biological systems driven by the pressure for efficiency in evolution. Design reuse requires clean abstractions and interfaces, and these fortuitously provide an opportunity for human understanding and exploitation with computational toolsets. We draw some conclusions about future systems biology toolsets that might be inspired by EDA tools.

Formal analysis of security protocols is largely based on an set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiuser rewriting with existential quantification. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the stand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands.

Organizations in the private, public, and governmental sectors are more and more required to make their data available on the Internet. This demand often involves archival data maintained at the organization, which must be disclosed selectively. We illustrate an approach to classifying information for external release that guarantees protection of sensitive data while maximizing information release.

Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Strand spaces provide a simple and economical approach to state-based analysis of completed protocol runs by emphasizing causal interactions among protocol participants. The multiset rewriting formalism provides a very precise way of specifying finite-length protocols, with a bounded initialization phase but allowing unboundedly many instances of each protocol role, such as client, server, initiator, or responder. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the strand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands. The relationship we illustrate here between multiset rewriting specifications and strand spaces thus suggests refinements to both frameworks, and deepens our understanding of the Dolev-Yao model.