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.

Requirements are informal and semi-formal descriptions of the expected behavior of a complex system from the viewpoints of its stakeholders customers, users, operators, designers, and engineers. However, for the purpose of design, testing, and verification for critical systems, we can transform requirements into formal models that can be analyzed automatically. ARSENAL is a framework and methodology for systematically transforming natural language NL requirements into analyzable formal models and logic specifications. These models can be analyzed for consistency and implementability. The ARSENAL methodology is specialized to individual domains, but the approach is general enough to be adapted to new domains.

This paper is a tribute to Jose Meseguer, from the rest of us in the Maude team, reviewing the past, the present, and the future of the language and system with which we have been working for around two decades under his leadership. After reviewing the origins and the language’s main features, we present the latest additions to the language and some features currently under development. This paper is not an introduction to Maude, and some familiarity with it and with rewriting logic are indeed assumed.

Despite advances in recent years in the area of mandatory access control in database systems, today's information repositories remain vulnerable to inference and data association attacks that can result in serious information leakage. Without support for coping against these attacks, sensitive information can be put at risk because of release of other (less sensitive) related information. The ability to protect information diclosure against such improper leakage would be of great benefit to governmental, public, and private institutions, which are, today more than ever, required to make portions of their data available for external release. In this paper we address the problem of classifying information by enforcing explicit data classification as well as inference and association constraints. We formulate the problem of determining a classification that ensures satisfaction of the constraints, while at the same time guaranteeing that information will not be overclassified. We present an approach to the solution of this problem and give an algorithm implementing it which is linear in simple cases, and quadratic in the general case. We also analyze a variant of the problem that is NP-complete.

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.

We present an approach for detecting sensor spoofing attacks on a cyber-physical system. Our approach consists of two steps. In the first step, we construct a safety envelope of the system. Under nominal conditions (that is, when there are no attacks), the system always stays inside its safety envelope. In the second step, we build an attack detector: a monitor that executes synchronously with the system and raises an alarm whenever the system state falls outside the safety envelope. We synthesize safety envelopes using a modifed machine learning procedure applied on data collected from the system when it is not under attack. We present experimental results that show effectiveness of our approach, and also validate the several novel features that we introduced in our learning procedure.

We present a methodology for the probabilistic modeling of failure dependencies in large, complex systems using Markov Logic Networks (MLNs), a state-of-the-art probabilistic relational modeling technique in machine learning. We illustrate this modeling methodology on example system architectures, and show how the the Probabilistic Consistency Engine (PCE) tool can create and analyze failure-dependency models. We compare MLN-based analysis with analytical symbolic analysis to validate our approach. The latter method yields bounds on the expected system behaviors for different component-failure probabilities, but it requires closed-form representations and is therefore often an impractical approach for complex system analysis. The MLN-based method facilitates techniques of early design analysis for reliability (e.g., probabilistic sensitivity analysis). We analyze two examples - a portion of the Time-Triggered Ethernet (TTEthernet) communication platform used in space, and an architecture based on Honeywell's Cabin Air Compressor(CAC) - that highlight the value of the MLN-based approach for analyzing failure dependencies in complex cyber-physical systems.

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.

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.

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications, and has a relatively large worldwide user and open-source developer base. This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel functions for order-sorted unification modulo some frequently occurring equational axioms. Narrowing is currently supported in its Full Maude extension. We also give a brief summary of the most important features of Maude 2.4 that were not part of Maude 2.0 and earlier releases. These features include communication with external objects, a new implementation of its module algebra, and new predefined libraries. We also review some new Maude applications.

During the development of the Maude system we have put special emphasis on the creation of metaprogramming facilities to allow the generation of execution environments for a wide variety of languages and logics. The first most obvious area where Maude can be used as a metalanguage is in building language extensions for Maude itself. Our experience in this regard—first reported in [107], and further documented in [108, 98, 99, 109]—is very encouraging.

