Author: "Thomas Genet" / Database: OpenAIRE - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Thomas Genet"' showing total 29 results

Start Over Author "Thomas Genet" Database OpenAIRE

Sorry, I don't understand your search. ×

29 results on '"Thomas Genet"'

1. Regular language type inference with term rewriting

Author: Thomas Genet, Timothée Haudebourg, Thomas Jensen, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Université de Rennes (UNIV-RENNES)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Rennes (ENS Rennes)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Université de Rennes (UNIV-RENNES), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)
Subjects: Functional programming, Theoretical computer science, Computer science, Type inference, Inference, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Abstract interpretation, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Regular language, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Algebraic data type, Computer Science::Programming Languages, Rewriting, Invariant (mathematics), Safety, Risk, Reliability and Quality, Software, ComputingMilieux_MISCELLANEOUS
Abstract: This paper defines a new type system applied to the fully automatic verification of safety properties of tree-processing higher-order functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counter-example.
Published: 2020
Full Text: View/download PDF

2. Termination of Ethereum’s Smart Contracts

Author: Thomas Genet, Thomas Jensen, Justine Sauvage, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), This work was partially supported by Laboratoired’excellence CominLabs, Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Subjects: Measure (data warehouse), Property (programming), Computer science, Process (computing), Denial-of-service attack, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], computer.software_genre, Computer security, Formal Methods for Security, Formal proof, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Smart Contracts, Ethereum, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Virtual machine, Code (cryptography), Security in Distributed Systems, Implementation, computer
Abstract: International audience; Ethereum is a decentralized blockchain technology equipped with so-called Smart Contracts. Acontract is a program whose code is public, which can be triggered by any user, and whose actualexecution is performed by miners participating in Ethereum. Miners execute the contract on theEthereum Virtual Machine (EVM) and apply its effect by adding new blocks to the blockchain.A contract that takes too much time to be processed by the miners of the network may resultinto delays or a denial of service in the Ethereum system. To prevent this scenario, termination ofEthereum’s Smart Contracts is ensured using a gas mechanism. Roughly, the EVM consumes gasto process each instruction of a contract and the gas provided to run a contract is limited. Thistechnique could make termination of contracts easy to prove but the way the official definition ofthe EVM specifies gas usage makes the proof of this property non-trivial. EVM implementationsand formal analysis techniques of EVM’s Smart Contracts use termination of contracts as anassumption, so having a formal proof of termination of contracts is crucial. This paper presents amechanized, formal, and general proof of termination of Smart Contracts based on a measure ofEVM call stacks.
Published: 2020
Full Text: View/download PDF

3. Verifying Higher-Order Functions with Tree Automata

Author: Timothée Haudebourg, Thomas Jensen, Thomas Genet, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1)
Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Term (logic), 01 natural sciences, Automaton, Set (abstract data type), Tree (data structure), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Simple (abstract algebra), 0202 electrical engineering, electronic engineering, information engineering, Rewriting, State (computer science), Tree automaton, Algorithm, Mathematics
Abstract: International audience; This paper describes a fully automatic technique for verifying safety properties of higher-order functional programs. Tree automata are used to represent sets of reachable states and functional programs are modeled using term rewriting systems. From a tree automaton representing the initial state, a completion algorithm iteratively computes an automaton which over-approximates the output set of the program to verify. We identify a subclass of higher-order functional programs for which the completion is guaranteed to terminate. Precision and termination are obtained conjointly by a careful choice of equations between terms. The verification objective can be used to generate sets of equations automatically. Our experiments show that tree automata are sufficiently expressive to prove intricate safety properties and sufficiently simple for the verification result to be certified in Coq.
Published: 2018
Full Text: View/download PDF

4. Extending Timbuk to Verify Functional Programs

Author: Timothée Haudebourg, Sébastien Lê Cong, Tristan Gillard, Thomas Genet, Software certification with semantic analysis ( CELTIQUE ), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -LANGAGE ET GÉNIE LOGICIEL ( IRISA_D4 ), Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ), Software certification with semantic analysis (CELTIQUE), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Bio-Inspired, Situated and Cellular Unconventional Information Technologies (BISCUIT), Department of Complex Systems, Artificial Intelligence & Robotics (LORIA - AIS), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Logic and Applications (LogicA), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-École normale supérieure - Cachan (ENS Cachan), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), École normale supérieure - Cachan (ENS Cachan)-Université de Rennes (UR)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Cachan (ENS Cachan)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)
Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Theoretical computer science, Property (programming), Computer science, Parameterized complexity, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 0102 computer and information sciences, 02 engineering and technology, Extension (predicate logic), [ INFO.INFO-SE ] Computer Science [cs]/Software Engineering [cs.SE], Term (logic), 01 natural sciences, Automaton, Set (abstract data type), Tree (data structure), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Rewriting system
Abstract: International audience; Timbuk implements the Tree Automata Completion algorithm whose purpose is to over-approximate sets of terms reachable by a term rewriting system. Completion is parameterized by a set of equations defining which terms are equated in the approximation. In this paper we present two extensions of Timbuk which permit us to automatically verify safety properties on functional programs. The first extension is a language, based on regular tree expressions, which eases the specification of the property to prove on the program. The second extension automatically generates a set of equations adapted to the property to prove on the program.
Published: 2018
Full Text: View/download PDF

5. GPFinder: Tracking the invisible in Android malware

