44 results on '"José Meseguer"'
Search Results
2. Checking Sufficient Completeness by Inductive Theorem Proving
- Author
-
José Meseguer
- Published
- 2022
3. Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
- Author
-
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn Talcott
- Abstract
Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.
- Published
- 2022
4. On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Author
-
José Meseguer and Stephen Skeirik
- Published
- 2022
5. Protocol Analysis with Time and Space
- Author
-
Catherine Meadows, José Meseguer, Julia Sapiña, Santiago Escobar, and Damián Aparicio-Sánchez
- Subjects
Spacetime ,Computer science ,Real-time computing ,Protocol analysis - Published
- 2021
6. Symbolic Computation in Maude: Some Tapas
- Author
-
José Meseguer
- Subjects
050101 languages & linguistics ,Programming language ,Computer science ,05 social sciences ,02 engineering and technology ,computer.file_format ,computer.software_genre ,Symbolic computation ,Logical framework ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,Code (cryptography) ,020201 artificial intelligence & image processing ,0501 psychology and cognitive sciences ,Executable ,Rewriting ,computer - Abstract
Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.
- Published
- 2021
7. Variant Satisfiability of Parameterized Strings
- Author
-
José Meseguer
- Subjects
Computer science ,String (computer science) ,Concatenation ,Parameterized complexity ,0102 computer and information sciences ,02 engineering and technology ,Predicate (mathematical logic) ,01 natural sciences ,Data type ,Satisfiability ,Algebra ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,Algebraic data type ,020201 artificial intelligence & image processing ,Parametric statistics - Abstract
Two “knowingly incomplete,” yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of “parametric” here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a “knowingly incomplete,” yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.
- Published
- 2020
8. Verification of the IBOS Browser Security Properties in Reachability Logic
- Author
-
José Meseguer, Stephen Skeirik, and Camilo Rocha
- Subjects
Security properties ,Modularity (networks) ,Programming language ,Computer science ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Browser security ,Automated theorem proving ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Reachability ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Rewriting ,computer - Abstract
This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.
- Published
- 2020
9. Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Author
-
José Meseguer and Stephen Skeirik
- Subjects
Initial algebra ,Discrete mathematics ,Automated theorem proving ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Unification ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,Rewriting ,Inductive reasoning ,Rule of inference ,Satisfiability ,Axiom ,Mathematics - Abstract
We present an inductive inference system for proving validity of formulas in the initial algebra \(T_{\mathcal {E}}\) of an order-sorted equational theory \(\mathcal {E}\) with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as simplification rules and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For \(\mathcal {E} = (\varSigma , E \uplus B)\), these techniques work modulo B, with B a combination of associativity and/or commutativity and/or identity axioms.
- Published
- 2020
10. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs
- Author
-
Atul Sandur, Qi Wang, Peter Csaba Ölveczky, Si Liu, José Meseguer, Lee, Ritchie, Jha, Susmit, and Mavridou, Anastasia
- Subjects
Transformation (function) ,Programming language ,Logical conjunction ,Computer science ,Formal specification ,Liveness ,ComputingMilieux_COMPUTERSANDEDUCATION ,Distributed transaction ,Systems design ,computer.software_genre ,computer ,Implementation ,Task (project management) - Abstract
Lecture Notes in Computer Science, 12229, ISSN:0302-9743, ISSN:1611-3349, NASA Formal Methods. 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings, ISBN:978-3-030-55753-9, ISBN:978-3-030-55754-6
- Published
- 2020
11. Variants in the Infinitary Unification Wonderland
- Author
-
José Meseguer
- Subjects
Discrete mathematics ,Property (philosophy) ,Unification ,Modulo ,0102 computer and information sciences ,02 engineering and technology ,Extension (predicate logic) ,01 natural sciences ,Set (abstract data type) ,Mathematics::Logic ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,Finitary ,020201 artificial intelligence & image processing ,Axiom ,Associative property ,Mathematics - Abstract
So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories \(E \cup B\) where B is a set of axioms having a finitary unification algorithm, and the equations E, oriented as rewrite rules \(\vec {E}\), are convergent modulo B. The extension to the case when B has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on \(E \cup B\) ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.
- Published
- 2020
12. Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method
- Author
-
Santiago Escobar and José Meseguer
- Subjects
Algebra ,Property (philosophy) ,Reachability ,Computer science ,Computer Science::Logic in Computer Science ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,Computer Science::Programming Languages ,Irreducibility ,Protocol analysis ,Equational theory - Abstract
This work proposes canonical constrained narrowing, a new symbolic reachability analysis technique applicable to topmost rewrite theories where the equational theory has the finite variant property. Our experiments suggest that canonical constrained narrowing is more efficient than both standard narrowing and the previously studied contextual narrowing. These results are relevant not only for Maude-NPA, but also for symbolically analyzing many other concurrent systems specified by means of rewrite theories.
- Published
- 2019
13. Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms
- Author
-
María Alpuente, Angel Cuenca-Ortega, José Meseguer, and Santiago Escobar
- Subjects
Computer science ,Modulo ,010102 general mathematics ,Context (language use) ,02 engineering and technology ,Symbolic execution ,01 natural sciences ,Algebra ,Binary operation ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,Embedding ,020201 artificial intelligence & image processing ,0101 mathematics ,Commutative property ,Axiom ,Associative property - Abstract
The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.
- Published
- 2019
14. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude
- Author
-
Qi Wang, Peter Csaba Ölveczky, Min Zhang, Si Liu, and José Meseguer
- Subjects
Model checking ,Atomicity ,Computer science ,Distributed computing ,Strong consistency ,Consistency model ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,010201 computation theory & mathematics ,Serializability ,020204 information systems ,Scalability ,0202 electrical engineering, electronic engineering, information engineering ,Distributed transaction ,Snapshot isolation - Abstract
Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.
- Published
- 2019
15. A Constructor-Based Reachability Logic for Rewrite Theories
- Author
-
Andrei Stefanescu, Stephen Skeirik, and José Meseguer
- Subjects
Class (computer programming) ,Programming language ,Computer science ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Satisfiability ,Semantic unification ,Decidability ,Range (mathematics) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Reachability ,Proof theory ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Computer Science::Logic in Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,Computer Science::Programming Languages ,Rewriting ,computer - Abstract
Reachability logic has been applied to \(\mathbb {K}\) rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
- Published
- 2018
16. Proving Ground Confluence of Equational Specifications Modulo Axioms
- Author
-
Francisco Durán, Camilo Rocha, and José Meseguer
- Subjects
Normalization property ,Property (philosophy) ,Computer science ,Modulo ,Order (ring theory) ,0102 computer and information sciences ,02 engineering and technology ,Inductive reasoning ,01 natural sciences ,Determinism ,Algebra ,010201 computation theory & mathematics ,Computer Science::Logic in Computer Science ,Confluence ,0202 electrical engineering, electronic engineering, information engineering ,Computer Science::Programming Languages ,020201 artificial intelligence & image processing ,Axiom - Abstract
Terminating functional programs should be deterministic, i.e., should evaluate to a unique result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the ground confluence property. For terminating equations this is equivalent to ground local confluence, which follows from local confluence. Checking local confluence by computing critical pairs is the standard way to check ground confluence. The problem is that some perfectly reasonable equational programs are not locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose a three-step strategy to prove that an equational program as is is ground confluent: First: apply the strategy proposed in [9] to use non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Second: use the inductive inference system proposed in this paper to prove the remaining critical pairs ground joinable. Third: to show ground confluence of the original specification, prove also ground joinable the equations added. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules.
- Published
- 2018
17. ROLA: A New Distributed Transaction Protocol and Its Formal Analysis
- Author
-
Indranil Gupta, Keshav Santhanam, Qi Wang, Si Liu, Peter Csaba Ölveczky, and José Meseguer
- Subjects
Model checking ,Atomicity ,Correctness ,Theoretical computer science ,Distributed database ,Computer science ,Consistency model ,Causal consistency ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Consistency (database systems) ,010201 computation theory & mathematics ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Distributed transaction - Abstract
Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.
- Published
- 2018
18. Associative Unification and Symbolic Reasoning Modulo Associativity in Maude
- Author
-
José Meseguer, Francisco Durán, Santiago Escobar, Carolyn L. Talcott, Steven Eker, and Narciso Martí-Oliet
- Subjects
Class (set theory) ,Unification ,Computer science ,Modulo ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Set (abstract data type) ,Algebra ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Reachability ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,Finitary ,020201 artificial intelligence & image processing ,Finite set ,Associative property - Abstract
We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems \(u =^? v\) such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.
- Published
- 2018
19. Generalized Rewrite Theories and Coherence Completion
- Author
-
José Meseguer
- Subjects
Class (set theory) ,Computer science ,0102 computer and information sciences ,02 engineering and technology ,Coherence (statistics) ,Symbolic execution ,01 natural sciences ,Algebra ,Symbolic reasoning ,010201 computation theory & mathematics ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,Computer Science::Symbolic Computation ,020201 artificial intelligence & image processing ,Rewriting - Abstract
A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [3] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [8] for standard rewrite theories, including a generalized notion of coherence, are given. Finally, symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations.
- Published
- 2018
20. Formal Modeling and Analysis of the Walter Transactional Data Store
- Author
-
Qi Wang, Peter Csaba Ölveczky, Si Liu, and José Meseguer
- Subjects
Model checking ,Computer science ,Property (programming) ,Programming language ,Probabilistic logic ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Consistency (database systems) ,Range (mathematics) ,010201 computation theory & mathematics ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Snapshot isolation ,Throughput (business) ,Transaction data ,computer - Abstract
Walter is a distributed partially replicated data store providing Parallel Snapshot Isolation (PSI), an important consistency property that offers attractive performance while ensuring adequate guarantees for certain kinds of applications. In this work we formally model Walter’s design in Maude and formally specify and verify PSI by model checking. To also analyze Walter’s performance we extend the Maude specification of Walter to a probabilistic rewrite theory and perform statistical model checking analysis to evaluate Walter’s throughput for a wide range of workloads. Our performance results are consistent with a previous experimental evaluation and throw new light on Walter’s performance for different workloads not evaluated before.
- Published
- 2018
21. Modular Verification of Sequential Composition for Private Channels in Maude-NPA
- Author
-
Santiago Escobar, Catherine Meadows, José Meseguer, and Fan Yang
- Subjects
Discrete mathematics ,Computer science ,business.industry ,020207 software engineering ,02 engineering and technology ,Composition (combinatorics) ,Modular design ,Alpha (programming language) ,Reachability ,Secrecy ,0202 electrical engineering, electronic engineering, information engineering ,Key establishment protocol ,020201 artificial intelligence & image processing ,business ,Protocol (object-oriented programming) ,Parametric statistics - Abstract
This paper gives a modular verification methodology in which, given parametric specifications of a key establishment protocol P and a protocol Q providing private channel communication, security and authenticity properties of their sequential composition \(P\; ;\; Q\) can be reduced to: (i) verification of corresponding properties for P, and (ii) verification of corresponding properties for an abstract version \(Q^\alpha \) of Q in which keys have been suitably abstracted. Our results improve upon previous work in this area in several ways. First of all, we both support a large class of equational theories and provide tool support via the Maude-NPA cryptographic protocol analysis tool. Secondly as long as certain conditions on P and Q guaranteeing the secrecy of keys inherited by Q from P are satisfied, our results apply to the composition of any two reachability properties of the two protocols.
- Published
- 2018
22. Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms
- Author
-
María Alpuente, Angel Cuenca-Ortega, José Meseguer, and Santiago Escobar
- Subjects
Programming language ,Computer science ,Modulo ,Context (language use) ,0102 computer and information sciences ,02 engineering and technology ,Term (logic) ,Program optimization ,computer.software_genre ,01 natural sciences ,Partial evaluation ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Rewriting ,Commutative property ,computer ,Axiom - Abstract
Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts and overloading; and equational rewriting modulo axioms such as commutativity, associativity–commutativity, and associativity–commutativity–identity. In this paper, we illustrate the key concepts by showing how they apply to partial evaluation of expressive rule-based programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on equational least general generalization for ensuring global termination. We demonstrate the use of the resulting partial evaluator for program optimization on several examples where it shows significant speed-ups.
- Published
- 2017
23. Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking
- Author
-
José Meseguer, Si Liu, Indranil Gupta, Peter Csaba Ölveczky, and Jatin Ganhotra
- Subjects
Theoretical computer science ,Programming language ,Computer science ,Probabilistic logic ,0102 computer and information sciences ,02 engineering and technology ,Experimental validation ,computer.software_genre ,01 natural sciences ,Statistical model checking ,Task (project management) ,Consistency (database systems) ,010201 computation theory & mathematics ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Key (cryptography) ,computer ,Design space ,Database transaction - Abstract
Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.
- Published
- 2017
24. Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- Author
-
Steven Eker, José Meseguer, Narciso Martí-Oliet, Francisco Durán, Santiago Escobar, and Carolyn L. Talcott
- Subjects
Discrete mathematics ,Unification ,Modulo ,media_common.quotation_subject ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Algebra ,010201 computation theory & mathematics ,Reachability ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Identity (philosophy) ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Equational theory ,Commutative property ,Associative property ,Mathematics ,media_common - Abstract
This paper introduces some novel features of Maude 2.7. We have added support for: i built-in order-sorted unification modulo associativity, commutativity, and identity, ii built-in variant generation, iii built-in order-sorted unification modulo a finite variant theory, and iv symbolic reachability modulo a finite variant theory.
- Published
- 2016
25. Towards Generic Monitors for Object-Oriented Real-Time Maude Specifications
- Author
-
José Meseguer, Francisco Durán, and Antonio Moreno-Delgado
- Subjects
Object-oriented programming ,Computer science ,business.industry ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Rotation formalisms in three dimensions ,Software development process ,Software ,Work (electrical) ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,Instrumentation (computer programming) ,Architecture ,Software engineering ,business - Abstract
Non-Functional Properties (NFPs) are crucial in the design of software. Specification of systems is used in the very first phases of the software development process for the stakeholders to make decisions on which architecture or platform to use. These specifications may be analyzed using different formalisms and techniques, simulation being one of them. During a simulation, the relevant data involved in the analysis of the NFPs of interest can be measured using monitors. In this work, we show how monitors can be parametrically specified so that the instrumentation of specifications to be monitored can be automatically performed. We prove that the original specification and the automatically obtained specification with monitors are bisimilar by construction. This means that the changes made on the original system by adding monitors do not affect its behavior. This approach allows us to have a library of possible monitors that can be safely added to analyze different properties, possibly on different objects of our systems, at will.
- Published
- 2016
26. Metalevel Algorithms for Variant Satisfiability
- Author
-
Stephen Skeirik and José Meseguer
- Subjects
Initial algebra ,Reflection (mathematics) ,Property (philosophy) ,Compact space ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Algorithm ,Satisfiability ,Mathematics - Abstract
Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra \(T_{\varSigma /E}\) when the theory \((\varSigma ,E)\) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation in Maude 2.7 of variant satisfiability using these sub-algorithms.
- Published
- 2016
27. Variant-Based Satisfiability in Initial Algebras
- Author
-
José Meseguer
- Subjects
Discrete mathematics ,Property (philosophy) ,Current (mathematics) ,Unification ,020207 software engineering ,02 engineering and technology ,Folding (DSP implementation) ,Satisfiability ,Decidability ,Algebra ,0202 electrical engineering, electronic engineering, information engineering ,Grand Unified Theory ,020201 artificial intelligence & image processing ,Finite set ,Mathematics - Abstract
Although different satisfiability decision procedures can be combined by algorithms such as those of Nelson-Oppen or Shostak, current tools typically can only support a finite number of theories to use in such combinations. To make SMT solving more widely applicable, generic satisfiability algorithms that can allow a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by the implementers, are highly desirable. This work studies how folding variant narrowing, a generic unification algorithm that offers good extensibility in unification theory, can be extended to a generic variant-based satisfiability algorithm for the initial algebras of its user-specified input theories when such theories satisfy Comon-Delaune’s finite variant property (FVP) and some extra conditions. Several, increasingly larger infinite classes of theories whose initial algebras enjoy decidable variant-based satisfiability are identified and illustrated with examples.
- Published
- 2016
28. Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems
- Author
-
Salvador Lucas, Raúl Gutiérrez, and José Meseguer
- Subjects
Discrete mathematics ,Program analysis ,Dependency (UML) ,Development (topology) ,Conditional term ,Computer science ,Component (UML) ,Structure (category theory) ,Rewriting ,Algorithm ,Zero (linguistics) - Abstract
Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps \(s\rightarrow t\) and rewritings \(s\rightarrow ^*t\) (in zero or more steps) are defined for specific terms \(s\) and \(t\) by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules. We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.
- Published
- 2015
29. Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
- Author
-
Stephen Skeirik and José Meseguer
- Subjects
Discrete mathematics ,Computer science ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Computer Science::Programming Languages ,Boolean operations in computer-aided design ,Finite set ,Algorithm ,Decidability - Abstract
A patternt, i.e., a term possibly with variables, denotes the set language $$\llbracket t \rrbracket $$ of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation $$\varSigma \mapsto \varSigma ^{\#}$$ that enriches the types of $$\varSigma $$. We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted i.e., simply typed algebra. This yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.
- Published
- 2015
30. Quantitative Analysis of Consistency in NoSQL Key-Value Stores
- Author
-
Jatin Ganhotra, Indranil Gupta, Muntasir Raihan Rahman, José Meseguer, Si Liu, and Son T. Nguyen
- Subjects
Consistency (database systems) ,Database ,Computer science ,Sequential consistency ,Scalability ,Strong consistency ,Probabilistic logic ,Consistency model ,Eventual consistency ,Data mining ,computer.software_genre ,NoSQL ,computer - Abstract
The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems RDBMS with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value stores seem to offer stronger consistency. Quantifying how well consistency properties are met is a non-trivial problem. We address this problem by formally modeling key-value stores as probabilistic systems and quantitatively analyzing their consistency properties by statistical model checking. We present for the first time a formal probabilistic model of Apache Cassandra, a popular NoSQL key-value store, and quantify how much Cassandra achieves various consistency guarantees under various conditions. To validate our model, we evaluate multiple consistency properties using two methods and compare them against each other. The two methods are: 1 an implementation-based evaluation of the source code; and 2 a statistical model checking analysis of our probabilistic model.
- Published
- 2015
31. Analysis of the PKCS#11 API Using the Maude-NPA Tool
- Author
-
José Meseguer, Santiago Escobar, Sonia Santiago, Catherine Meadows, and Antonio González-Burgueño
- Subjects
Hardware security module ,Cryptographic primitive ,business.industry ,Computer science ,PKCS ,Cryptographic protocol ,Computer security ,computer.software_genre ,Public-key cryptography ,PKCS #11 ,PKCS #12 ,Embedded system ,business ,computer ,PKCS #1 - Abstract
Cryptographic Application Programmer Interfaces Crypto APIs are designed to allow a secure interoperation between applications and cryptographic devices such as smartcards and Hardware Security Modules HSMs. However, several Crypto APIs have been shown to be subject to attacks in which sensitive information is disclosed to an attacker, such as the RSA Laboratories Public Key Standards PKCS#11, an API widely adopted in industry. Recently, there has been a growing interest on applying automated crypto protocol analysis methods to formally analyze APIs. However, the PKCS#11 has been proven difficult to analyze using such methods since it involves non-monotonic mutable global state. In this paper we specify and analyze the PKCS#11 in Maude-NPA, a general purpose crypto protocol analysis tool.
- Published
- 2015
32. Formal Analysis of Leader Election in MANETs Using Real-Time Maude
- Author
-
José Meseguer, Peter Csaba Ölveczky, and Si Liu
- Subjects
Mobility model ,Leader election ,business.industry ,Computer science ,ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS ,Mobile ad hoc network ,Rewriting ,Formal methods ,business ,Protocol (object-oriented programming) ,Wireless sensor network ,Computer network - Abstract
The modeling and analysis of mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ways that are hard to model and analyze by automatic formal methods. In this work we use rewriting logic and Real-Time Maude to address this challenge. We propose a composable formal framework for MANET protocols and their mobility models that can take into account such complex interactions. We illustrate our framework by analyzing a well-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.
- Published
- 2015
33. Localized Operational Termination in General Logics
- Author
-
José Meseguer and Salvador Lucas
- Subjects
Theoretical computer science ,Imperative programming ,Property (programming) ,Programming language ,Termination analysis ,Computational logic ,Programming paradigm ,Inference ,computer.software_genre ,Mathematical proof ,computer ,Operational semantics ,Mathematics - Abstract
Termination can be thought of as the property of programs ensuring that every input is given an answer in finite time. There are, however, many different (combinations of) programming paradigms and languages for these paradigms. Is a common formal definition of termination of programs in any (or most) of these programming languages possible? The notion of operational termination provides a general definition of termination which relies on the logic-based description of (the operational semantics of) a programming language. The key point is capturing termination as the absence of infinite inference, that is: all proof attempts must either successfully terminate, or they must fail in finite time. This global notion is well-suited for most declarative languages, where programs are theories in a logic whose inference system is specialized to each theory to characterize its computations. Other programming languages (e.g., imperative languages) and applications (e.g., the evaluation of specific expressions and goals in functional and logic programs) require a more specialized treatment which pays attention not just to theories, but to specific formulas to be proved within the given theory. For instance, the execution of an imperative program can be viewed as a proof of an specific formula (representing the program) within the computational logic describing the operational semantics of the programming language. In such cases, an appropriate definition of termination should focus on proving the absence of infinite proofs for computations localized to specific goals. In this paper we generalize the global notion of operational termination to this new setting and adapt the recently introduced OT-framework for mechanizing proofs of operational termination to support proofs of localized operational termination.
- Published
- 2015
34. Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Author
-
Catherine Meadows, Santiago Escobar, Sonia Santiago, and José Meseguer
- Subjects
Soundness ,Theoretical computer science ,Matching (graph theory) ,Unification ,Reachability ,Modulo ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,Protocol analysis ,Cryptographic protocol ,Completeness (statistics) ,Algorithm ,Mathematics - Abstract
Research in the formal analysis of cryptographic protocols has produced much good work in the solving of equality constraints, developing new methods for unification, matching, and deducibility. However, considerably less attention has been paid to disequality constraints. These also arise quite naturally in cryptographic protocol analysis, in particular for analysis of indistinguishability properties. Thus methods for deciding whether or not they are satisfiable could potentially be quite useful in reducing the size of the search space by protocol analysis tools. In this paper we develop a framework for reasoning about disequality constraints centered around the paradigm of the most discriminating Dolev-Yao attacker, who is able to detect a disequality if it is satisfied in some implementation of the crypto-algebra satisfying given equality properties. We develop several strategies for handling disequalities, prove their soundness and completeness, and demonstrate the result of experimental analyses using the various strategies. Finally, we discuss how disequality checking algorithms could be incorporated within symbolic reachability protocol analysis methods.
- Published
- 2015
35. Definition, Semantics, and Analysis of Multirate Synchronous AADL
- Author
-
José Meseguer, Peter Csaba Ölveczky, and Kyungmin Bae
- Subjects
Model checking ,Modeling language ,Computer science ,Semantics (computer science) ,Distributed computing ,Formal semantics (linguistics) ,Network delay ,State space ,Distributed control system ,Asynchrony (computer programming) - Abstract
Many cyber-physical systems are hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. Designing such systems is hard due to asynchrony, skews of the local clocks, and network delays; furthermore, their model checking is typically unfeasible due to state space explosion. Multirate PALS reduces the problem of designing and verifying virtually synchronous multirate systems to the much simpler tasks of specifying and verifying their underlying synchronous design. To make the Multirate PALS design and verification methodology available within an industrial modeling environment, we define in this paper the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using the AADL modeling standard. We then define the formal semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into the OSATE tool environment for AADL. Finally, we show how an algorithm for smoothly turning an airplane can be modeled and analyzed using Multirate Synchronous AADL.
- Published
- 2014
36. Formal Specification of Button-Related Fault-Tolerance Micropatterns
- Author
-
José Meseguer and Mu Sun
- Subjects
Model checking ,business.industry ,Button press ,Computer science ,Embedded system ,Formal specification ,Fault tolerance ,Probabilistic analysis of algorithms ,Hardware_PERFORMANCEANDRELIABILITY ,Internal object ,business ,Heuristics ,Imaging phantom - Abstract
Fault tolerance has been a major concern in the design of computing platforms. However, currently, fault tolerance has been done mostly with just heuristics, high level probabilistic analysis and extensive testing. In this work, we explore how we can use formal patterns to achieve fault-tolerance designs and methods. In particular, we look at faults that occur in mechanical button interfaces such as button bounce, button stuck, and phantom button faults. Our primary goal is the safety of such interfaces for medical devices [7], but the methods are more widely applicable. We formally describe corresponding patterns to address these faults including button debouncing, button stuck detection, and phantom press filtering. We prove stuttering-bisimulation results for some patterns showing their fault-masking capabilities. Furthermore, for patterns where fault-masking is not possible, we prove fault-detection properties. We also instantiate these patterns to a simple instance of a button-press counter and perform execution and model checking as further validation.
- Published
- 2014
37. A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA
- Author
-
Santiago Escobar, Sonia Santiago, José Meseguer, and Catherine Meadows
- Subjects
Discrete mathematics ,Class (set theory) ,Computer science ,Algebraic theory ,Product (mathematics) ,Modulo ,State (functional analysis) ,Cryptographic protocol ,Algorithm ,Protocol (object-oriented programming) ,Formal description - Abstract
Intuitively, two protocols \({\mathcal P}_1\) and \({\mathcal P}_2\) are indistinguishable if an attacker cannot tell the difference between interactions with \({\mathcal P}_1\) and with \({\mathcal P}_2\). In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how —assuming the protocol’s algebraic theory has a finite variant (FV) decomposition– these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.
- Published
- 2014
38. Infinite-State Model Checking of LTLR Formulas Using Narrowing
- Author
-
Kyungmin Bae and José Meseguer
- Subjects
Model checking ,Algebra ,Linear temporal logic ,Computer science ,Key (cryptography) ,State space ,Logical data model ,Rewriting ,Simple extension ,Algorithm ,Action (physics) - Abstract
The linear temporal logic of rewriting (LTLR) is a simple extension of LTL that adds spatial action patterns to the logic, expressing that a specific instance of an action described by a rewrite rule has been performed. Although the theory and algorithms of LTLR for finite-state model checking are well-developed [2], no theoretical foundations have yet been developed for infinite-state LTLR model checking. The main goal of this paper is to develop such foundations for narrowing-based logical model checking of LTLR properties. A key theme in this paper is the systematic relationship, in the form of a simulation with remarkably good properties, between the concrete state space and the symbolic state space. A related theme is the use of additional state space reduction methods, such as folding and equational abstractions, that can in some cases yield a finite symbolic state space.
- Published
- 2014
39. Formal Modeling and Analysis of Cassandra in Maude
- Author
-
Stephen Skeirik, José Meseguer, Si Liu, Indranil Gupta, and Muntasir Raihan Rahman
- Subjects
Cloud computing systems ,Linear temporal logic ,Programming language ,Computer science ,Strong consistency ,Consistency model ,Executable ,computer.file_format ,Latency (engineering) ,computer.software_genre ,computer ,Global time - Abstract
Distributed key-value stores are quickly becoming a key component of cloud computing systems. In order to improve read/write latency, distributed key-value stores offer weak notions of consistency to clients by using many complex design decisions. However, it is challenging to formally analyze consistency behaviors of such systems, both because there are few formal models, and because different consistency level combinations render understanding hard, particularly under communication latency. This paper presents for the first time a formal executable model in Maude of Cassandra, a popular key-value store. We formally models Cassandra’s main components and design strategies. We formally specify various consistency properties and model check them against our model under various communication latency and consistency combinations.
- Published
- 2014
40. Rewriting Modulo SMT and Open System Analysis
- Author
-
Camilo Rocha, César A. Muñoz, and José Meseguer
- Subjects
Model checking ,Programming language ,Computer science ,Modulo ,computer.software_genre ,Open system (systems theory) ,Formalism (philosophy of mathematics) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Reachability ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Computer Science::Logic in Computer Science ,ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION ,Computer Science::Programming Languages ,Computer Science::Symbolic Computation ,Rewriting ,computer - Abstract
This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. The proposed technique is illustrated with the formal analysis of a real-time system that is beyond the scope of timed-automata methods.
- Published
- 2014
41. Predicate Abstraction of Rewrite Theories
- Author
-
José Meseguer and Kyungmin Bae
- Subjects
Discrete mathematics ,Computer science ,Programming language ,Kripke structure ,computer.software_genre ,Predicate (grammar) ,Semantic unification ,Automated theorem proving ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Predicate abstraction ,Computer Science::Logic in Computer Science ,Formal specification ,Computer Science::Programming Languages ,Tree automaton ,Rewriting ,computer - Abstract
For an infinite-state concurrent system \(\mathcal{S}\) with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s → s′ are witnessed by concrete transitions between states in \(\mathcal{S}\) satisfying the respective sets of predicates s and s′. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems \(\mathcal{S}\) described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method—based on rewriting, semantic unification, and variant narrowing—to automatically generate a predicate abstraction when the formal specification of \(\mathcal{S}\) is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.
- Published
- 2014
42. Analysis of the IBM CCA Security API Protocols in Maude-NPA
- Author
-
José Meseguer, Santiago Escobar, Sonia Santiago, Antonio González-Burgueño, and Catherine Meadows
- Subjects
Flujo de datos multimedia 11295 / Q - Doble titulación. grado en ingeniería de sistemas de telecomunicación, sonido e imagen y grado en comunicación audiovisual 191 ,Class (computer programming) ,Flujo de datos multimedia 11295 / Q - Grado en ingeniería de sistemas de telecomunicación, sonido e imagen 152 ,Cryptographic primitive ,Automatic reasoning modulo XOR theory ,Application programming interface ,Computer science ,Cryptographic protocol ,Computer security ,computer.software_genre ,Security Application Programming Interfaces (security APIs) ,IBM 4758 common cryptographic architecture ,Cryptosystem ,Symbolic cryptographic protocol analysis ,IBM ,LENGUAJES Y SISTEMAS INFORMATICOS ,computer ,Protocol (object-oriented programming) ,Formal verification - Abstract
Standards for cryptographic protocols have long been attractive candidates for formal verification. It is important that such standards be correct, and cryptographic protocols are tricky to design and subject to non-intuitive attacks even when the underlying cryptosystems are secure. Thus a number of general-purpose cryptographic protocol analysis tools have been developed and applied to protocol standards. However, there is one class of standards, security application programming interfaces (security APIs), to which few of these tools have been applied. Instead, most work has concentrated on developing special-purpose tools and algorithms for specific classes of security APIs. However, there can be much advantage gained from having general-purpose tools that could be applied to a wide class of problems, including security APIs. One particular class of APIs that has proven difficult to analyze using general-purpose tools is that involving exclusive-or. In this paper we analyze the IBM 4758 Common Cryptographic Architecture (CCA) protocol using an advanced automated protocol verification tool with full exclusive-or capabilities, the Maude-NPA tool. This is the first time that API protocols have been satisfactorily specified and analyzed in the Maude-NPA, and the first time XOR-based APIs have been specified and analyzed using a general-purpose unbounded session cryptographic protocol verification tool that provides direct support for AC theories. We describe our results and indicate what further research needs to be done to make such protocol analysis generally effective., Antonio González-Burgueño, Sonia Santiago and Santiago Escobar have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEO2011/052. José Meseguer has been partially supported by NSF Grant CNS 13-10109.
- Published
- 2014
43. A Framework for Mobile Ad hoc Networks in Real-Time Maude
- Author
-
Peter Csaba Ölveczky, Si Liu, and José Meseguer
- Subjects
Routing protocol ,Mobility model ,Vehicular ad hoc network ,Adaptive quality of service multi-hop routing ,Wireless ad hoc network ,Computer science ,Ad hoc On-Demand Distance Vector Routing ,Distributed computing ,ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS ,Mobile ad hoc network ,Ad hoc wireless distribution service - Abstract
Mobile ad hoc networks (MANETs) are increasingly popular and deployed in a wide range of environments. However, it is challenging to formally analyze a MANET, both because there are few reasonably accurate formal models of mobility, and because the large state space caused by the movements of the nodes renders straightforward model checking hard. In particular, the combination of wireless communication and node movement is subtle and does not seem to have been adequately addressed in previous formal methods work. This paper presents a formal executable and parameterized modeling framework for MANETs in Real-Time Maude that integrates several mobility models and wireless communication. We illustrate the use of our modeling framework with the Ad hoc On-Demand Distance Vector (AODV) routing protocol, which allows us to analyze this protocol under different mobility models.
- Published
- 2014
44. A Tutorial-Style Introduction to $$\textsf {DY}^\star $$
- Author
-
Ralf Küsters, Quoc Huy Do, Tim Würtele, Guido Schmitz, Pedram Hosseyni, Karthikeyan Bhargavan, Abhishek Bichhawat, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Indian Institute of Technology [Gandhinagar] ( IIT Gandhinagar ), University of Stuttgart, Royal Holloway [University of London] (RHUL), Daniel Dougherty, José Meseguer, Sebastian Alexander Mödersheim, and Paul Rowe
- Subjects
Discrete mathematics ,[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] ,Finite-state machine ,Trace (linear algebra) ,Computer science ,Star (game theory) ,State (functional analysis) ,Cryptographic protocol ,Data structure ,Formal verification ,Dependent type ,ComputingMilieux_MISCELLANEOUS ,[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] - Abstract
\(\textsf {DY}^\star \) is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the \(\textsf {F}^\star \) programming language. Unlike automated symbolic provers, \(\textsf {DY}^\star \) accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in \(\textsf {DY}^\star \) can be executed, and hence, tested, and they can even interoperate with real-world counterparts. \(\textsf {DY}^\star \) extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security.
- Published
- 2021
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.