This chapter describes the equational specification in Maude of a series of typical data structures, complementing in this way the list and set data structures provided as predefined modules in Maude and described in Section 9.12.

This chapter explains how to use the facilities provided by the predefined modules META-LEVEL and LOOP-MODE for constructing user interfaces and metalanguage applications, in which Maude is used not only to define a domain-specific language or tool, but also to build an environment for the given language or tool. In such applications, the LOOP-MODE module can be used to handle the input/ output and to maintain the persistent state of the language environment or tool. This chapter also describes an approach based on actors to endow Maude with interactive capabilities.

Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant metatheoretic aspects. In other words, a reflective logic is a logic which can be faithfully interpreted in itself. Maude’s language design and implementation make systematic use of the fact that rewriting logic is reflective [66, 56, 67, 68]. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way. However, since a naive implementation of reflection can be computationally expensive, a good implementation must provide efficient ways of performing reflective computations. This chapter explains how this is achieved in Maude through its predefined META-LEVEL module, that can be found in the prelude.maude file.

In Full Maude, concurrent object-oriented systems can be defined by means of object-oriented modules—introduced by the keyword omod...endom—using a syntax more convenient than that of system modules, because it assumes acquaintance with the basic entities, such as objects, messages and configurations, and supports linguistic distinctions appropriate for the object-oriented case.

This chapter introduces the basic syntactic ingredients of all Maude specifications: identifiers, module names, sort names, and operator declarations. Other syntactic parts of Maude specifications, like equations and rules, will appear in the following chapters.

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

There are several approaches to debugging and optimizing Maude programs: tracing, term coloring, using the debugger, and using the profiler.

As pointed out in Section 1.4, given a Maude system module, we can distinguish two levels of specification: a system specification level, provided by the rewrite theory specified by that system module which defines the behavior of the system, and a property specification level, given by some property (or properties) φ that we want to state and prove about our module.

As the systems we have to specify and verify become larger and more complex, there is a mounting need to combine different tools and decision procedures to accomplish large proof tasks. The problem, then, is how to be sure that we can trust heterogeneous proofs produced by different tools based on different formalisms. In this work we focus on certification and synthesis of equational proofs, that are pervasive in most proof tasks and for which many tools are poorly equipped. Fortunately, equational proof engines like ELAN and Maude can perform millions of equational proof steps per second which, if properly certified, can be trusted by other tools. We present a general method to certify and synthesize proofs in membership equational logic, where the synthesis may involve generating full proofs from proof traces modulo combinations of associativity, commutativity, and identity axioms. We propose a simple representation for proof objects and give algorithms that can synthesize space-efficient, machine-checkable proof objects from proof traces.

This paper gives an overviewof the Maude 2.0 system. We emphasize the full generality with which rewriting logic and membership equational logic are supported, operational semantics issues, the new built-in modules, the more general Full Maude module algebra, the new META-LEVEL module, the LTL model checker, and new implementation techniques yielding substantial performance improvements in rewriting modulo. We also comment on Maude's formal tool environment and on applications.

We propose a new practical technique for the distributed execution-driven simulation of parallel computers. Our simulation methodology allows complete verbalization of the design at all levels and achieves good performance by preserving and exploiting the parallelism of the parallel program being simulated. With our technique it is possible to decouple the simulation of the execution of a parallel application from the estimation of the virtual execution time in which such execution is carried out. Our technique uses minimal overhead to maintain coherent distributed event causality relations by making it possible for the simulated executions to reflect the intrinsic uncertainties of parallel applications being simulated. We include a detailed description of our methodology, explain how to apply our ideas to parallelize an existing execution-driven sequential simulator under quite general assumptions, discuss the trade-offs of our methodology, and give preliminary performance measurements of a distributed simulator that uses our technique.