Author: Jean-François Lalande, Valérie Viet Triem Tong, Thomas Genet, Mourad Leslous, Confidentialité, Intégrité, Disponibilité et Répartition (CIDRE), CentraleSupélec-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Université d'Orléans (UO)-Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), ANR-10-LABX-0007,COMIN Labs,Digital Communication and Information Sciences for the Future Internet(2010), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Subjects: 021110 strategic, defence & security studies, Computer science, 0211 other engineering and technologies, 020207 software engineering, 02 engineering and technology, Special events, Static analysis, Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Control flow, Android malware, 0202 electrical engineering, electronic engineering, information engineering, Malware, Android (operating system), computer, Humanoid robot, Reboot
Abstract: International audience; Malicious Android applications use clever techniques to hide their real intents from the user and avoid detection by security tools. They resort to code obfuscation and dynamic loading, or wait for special events on the system like reboot or WiFi activation. Therefore, promising approaches aim to locate, study and execute specific parts of Android applications in order to monitor for suspicious behavior. They rely on Control Flow Graphs (CFGs) to obtain execution paths towards sensitive codes. We claim here that these CFGs are incomplete because they do not take into consideration implicit control flow calls, i.e., those that occur when the Android framework calls a method implemented in the application space. This article proposes a practical tool, GPFinder, exposing execution paths towards any piece of code considered as suspicious. GPFinder takes the Android framework into account and considers explicit and implicit control flow calls to build CFGs. Using GPFinder, we give global characteristics of application CFGs by studying a dataset of 14,224 malware and 2,311 goodware samples. We evaluate that 72.69% of the analyzed malicious samples have at least one suspicious method reachable only through implicit calls.
Published: 2017
Full Text: View/download PDF

6. Termination criteria for tree automata completion

Author: Thomas Genet, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Theoretical computer science, Logic, Functional Programming, Tree Automata, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 01 natural sciences, Theoretical Computer Science, Set (abstract data type), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0202 electrical engineering, electronic engineering, information engineering, Tree Automata Completion, Tree automaton, Regular Tree Languages, Knuth–Bendix completion algorithm, Mathematics, Term Rewriting, Discrete mathematics, Static Analysis, Regularity Preservation, Term (logic), Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, Confluence, 020201 artificial intelligence & image processing, Rewriting, Tree (set theory), Software, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; This paper presents two criteria for the termination of tree automata completion. Tree automata completion is a technique for computing a tree automaton recognizing or over-approximating the set of terms reachable w.r.t. a term rewriting system. The first criterion is based on the structure of the term rewriting system itself. We prove that for most of the known classes of linear rewriting systems preserving regularity, the tree automata completion is terminating. Moreover, it outputs a tree automaton recognizing exactly the set of reachable terms. When the term rewriting system is outside of such classes, the set of reachable terms can be approximated using a set of equations defining an abstraction. The second criterion, which holds for any left-linear term rewriting system, defines sufficient restrictions on the set of equations for the tree automata completion to terminate. We then show how to take advantage of this second criterion to use completion as a new static analysis technique for functional programs. Some examples are demonstrated using the Timbuk completion tool.
Published: 2016
Full Text: View/download PDF

7. Reachability Analysis over Term Rewriting Systems

Author: Thomas Genet, Valérie Viet Triem Tong, and Guillaume Feuillade
Subjects: 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Term (logic), 01 natural sciences, Set (abstract data type), Tree (descriptive set theory), Computational Theory and Mathematics, 010201 computation theory & mathematics, Artificial Intelligence, Reachability, Confluence, 0202 electrical engineering, electronic engineering, information engineering, Rewriting, Tree automaton, Algorithm, Knuth–Bendix completion algorithm, Software, Mathematics
Abstract: This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the \textsf{Timbuk} tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by \textsf{Timbuk} . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.
Published: 2004
Full Text: View/download PDF

8. A Java Card CAP converter in PVS1 1This work was partially funded by the European IST R&D project 2000-26328 'Verifi card'

Author: Vikash Kodati, Thomas Genet, David Pichardie, and Thomas Jensen
Subjects: General Computer Science, Java, Computer science, Scala, computer.software_genre, Theoretical Computer Science, Real time Java, Java applet, computer.programming_language, OpenPGP card, Programming language, business.industry, strictfp, Non-blocking I/O, Generics in Java, computer.file_format, BasicCard, File format, Java concurrency, Smart card application protocol data unit, JAR, Operating system, Java Card OpenPlatform, Open Smart Card Development Platform, Smart card, Java Card, business, computer, Java annotation, Computer Science(all), Java Modeling Language
Abstract: The Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card specifies its own class file format (the Java Card Converted APplet (CAP) format) that is optimised with respect to the limited space resources of smart cards. This paper deals with the certified development of algorithms necessary for the conversion of ordinary Java class files into the CAP format. More precisely, these algorithms are concerned with constructing and compressing method tables and constant pools. The main contribution of this paper is to specify and prove the correctness of these algorithms using the theorem prover PVS.
Published: 2004
Full Text: View/download PDF

9. Towards Static Analysis of Functional Programs using Tree Automata Completion

Author: Thomas Genet, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Santiago Escobar, LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: FOS: Computer and information sciences, Discrete mathematics, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Formal Languages and Automata Theory (cs.FL), Parameterized complexity, Computer Science - Formal Languages and Automata Theory, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Static analysis, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, Logic in Computer Science (cs.LO), Automaton, Critical pair, Set (abstract data type), Combinatorics, Tree (descriptive set theory), ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methods, Rewriting, Tree automaton, Programming Languages (cs.PL), Mathematics
Abstract: This paper presents the first step of a wider research effort to apply tree automata completion to the static analysis of functional programs. Tree Automata Completion is a family of techniques for computing or approximating the set of terms reachable by a rewriting relation. The completion algorithm we focus on is parameterized by a set E of equations controlling the precision of the approximation and influencing its termination. For completion to be used as a static analysis, the first step is to guarantee its termination. In this work, we thus give a sufficient condition on E and T(F) for completion algorithm to always terminate. In the particular setting of functional programs, this condition can be relaxed into a condition on E and T(C) (terms built on the set of constructors) that is closer to what is done in the field of static analysis, where abstractions are performed on data., Proceedings of WRLA'14. 2014
Published: 2014
Full Text: View/download PDF

10. A completion algorithm for lattice tree automata

Author: Tristan Le Gall, Valérie Murat, Axel Legay, Thomas Genet, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Software certification with semantic analysis (CELTIQUE), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Reliable and efficient component based software engineering (TRISKELL), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique
Subjects: Fractal tree index, Model checking, Extended versions, Programing Languages, 0102 computer and information sciences, 02 engineering and technology, Integer arithmetic, Interval tree, 01 natural sciences, Trees (mathematics), Tree automata, Computer Programs, Regular tree, Computer Programing, Trie, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Tree automaton, Computer software, Infinite state systems, Mathematics, Automata theory, Incremental decision tree, Segment tree, Java programming language, Forestry, Integer programming, Completion algorithms, Abstract domains, 010201 computation theory & mathematics, 020201 artificial intelligence & image processing, Algorithm, Robots, Order statistic tree, Algorithms, Java program
Abstract: Conference Code:98294; International audience; When dealing with infinite-state systems, Regular Tree Model Checking approaches may have some difficulties to represent infinite sets of data. We propose Lattice Tree Automata, an extended version of tree automata to represent complex data domains and their related operations in an efficient manner. Moreover, we introduce a new completion-based algorithm for computing the possibly infinite set of reachable states in a finite amount of time. This algorithm is independent of the lattice making it possible to seamlessly plug abstract domains into a Regular Tree Model Checking algorithm. As a first instance, we implemented a completion with an interval abstract domain. We provide some experiments showing that this implementation permits to scale up regular tree model-checking of Java programs dealing with integer arithmetics.
Published: 2013
Full Text: View/download PDF

11. Equational Abstraction Refinement for Certified Tree Regular Model Checking

Author: Thomas Genet, Benoît Boyer, Yohan Boichut, Axel Legay, Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Université d'Orléans (UO)-Ecole Nationale Supérieure d'Ingénieurs de Bourges, Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Distributed and Iterative Algorithms for the Management of Telecommunications Systems (DISTRIBCOM), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Ecole Nationale Supérieure d'Ingénieurs de Bourges-Université d'Orléans (UO), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, System synthesis and supervision, scenarios (S4), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, and Genet, Thomas
Subjects: Model checking, Theoretical computer science, Java, Computer science, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], computer.software_genre, 01 natural sciences, 0202 electrical engineering, electronic engineering, information engineering, refinement, Tree automaton, tree automaton, computer.programming_language, Programming language, Proof assistant, Automaton, Critical pair, Model-checking, 010201 computation theory & mathematics, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, computer, Counterexample
Abstract: International audience; Tree Regular Model Checking (TRMC) is the name of a fam- ily of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time. This paper proposes a new CounterExample Guided Abstraction Re- finement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regu- lar overapproximation of the set of reachable states in finite time. This set is represented by R/E-automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java pro- grams by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outper- forms existing CEGAR-based completion algorithms. Contrary to exist- ing TRMC toolsets, the answers provided by TimbukCEGAR are certi- fied by Coq, which means that they are formally proved correct.
Published: 2012

12. Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems

Author: Benoît Boyer, Thomas Genet, Software certification with semantic analysis (CELTIQUE), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Computer science, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, lcsh:QA75.5-76.95, Set (abstract data type), Linear temporal logic, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Tree automaton, Equivalence class, [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS], lcsh:Mathematics, Kripke structure, Term (logic), lcsh:QA1-939, Automaton, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, lcsh:Electronic computers. Computer science, Rewriting, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; The tree automaton completion is an algorithm used for proving safety properties of systems that can be modeled by a term rewriting system. This representation and verification technique works well for proving properties of infinite systems like cryptographic protocols or more recently on Java Bytecode programs. This algorithm computes a tree automaton which represents a (regular) over approximation of the set of reachable terms by rewriting initial terms. This approach is limited by the lack of information about rewriting relation between terms. Actually, terms in relation by rewriting are in the same equivalence class: there are recognized by the same state in the tree automaton. Our objective is to produce an automaton embedding an abstraction of the rewriting relation sufficient to prove temporal properties of the term rewriting system. We propose to extend the algorithm to produce an automaton having more equivalence classes to distinguish a term or a subterm from its successors w.r.t. rewriting. While ground transitions are used to recognize equivalence classes of terms, $\epsilon$-transitions represent the rewriting relation between terms. From the completed automaton, it is possible to automatically build a Kripke structure abstracting the rewriting sequence. States of the Kripke structure are states of the tree automaton and the transition relation is given by the set of $\epsilon$-transitions. States of the Kripke structure are labelled by the set of terms recognized using ground transitions. On this Kripke structure, we define the Regular Linear Temporal Logic (R-LTL) for expressing properties. Such properties can then be checked using standard model checking algorithms. The only difference between LTL and R-LTL is that predicates are replaced by regular sets of acceptable terms.
Published: 2010
Full Text: View/download PDF

13. Equational Approximations for Tree Automata Completion

Author: Vlad Rusu, Thomas Genet, Dart, Mister, Programme 'Sécurité et Informatique' - Réécriture et Approximation pour la Vérification d'Applications Java - - RAVAJ2006 - ANR-06-SETI-0014 - SETI - VALID, Software certification with semantic analysis (CELTIQUE), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Verification models and techniques applied to testing and control of reactive systems (VERTECS), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-06-SETI-0014,RAVAJ,Réécriture et Approximation pour la Vérification d'Applications Java(2006), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Subjects: Parameterized complexity, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Tree automata, Set (abstract data type), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Term rewriting systems, Knuth–Bendix completion algorithm, Mathematics, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Discrete mathematics, Algebra and Number Theory, Verification, Reachability, Term (logic), Automaton, Algebra, Computational Mathematics, Rewriting modulo equations, 010201 computation theory & mathematics, Confluence, 020201 artificial intelligence & image processing, Rewriting, Tree (set theory)
Abstract: International audience; In this paper we deal with the veriﬁcation of safety properties of inﬁnite-state systems modeled by term-rewriting systems. An over-approximation of the set of reachable terms of a term- rewriting system R is obtained by automatically constructing a ﬁnite tree automaton. The construction is parameterized by a set E of equations on terms, and we also show that the approximating automata recognize at most the set of R/E-reachable terms. Finally, we present some experiments carried out with the implementation of our algorithm. In particular, we show how some approximations from the literature can be deﬁned using equational approximations.
Published: 2010