Organizations today are faced with an ever-increasing need to become more efficient in their methods for exchange of information with consumers, collaborators, and partners. Unfortunately existing mechanisms for such information exchange provide nowhere near the levels of both security and automation required to satisfy this need. Effective information sharing and dissemination can take place only if the data holders have assurance that access constraints on the information they own or manage will be respected and that, while releasing information, disclosure of sensitive information is not a risk. The Secure Access Wrapper (SAW) project is a collaborative effort between SRI International and Stanford University to develop techniques that provide substantially more automation and assurance than has previously been available for secure, selective information sharing. The SAW project is sponsored by DARPA ITO under the Wrappers and Composition focus area of the Information Survivability program.

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude.

Mobile Maude is a mobile agent language extending the rewriting logic language Maude and supporting mobile computation. Mobile Maude uses reflection to obtain a simple and general declarative mobile language design and makes possible strong assurances of mobile agent behavior. The two key notions are processes and mobile objects. Processes are located computational environments where mobile objects can reside. Mobile objects have their own code, can move between different processes in different locations, and can communicate asynchronously with each other by means of messages. Mobile Maude’s key novel characteristics include: (1) reflection as a way of endowing mobile objects with “higher-order” capabilities; (2) object-orientation and asynchronous message passing; (3) a high-performance implementation of the underlying Maude basis; (4) a simple semantics without loss in the expressive power of application code; and (5) security mechanisms supporting authentication, secure message passing, and secure object mobility. Mobile Maude has been specified and prototyped in Maude. Here we present the Mobile Maude language for the first time, and illustrate its use in applications by means of Milner’s cell-phone example. We also discuss security and implementation issues.

Maude 2.0 is the new version of the Maude rewriting logic language currently under development. Maude 2.0’s three main goals are: (i) greater generality and expressiveness;( ii) efficient support for a wider range of programming applications;and (iii) usability as a key component for developing internet programming and mobile computing systems. To meet these goals, a number of new features have been added. The membership equational logic of functional modules and the rewriting logic of system modules are now supported in their greatest possible generality, and the operational semantics of object-oriented modules guarantees object and message fairness. Module operations in Full Maude are also more general thanks to parameterized theories and views. Efficient support for a wider range of programming applications is provided both by the Maude compiler—which can reach up to 15 million rewrites per second on a 667MHz Xeon—and by a library of new built-in modules. Besides new built-in functional modules, a key new feature is built-in object-oriented modules that provide flexible interaction with external objects such as file systems, window systems, and internet sockets. In particular, built-in internet sockets will provide excellent support for a new declarative style of internet programming in Maude, and will be used as a key building block to implement the Mobile Maude language.

Maude is a high-performance language and system supporting both equational and rewriting logic computation for a wide range of applications, including development of theorem proving tools, language prototyping, executable specification and analysis of concurrent and distributed systems, and logical framework applications in which other logics are represented, translated, and executed. Maude’s functional modules are theories in membership equational logic [8,1], a Horn logic whose atomic sentences are either equalities t = t′ or membership assertions of the form t : s, stating that a term t has a certain sort s. Such a logic extends OBJ3’s [4] order-sorted equational logic and supports sorts, subsorts, subsort polymorphic overloading of operators, and definition of partial functions with equationally defined domains. Maude’s functional modules are assumed to be Church-Rosser; they are executed by the Maude engine according to the rewriting techniques and operational semantics developed in [1]. Membership equational logic is a sublogic of rewriting logic [6]. A rewrite theory is a pair (T, R) with T a membership equational theory, and R a collection of labeled and possibly conditional rewrite rules involving terms in the signature of T . Maude’s system modules are rewrite theories in exactly this sense. The rewrite rules r : t −→ t′ in R are not equations. Computationally, they are interpreted as local transition rules in a possibly concurrent system. Logically, they are interpreted as inference rules in a logical system. This makes rewriting logic both a general semantic framework to specify concurrent systems and languages [7], and a general logical framework to represent and execute different logics [5]. Rewriting in (T, R) happens modulo the equational axioms in T . Maude supports rewriting modulo different combinations of associativity, commutativity, identity, and idempotency axioms. The rules in R need not be Church-Rosser and need not be terminating. Many different rewriting paths are then possible; therefore, the choice of appropriate strategies is crucial for executing rewrite theories. In Maude, such strategies are not an extra-logical part of the language.