14. On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks

Author: Gilles Guette, Olivier Heen, Thomas Genet, Thomson Multimedia R&D France, Thomson, Département Réseaux et Télécoms - IUT Lannion, Institut Universitaire de Technologie - Lannion (IUT Lannion), Université de Rennes (UR)-Université de Rennes (UR), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Vehicular ad hoc network, Computer science, business.industry, Mobile computing, 020206 networking & telecommunications, 02 engineering and technology, Mobile ad hoc network, Cryptographic protocol, Ad hoc wireless distribution service, Computer security, computer.software_genre, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Optimized Link State Routing Protocol, 0202 electrical engineering, electronic engineering, information engineering, Wireless, 020201 artificial intelligence & image processing, business, computer, Mobile device, Computer network, Anonymity
Abstract: International audience; More and more mobile devices feature wireless communica- tion capabilities. They can self-organize in a mobile ad hoc network in order to communicate and maintain connectivity without any infrastruc- ture component. In this context, some devices may benefit from established trust relations in order to communicate private data. Various solutions already exist for establishing and detecting such trust relations. But is it still possible to detect a trust relation in an unobservable manner? That is, in a way that an attacker cannot understand whether devices share a trust relation or not. We exhibit a solution to this problem. Our solution guaranties the anony- mity and the unobservability of participants against passive and active attackers. The security properties of the solution are machine checked with the AVISPA framework [2] and the SPAN tool [5]. The main applications could be found in mobile ad hoc networks and in vehicular networks [6, 7] where anonymity and unobservability contribute to a better privacy.
Published: 2009

15. Certifying a Tree Automata Completion Checker

Author: Thomas Genet, Benoît Boyer, and Thomas Jensen
Subjects: Correctness, Theoretical computer science, Computer science, Programming language, 0102 computer and information sciences, 02 engineering and technology, Cryptographic protocol, computer.software_genre, 01 natural sciences, Automaton, Tree (data structure), 010201 computation theory & mathematics, Reachability, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Formal specification, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Tree automaton, State (computer science), computer
Abstract: Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static analyzers. However, as for many other verification techniques, the correctness of the associated tool becomes more and more difficult to guarantee. It is due to the size of the implementation that constantly grows and due to optimizations which are necessary to scale up the efficiency of the tool to verify real-size systems. In this paper, we define and develop a checker for tree automata produced by completion. The checker is defined using coq and its implementation is automatically extracted from its formal specification. Using extraction gives a checker that can be run independently of the coq environment. A specific algorithm for tree automata inclusion checking has been defined so as to avoid the exponential blow up. The obtained checker is certified in coq , independent of the implementation of completion, usable with any approximation performed during completion, small and fast. Some benchmarks are given to show how efficient the tool is.
Published: 2008
Full Text: View/download PDF

16. Towards an Efficient Implementation of Tree Automata Completion

Author: Yohan Boichut, Emilie Balland, Thomas Genet, Pierre-Etienne Moreau, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Logiciel : ANalyse et DEveloppement (Lande), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), José Meseguer and Grigore Rosu, Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique
Subjects: Theoretical computer science, Programming language, Computer science, 0102 computer and information sciences, 02 engineering and technology, Term (logic), computer.software_genre, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Critical pair, Tree (data structure), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Reachability, Confluence, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, Tree automaton, computer, Knuth–Bendix completion algorithm, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; Term Rewriting Systems (TRSs) are now commonly used as a modeling language for applications. In those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient veriﬁcation technique. Using a tree automata completion technique, it has been shown that the non reachability of a term t can be veriﬁed by computing an over- approximation of the set of reachable terms and proving that t is not in the over-approximation. Since the veriﬁcation of real programs gives rise to rewrite models of signiﬁcant size, efficient implementations of completion are essential. We present in this paper a TRS transformation preserving the reachability analysis by tree automata completion. This transforma- tion makes the completion implementation based on rewriting techniques possible. Thus, the reduction of a term to a state by a tree automaton is fully handled by rewriting. This approach has been prototyped in Tom, a language extension which adds rewriting primitives to Java. The ﬁrst experiments are very promising relative to the state-of-the-art tool Timbuk.
Published: 2008

17. AN INDUSTRIAL AND ACADEMIC JOINT EXPERIMENT ON AUTOMATED VERIFICATION OF A SECURITY PROTOCOL

Author: Nicolas Prigent, Thomas Genet, Olivier Heen, and Stephane Geller
Subjects: business.industry, Computer science, Formal specification, Key (cryptography), Joint (building), Verification, Animation, Cryptographic protocol, Software engineering, business, Protocol (object-oriented programming), Visualization
Abstract: This paper relates the collaboration between industrial and academic teams for the design and the verification of a security protocol. The protocol is about trust establishment in large communities of devices where infrastructure components are not always reachable. The collaboration covers the writing of formal specifications up to their verification, using both manual and automated verification methods embedded in the AVISPA [1] and SPAN [7] tools. At each stage, the use of the visualization and protocol animation facilities of SPAN is key to the mutual understanding of working teams. As a result, we obtain much more confidence in the security of the final protocol. We also demonstrate the usefulness of some embedded countermeasures.
Published: 2008
Full Text: View/download PDF

18. Rewriting Approximations for Fast Prototyping of Static Analyzers

Author: Thomas Genet, Thomas Jensen, Luka Le Roux, Yohan Boichut, Logiciel : ANalyse et DEveloppement (Lande), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique
Subjects: Theoretical computer science, Computer science, Programming language, Semantics (computer science), [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Java bytecode, 0102 computer and information sciences, 02 engineering and technology, Construct (python library), Term (logic), computer.software_genre, 01 natural sciences, Operational semantics, Critical pair, Set (abstract data type), 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, computer, computer.programming_language
Abstract: International audience; This paper shows how to construct static analyzers using tree automata and rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target programming language and given a program to analyze, we automatically construct an over-approximation of the set of reachable terms, i.e. of the program states that can be reached. The approach enables fast prototyping of static analyzers because modifying the analysis simply amounts to changing the set of rewrite rules defining the approximation. A salient feature of this approach is that the approximation is correct by construction and hence does not require an explicit correctness proof. To illustrate the framework proposed here on a realistic programming language we instantiate it with the Java Virtual Machine semantics and perform class analysis on Java bytecode programs.
Published: 2007

19. Feasible Trace Reconstruction for Rewriting Approximations

Author: Thomas Genet, Yohan Boichut, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Logiciel : ANalyse et DEveloppement (Lande), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique
Subjects: Theoretical computer science, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], 0102 computer and information sciences, 02 engineering and technology, Term (logic), 01 natural sciences, Set (abstract data type), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Reachability, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, 020204 information systems, Confluence, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Path (graph theory), 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, Tree automaton, Rewriting, Knuth–Bendix completion algorithm, Algorithm, Computer Science::Formal Languages and Automata Theory, Mathematics
Abstract: International audience; Term Rewriting Systems are now commonly used as a modeling language for programs or systems. On those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth- Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term t can be shown by computing an overapproximation of the set of reachable terms and prove that t is not in the approximation. However, when the term t is in the approximation, nothing can be said. In this paper, we refine this approach and propose a method taking advantage of the approximation to compute a rewriting path to the reachable term when it exists, i.e. produce a counter example. The algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the interest of such an approach w.r.t. verification of rewriting models.
Published: 2006
Full Text: View/download PDF

20. Reachability Analysis of Term Rewriting Systems with Timbuk

Author: Valérie Viet Triem Tong and Thomas Genet
Subjects: Discrete mathematics, Normalization property, Theoretical computer science, Computer science, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Term (logic), 01 natural sciences, Automaton, Critical pair, Regular language, 010201 computation theory & mathematics, Reachability, Confluence, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, Tree automaton, Tree (set theory), Rewriting
Abstract: We present Timbuk - a tree automata library - which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.
Published: 2001
Full Text: View/download PDF

21. Rewriting for Cryptographic Protocol Verification

Author: Francis Klay and Thomas Genet
Subjects: Theoretical computer science, Intersection (set theory), Programming language, Empty set, Cryptographic protocol, computer.software_genre, Set (abstract data type), Critical pair, Tree (data structure), Tree automaton, Rewriting, computer, Computer Science::Cryptography and Security, Mathematics
Abstract: On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation.
Published: 2000
Full Text: View/download PDF

22. Decidable Approximations of Sets of Descendants and Sets of Normal forms

Author: Thomas Genet, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Atteignabilité, Complétude suffisante, Computer science, Automates d'arbre, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Tree Automata, 0102 computer and information sciences, 02 engineering and technology, Subset and superset, 01 natural sciences, Terminaison, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Rewriting system, Tree automaton, Formes Normales, Approximation, Term Rewriting, Discrete mathematics, Program Verification, Reduction strategy, Systèmes de réécriture, Least-upper-bound property, 020207 software engineering, Reachability, Term (logic), Decidability, Normal Forms, Sufficient Completeness, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Confluence, Descendants, Computer Science::Programming Languages, Rewriting, Vérification de programmes, Termination
Abstract: We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the context of rewriting logic, a Term Rewriting System is a program, and a normal form is a result of the program. Thus, approximations of sets of descendants and sets of normal forms provide tools for analysing a few properties of programs: we show how to compute a superset of results, to prove the sufficient completeness property, or to find a criterion for proving termination under a specific strategy, the sequential reduction strategy. The main technical contribution of the paper is the construction of an approximation automaton which recognises a superset of the set of normal forms of terms in a set E, w.r.t. a Term Rewriting System R.
Published: 1998

23. Termination proofs using gpo ordering constraints

Author: Thomas Genet and Isabelle Gnaedig
Subjects: Constraint (information theory), Theoretical computer science, Rewriting, Data structure, Mathematical proof, Mathematics, Term (time)
Abstract: We present here an algorithm for proving termination of term rewriting systems by gpo ordering constraint solving. The algorithm gives, as automatically as possible, an appropriate instance of the gpo generic ordering proving termination of a given system. Constraint solving is done efficiently thanks to a DAG shared term data structure.
Published: 1997
Full Text: View/download PDF

24. Vérification automatique de programmes fonctionnels d'ordre supérieur à l'aide de languages réguliers d'arbres