We present compilation techniques for Simple Maude, a declarative programming language based on Rewriting Logic which supports term, graph, and object-oriented rewriting. We show how to compile various constructs of Simple Maude onto SIMD and MIMD/SIMD massively parallel architectures, and in particular onto the Rewrite Rule Machine (RRM), a special purpose MIMD/SIMD architecture for rewriting. We then demonstrate how to compile SIMD graph rewriting onto MIMD/SIMD architectures, and discuss mapping 3-D structures into 2-D SIMD meshes. Finally, we sketch the compilation of object-oriented rewriting into efficient MIMD/SIMD code. We thus show that Simple Maude is an efficient, machine-independent parallel programming language.

Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way, and makes possible many advanced metaprogramming applications, including user-definable strategy languages, language extensions by new module composition operations, development of theorem proving tools, and reifications of other languages and logics within rewriting logic. A naive implementation of reflection can be computationally very expensive. We explain the semantic principles and implementation techniques through which efficient ways of performing reflective computations are achieved in Maude through its predefined META-LEVEL module. We are indebted to Jose F. Quesada for his excellent work on the MSCP context-free parser for Maude, that---besides being used for different parsing functions in Maude---is used as a key component of the built-in function meta-parse in META-LEVEL. We cordially thank Carolyn Talcott for many discussions on metalevel issues that have contributed to the development of our ideas.

One of the key goals of rewriting logic from its beginning has been to provide a semantic and logical framework in which many models of computation and languages can be naturally represented. There is by now very extensive evidence supporting the claim that rewriting logic is indeed a very flexible and simple logical and semantic framework. From a language design point of view the obvious question to ask is: how can a rewriting logic language best support logical and semantic framework applications, so that it becomes a metalanguage in which a very wide variety of logics and languages can be both semantically defined, and implemented? Our answer is: by being reflective. This paper discusses our latest language design and implementation work on Maude as a reflective metalanguage in which entire environments---including syntax definition, parsing, pretty printing, execution, and input/output---can be defined for a language or logic £ of choice.

Most formal approaches to security protocol analysis are based on a set of assumptions commonly referred to as the "Dolev-Yao model". In this paper, we use a multiset rewriting formalism, based on linear logic, to state the basic assumptions of this model. A characteristic of our formalism is the way that existential quantification provides a succinct way of choosing new values, such as new keys or nonces. We define a class of theories in this formalism that correspond to finite-length protocols, with a bounded initialization phase but allowing unboundedly many instances of each protocol role (e.g., client, sewer; initiator or responder). Undecidability is proved for a restricted class of these protocols, and PSPACE-completeness is claimed for a class further restricted to have no new data (nonces). Since it is a fragment of linear logic, we can use our notation directly as input to linear logic tools, allowing us to do proof search for attacks with relatively little programming effort, and to formally verify protocol transformations and optimizations.

Despite advances in recent years in the area of mandatory access control in database systems, today’s information repositories remain vulnerable to inference and data association attacks that can result in serious information leakage. Such information leakage can be prevented by properly classifying information according to constraints that express relationships among the security levels of data objects. In this paper we address the problem of classifying information by enforcing explicit data classification as well as inference and association constraints. We formulate the problem of determining a classification that ensures satisfaction of the constraints, while at the same time guaranteeing that information will not be unnecessarily overclassified. We present an approach to the solution of this problem and give an algorithm implementing it which is linear in simple cases, and low-order polynomial (n) in the general case. We also analyze a variant of the problem that is NP-hard.