Author: Haudebourg, Timothée, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Université Rennes 1, Thomas Genet, Thomas Jensen, Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique)
Subjects: Program Verification, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Regular tree languages, Vérification de modèles (informatique), Langages de programmation fonctionnelle, Functional programming languages
Abstract: This thesis studies how regular tree languages can be used to automatically verify properties on higher-order functional programs. Our goal is to develop new techniques and tools for the programmers to develop safer programs while reducing the time and expertise needed to verify them. In particular, we focus on the automatic verification of regular safety properties, a family of properties for which we show that completely and fully automatic verification can be achieved. Our verification method is build upon a regular abstraction procedure that can automatically learn regular tree languages that over-approximates of the reachable states of a program, allowing the verification of a target property. By using regular languages as types we modularize this procedure to verify complex properties by stating them as type inference problems. In addition we study the performances of the overall technique in our prototype OCaml implementation in the Timbuk4 verification framework over a test suite of more than 80 verification problems. We then show how our abstraction procedure can be used to verify relational properties that seemed out of the scope of regular tree languages. To do that, we use and extend a convolution operator on trees to represent every element of a relation into a regular tree language. We can then extend our previously defied regular language learning procedure to automatically infer such regular relations. We propose a Rust implementation of this idea as a regular solver for Constrained Horn Clauses systems and study its performance on several relational verification problems.; Nous étudions comment les langages réguliers d'arbres peuvent être utilisés pour vérifier automatiquement des propriétés sur des programmes fonctionnels d'ordre supérieur. Notre but est de développer de nouvelles techniques et outils pour les programmeurs permettant de développer des programmes plus sûrs tout en réduisant le temps et l'expertise nécessaire pour les vérifier. Cette thèse se concentre sur la vérification de propriétés régulières, famille pour laquelle nous montrons qu'une vérification complète et automatique est possible. Notre méthode de vérification est construite sur une procédure d'abstraction capable d'apprendre des langages réguliers sur-approchant les états atteignables d'un programme. En utilisant les langages réguliers en tant que types, nous montrons comment modulariser cette procédure pour vérifier des propriétés complexes en les formulant en tant que problèmes d'inférence des types. Nous étudions ses performances au travers de notre implémentation OCaml, Timbuk4, sur plus de 80 problèmes de vérification. Nous montrons ensuite que notre procédure d'abstraction peut être utilisée pour vérifier des propriété relationnelles qui semblaient hors de portée des langages réguliers. Pour cela, nous utilisons et étendons un opérateur de convolution sur les arbres pour représenter une relation par langage régulier. Nous étendons ensuite notre procédure d'apprentissage de langages pour inférer automatiquement ces relations. Nous proposons une implémentation de cette idée en Rust en tant solveur de systèmes de clauses de Horn contraintes et étudions ses performances sur de multiples problèmes relationnels.
Published: 2020

25. Mettre en avant et exécuter les chemins suspicieux dans les malwares Android

Author: Leslous, Mourad, Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Confidentialité, Intégrité, Disponibilité et Répartition (CIDRE), CentraleSupélec-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Université de Rennes, Valérie Viêt Triêm Tông, Thomas Genet, Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), and Université Rennes 1
Subjects: Graphe de flot de contrôle, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Control flow graph, Analyse dynamique, Android, Analyse statique, Dynamic analysis, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Retro ingénierie, Static analysis, Reverse engineering, Malware
Abstract: The last years have known an unprecedented growth in the use of mobile devices especially smartphones. They became omnipresent in our daily life because of the features they offer. They allow the user to install third-party apps to achieve numerous tasks. Smartphones are mostly governed by the Android operating system. It is today installed on more than 80% of the smartphones. Mobile apps collect a huge amount of data such as email addresses, contact list, geolocation, photos and bank account credentials. Consequently, Android has become a favorable target for cyber criminals. Thus, understanding the issue, i.e., how Android malware operates and how to detect it, became an important research challenge. Android malware frequently tries to bypass static analysis using multiple techniques such as code obfuscation and dynamic code loading. To overcome these limitations, many analysis techniques have been proposed to execute the app and monitor its behavior at runtime. Nevertheless, malware developers use time and logic bombs to prevent the malicious code from executing except under certain circumstances. Therefore, more actions are needed to trigger it and monitor its behavior. Recent approaches try to automatically characterize the malicious behavior by identifying the most suspicious locations in the code and forcing them to execute. They strongly rely on the computation of application global control flow graphs (CFGs). However, these CFGs are incomplete because they do not take into consideration all types of execution paths. These approaches solely analyze the application code and miss the execution paths that occur when the application calls a framework method that in turn calls another application method. We propose in this dissertation a tool, GPFinder, that automatically exhibits execution paths towards suspicious locations in the code by computing global CFGs that include edges representing explicit and implicit interprocedural calls. It also gives key information about the analyzed application in order to understand how the suspicious code was injected into the application. To validate our approach, we use GPFinder to study a collection of 14,224 malware samples, and we evaluate that 72.69% of the samples have at least one suspicious code location which is only reachable through implicit calls. Triggering approaches mainly use one of the following strategies to run a specific portion of the application's code: the first approach heavily modifies the app to launch the targeted code without keeping the original behavioral context. The second approach generates the input to force the execution flow to take the desired path without modifying the app's code. However, it is sometimes hard to launch a specific code location just by fuzzing the input. For instance, when the application performs a hash on the input data and compares the result to a fixed string to decide which branch of the condition to take, the fuzzing program should reverse the hashing function, which is obviously a hard problem. We propose in this dissertation a tool, TriggerDroid, that has a twofold goal: force the execution of the suspicious code and keep its context close to the original one. It crafts the required framework events to launch the right app component and satisfies the necessary triggering conditions to take the desired execution path. To validate our approach, we led an experiment on a dataset of 135 malware samples from 71 different families. Results show that our approach needs more refinement and adaptation to handle special cases due to the highly diverse malware dataset that we analyzed. Finally, we give a feedback on the experiments we led on different malware datasets, and we explain our experimental process. Finally, we present the Kharon dataset, a collection of well documented Android malware that can be used to understand the malware landscape.; Les smartphones sont devenus omniprésents dans notre vie quotidienne à cause des options qu'ils proposent. Aujourd'hui, Android est installé sur plus de 80% des smartphones. Les applications mobiles recueillent une grande quantité d'informations sur l'utilisateur. Par conséquent, Android est devenu une cible préférée des cybercriminels. Comprendre le fonctionnement des malwares et comment les détecter est devenu un défi de recherche important. Les malwares Android tentent souvent d'échapper à l'analyse statique en utilisant des techniques telles que l'obfuscation et le chargement dynamique du code. Des approches d'analyse ont été proposées pour exécuter l'application et surveiller son comportement. Néanmoins, les développeurs des malwares utilisent des bombes temporelles et logiques pour empêcher le code malveillant d'être exécuté sauf dans certaines circonstances. Par conséquent, plus d'actions sont requises pour déclencher et surveiller leurs comportements. Des approches récentes tentent de caractériser automatiquement le comportement malveillant en identifiant les endroits du code les plus suspicieux et en forçant leur exécution. Elles se basent sur le calcul des graphes de flot de contrôle (CFG) qui sont incomplets, car ils ne prennent pas en considération tous les types de chemins d'exécution. Ces approches analysent seulement le code d'application et ratent les chemins d'exécution générés quand l'application appelle une méthode du framework, qui appelle à son tour une autre méthode applicative. Nous proposons GPFinder, un outil qui extrait automatiquement les chemins d'exécution qui mènent vers les endroits suspicieux du code, en calculant des CFG qui incluent les appels interprocéduraux explicites et implicites. Il fournit aussi des informations clés sur l'application analysée afin de comprendre comment le code suspicieux a été injecté dans l'application. Pour valider notre approche, nous utilisons GPFinder pour étudier une collection de 14224 malwares Android. Nous évaluons que 72,69% des échantillons ont au moins un endroit suspicieux du code qui n'est atteignable qu'à travers des appels implicites. Les approches de déclenchement actuelles utilisent principalement deux stratégies pour exécuter une partie du code applicatif. La première stratégie consiste à modifier l'application excessivement pour lancer le code ciblé sans faire attention à son contexte originel. La seconde stratégie consiste à générer des entrées pour forcer le flot de contrôle à prendre le chemin désiré sans modifier le code d'application. Cependant, il est parfois difficile de lancer un endroit spécifique du code seulement en manipulant les entrées. Par exemple, quand l'application fait un hachage des données fournies en entrée et compare le résultat avec une chaîne de caractères fixe pour décider quelle branche elle doit prendre. Clairement, le programme de manipulation d'entrée devrait inverser la fonction de hachage, ce qui est presque impossible. Nous proposons TriggerDroid, un outil qui a deux buts : forcer l'exécution du code suspicieux et garder le contexte originel de l'application. Il fournit les événements framework requis pour lancer le bon composant et satisfait les conditions nécessaires pour prendre le chemin d'exécution désiré. Pour valider notre approche, nous avons fait une expérience sur 135 malwares Android de 71 familles différentes. Les résultats montrent que notre approche nécessite plus de raffinement et d'adaptation pour traiter les cas spéciaux dus à la grande diversité des échantillons analysés. Finalement, nous fournissons un retour sur les expériences que nous avons conduites sur différentes collections, et nous expliquons notre processus expérimental. Nous présentons le dataset Kharon, une collection de malwares Android bien documentés qui peuvent être utilisés pour comprendre le panorama des malwares Android.
Published: 2018

26. Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur

Author: Salmon, Yann, Université de Rennes (UR), École normale supérieure de Cachan/Rennes, Université de Rennes 1, and Thomas Genet
Subjects: reachability analysis, automates d'arbres, stratégie d'évaluation en profondeur, innermost strategy, analyse d'atteignabilité, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Réécriture, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], tree automata, Term Rewriting
Abstract: This document presents an extension of tree automata completion to innermost rewriting.; Établir des preuves de bon fonctionnement des programmes est délicat ; on a recours à des outils de preuve, qui doivent procéder par surapproximation (à cause du théorème de Rice). La complétion d'automate est un tel outil, qui surapproxime l'ensemble des termes accessibles lors de l'exécution d'un programme représenté par un système de réécriture. La stratégie d'évaluation donne l'ordre dans lequel les sous-termes d'un terme doivent être réécrits ; en tenir compte permet une meilleur précision de l'analyse. Notre thèse propose une adaptation de la complétion d'automate à la stratégie en profondeur, utilisée notamment par OCaml. Nous établissons la correction et la précision de notre méthode et montrons comment elle s'inscrit dans le cadre plus large de l'analyse de programmes fonctionnels (OCaml).
Published: 2015

27. Tree automata extensions for verification of infinite states systems

Author: Murat, Valérie, Software certification with semantic analysis (CELTIQUE), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Université Rennes 1, Thomas Genet, STAR, ABES, Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), and Université de Rennes
Subjects: Formal methods (Computer science), [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], Automate d'arbres, [INFO.INFO-PF] Computer Science [cs]/Performance [cs.PF], Java (Computer program language), Interprétation abstraite, Lattice, Vérification formelle, Réécriture, Treillis, Java, Tree automata
Abstract: Computer systems are more and more important in everyday life, and errors into those systems can make dramatic damages. There are formal methods which can assure reliability of a system. The formal method used in this thesis is called tree automata completion and allows to analyze infinite state systems. In this representation, states of a system are represented by a term and sets of states by tree automata. The set of all reachable behaviors (or states) of the system is computed thanks to successive applications of a term rewriting system which represents the behavior of the system. The reliability of the system is assured by checking that no forbidden state is reachable by the system. But the set of reachable states is not always computable and we need to compute an over-approximation of it. This over-approximation is not always fine enough and can recognize counter examples. The first contribution of this thesis consist in characterizing by logical formulae, in an automatic way, what is a good approximation: an over-approximation which does not contain any counter example. Solving these formulae leads automatically to a good over-approximation if such an approximation exists, without any manual setting. An other problem of tree automata completion is the scaling when dealing with real life problems. In verification of Java programs using tree automata completion, this explosion may be due to the use of Peano numbers. The idea of the second contribution of this thesis is to evaluate directly the result of an arithmetic operation. Generally speaking, we integrate elements of an infinite domain in a tree automaton. Based on abstract interpretation, this thesis allows to integrate abstract lattice in tree automata. Operations on infinite domain are computed in one step of evaluation instead of probably many application of rewrite rules. Thus we adapted tree automata completion to this new type of tree automata with lattice, and genericity of the new algorithm allows to integrate many types of lattices. This technique has been implemented in a tool named TimbukLTA, and this implementation shows the efficiency of the technique., Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique.
Published: 2014

28. Analyse statique de code dynamique

Author: Wilke, Pierre, Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA), INRIA-IRISA Rennes Bretagne Atlantique, équipe CELTIQUE, and Frédéric Besson, Thomas Genet
Subjects: JavaScript, code dynamique, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Analyse statique, systèmes de réécriture, méthodes formelles
Abstract: JavaScript est un langage de scripts utilisé sur la majorité des sites web modernes. Plusieurs plateformes permettent à présent de faire interagir différents gadgets JavaScript afin de fournir un contenu plus riche. Le langage JavaScript donne beaucoup de flexibilité aux développeurs et est extrêmement dynamique. Ces atouts viennent au prix d'une sécurité difficile à garantir. JavaScript propose notamment une fonction eval qui permet d'évaluer dynamiquement du code JavaScript à partir d'une chaîne de caractères. Cette fonction en particulier rend l'analyse statique difficile. La littérature propose quelques tentatives d'analyses statique ou dynamique pour traiter, partiellement, cette fonction qui reste un challenge. Cette fonction est un défi car elle demande l'analyse d'un ensemble de programmes possibles, alors que les analyses standards ne s'intéressent qu'à un unique programme. Afin d'attaquer ce défi, nous proposons une sémantique de JavaScript exprimée à l'aide de systèmes de réécriture de termes qui permet de raisonner sur des ensembles de programmes et qui se prête bien à l'analyse statique des états accessibles par ces programmes. Nous montrons comment cette sémantique peut être utilisée en prouvant automatiquement qu'une propriété est vérifiée pour un ensemble donné de programmes.
Published: 2013

29. Ensemble de termes accessibles en réécriture : aux frontières de la régularité

Author: Salmon, Yann, V. Gouranton Et S. Blazy, Co-Responsables Du Mri, École normale supérieure - Cachan, antenne de Bretagne (ENS Cachan Bretagne), École normale supérieure - Cachan (ENS Cachan), INRIA-IRISA Rennes Bretagne Atlantique, équipe CELTIQUE, and Thomas Genet
Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Sécurité du logiciel, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], systèmes de réécriture, preuve de programmes, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract: Avant d'exploiter ou de diffuser un logiciel, il convient de s'assurer de sa correction. Lorsque la taille du programme est grande, l'automatisation de la preuve est à rechercher, mais elle ne peut être une panacée (théorème de Rice). Ce rapport s'inscrit dans une étude utilisant les systèmes de réécriture (TRS) comme modèles formels des programmes : la correction s'exprime par le fait que l'ensemble des termes accessibles par le TRS considéré est disjoint d'un ensemble de termes représentant les mauvais comportements. On sait décider une telle propriété si les langages en jeu sont réguliers (au sens des automates d'arbres). Certaines classes de TRS préservant la régularité sont connues mais ne couvrent pas tous les cas. Ici, nous nous intéressons à la complétion d'automate. La complétion équationnelle permet de paramétrer la sur-approximation par un ensemble $E$ d'équations entre termes afin de favoriser l'obtention d'un point fixe. Nous exposons cette méthode et tentons de l'exprimer dans le vocabulaire de l'interprétation abstraite, une autre méthode d'élaboration d'analyses statiques.
Published: 2011

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources

Refine your results

29 results on '"Thomas Genet"'

1. Regular language type inference with term rewriting

2. Termination of Ethereum’s Smart Contracts

3. Verifying Higher-Order Functions with Tree Automata

4. Extending Timbuk to Verify Functional Programs

5. GPFinder: Tracking the invisible in Android malware

6. Termination criteria for tree automata completion

7. Reachability Analysis over Term Rewriting Systems

8. A Java Card CAP converter in PVS1 1This work was partially funded by the European IST R&D project 2000-26328 'Verifi card'

9. Towards Static Analysis of Functional Programs using Tree Automata Completion

10. A completion algorithm for lattice tree automata

11. Equational Abstraction Refinement for Certified Tree Regular Model Checking

12. Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems

13. Equational Approximations for Tree Automata Completion

14. On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks

15. Certifying a Tree Automata Completion Checker

16. Towards an Efficient Implementation of Tree Automata Completion

17. AN INDUSTRIAL AND ACADEMIC JOINT EXPERIMENT ON AUTOMATED VERIFICATION OF A SECURITY PROTOCOL

18. Rewriting Approximations for Fast Prototyping of Static Analyzers

19. Feasible Trace Reconstruction for Rewriting Approximations

20. Reachability Analysis of Term Rewriting Systems with Timbuk

21. Rewriting for Cryptographic Protocol Verification

22. Decidable Approximations of Sets of Descendants and Sets of Normal forms

23. Termination proofs using gpo ordering constraints

24. Vérification automatique de programmes fonctionnels d'ordre supérieur à l'aide de languages réguliers d'arbres

25. Mettre en avant et exécuter les chemins suspicieux dans les malwares Android

26. Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur

27. Tree automata extensions for verification of infinite states systems

28. Analyse statique de code dynamique

29. Ensemble de termes accessibles en réécriture : aux frontières de la régularité

Catalog

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Journal

Database

Publisher

29 results on '"Thomas Genet"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources