Automates d'arbres à contraintes globales pour la vérification de propriétés de sécurité, Tree automata with global constraints for the verification of security properties

Camille Vacher

Description

Sous la direction de Jean Goubault-Larrecq, Florent Jacquemard
Thèse soutenue le 07 décembre 2010: École normale supérieure de Cachan
Nous étudions des classes d'automates à états finis calculant sur les arbres, étendus par des contraintes permettant de tester des égalités et diségalités entre sous-arbres. Nous nous concentrons sur des automates d'arbres à contraintes globales où les tests sont opérés en fonction des états que l'automate atteint lors de ses calculs. De tels automates ont été introduit dans le cadre de travaux sur les documents semi-structurés. Nous procédons ici à une comparaison détaillée en expressivité entre ces automates et d'autres modèles permettant de réaliser des tests similaires, comme les automates à contraintes entre frères ou les automates d'arbres avec une mémoire auxiliaire. Nous montrons comment de tels automates peuvent être utilisés pour vérifier des propriétés de sécurité sur les protocoles cryptographiques. Les automates d'arbres ont déjà été utilisés pour modéliser les messages échangés lors d'une session d'un protocole. En ajoutant des contraintes d'égalité, nous pouvons décrire précisement des sessions qui utilisent à plusieurs reprises un même message, évitant ainsi une approximation trop grande. Nous répondons ensuite positivement au problème de la décision du vide des langages reconnus par les automates à contraintes globales. En montrant que leur expressivité est très proche de celle des automates opérant sur des représentations de termes par des graphes orientés acycliques, nous en déduisons une procédure de décision du vide en temps non-déterministe doublement exponentiel. Finalement, nous étudions le problème de la décision du vide pour des automates à contraintes globales pour lesquels on autorise des contraintes dites de clé, exprimant intuitivement que tous les sous arbres d'un certain type dans un arbre en entrée sont distincts deux à deux. Le type des clés est classiquement utilisé pour représenter un identifiant unique, comme un numéro de sécurité sociale.Nous décrivons alors une procédure de décision du vide de complexité non-élementaire. Nous montrons que cette procédure est très robuste, et qu'il est possible d'étendre les automates avec des contraintes supplémentaires, comme des contraintes de comptage ou des tests locaux, tout en préservant la décidabilité du vide.
-Automates d'arbres
We study here several classes of finite state automata running on trees, extended with constraints that allow to test for equalities or disequalities between subterms. We focus on tree automata with global constraints where the tests are done depending on the states reached by the automaton on its runs. Such automata were introduced in studies on semi-structured documents. We do here a detailed comparison between those automata and other models that allow to operate similar tests, like tree automata with constraints between brothers, or tree automata with an auxiliary memory. We show how such automata may be used to verify security properties on cryptographic protocols. Tree automata have already been used to modelize the messages exchanged during a protocol session. By adding equality constraints, we can describe precisely protocol sessions that use a same message several times, hence avoiding an approximation. Then, we answer positively the decision problem of the emptiness of the languages recognized by tree automata with global constraints. By showing that their expressivity is very close from the one of the automata operating on directed acyclic graphs representations of terms, we infer an emptiness decision procedure in double exponential non-deterministic time. Finally, we study the emptiness decision problem for automata with global constraints where we authorize key constraints, that intuitively allow that all subtrees of a given type in an input tree are distincts. We give an emptiness decision procedure of non-primitive recursive complexity. Key constraints are classicaly used to represent a unique identifier. We describe a non-primitive recusrive emptiness decision procedure. We show that this procedure is very robust and that it allows to extend the automata with additionnal constraints, like counting constraints or local tests, while preserving decidability.
-Tree automata
-Global constraints
-Emptiness problem
-Well quasi-order
-Dag
Source: http://www.theses.fr/2010DENS0043/document

Informations

• Publié par: Thesee
• Nombre de lectures: 58
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

THESE DE DOCTORAT
DE L’ECOLE NORMALE SUPERIEURE DE CACHAN
Présentée par
Monsieur VACHER Camille

pour obtenir le grade de
DOCTEUR DE L’ECOLE NORMALE SUPERIEURE DE CACHAN
Domaine :
Informatique
Sujet de la th è:se
Automates d'arbres à contraintes globales p our la
vérification de propriétés de sécurité
Thèse présentée et soutenue à Cachan le 07/12/2010 devant le jury
composé de :
Jean Goubault-Larrecq Professeur Directeur de thèse
Florent Jacquemard Chargé de recherche Co-directeur de thèse
Christof Loeding Professeur Examinateur
Jean-Marc Talbot Professeur Rapporteur
Sophie Tison Professeure Présidente
Igor Walukiewicz Professeur Rapporteur
Nom du Laboratoire : Laboratoire de Spécification et Vérification
ENS CACHAN/CNRS/UMR : 8643
61, avenue du Président Wilson, 94235 CACHAN CEDEX (France)
tel-00598494, version 1 - 6 Jun 2011tel-00598494, version 1 - 6 Jun 2011Remerciements
Jetienstoutd’abord`aremercierIgorWalukiewiczetJean-MarcTalbot
pour m’avoir fait l’honneur d’accepterd’ˆetre rapporteurs de cette th`ese.
Leur lecture attentive de mon manuscrit et leurs commentaires m’ont
´et´ed’uneaidepr´ecieuse. Jeremercie´egalementSophieTisonetChristof
Loeding d’avoir accept´e de participer au jury.
Merci ´egalement `a mon directeur de th`ese officiel, Jean Goubault-
Larrecq, d’avoir accepter cette responsabilit´e.
Je remercie Florent Jacquemard, mon co-directeur de th`ese, avec
qui j’ai travaill´e avec plaisir pendant plus de trois ans. La plupart des
r´esultats pr´esent´es ici doivent leur origine a` de longs apr`es-midi pass´es
ensembledevantuntableau. Qu’ilaitsug´erermesexc`esd’enthousiasme
ou de scepticisme n’est pas le moindre de ses m´erites.
Merci a` Francis Klay, de France T´el´ecom, pour son accueil, pour les
´echanges scientifiques, malheureusement trop peu nombreux, et pour
s’ˆetre assur´e que tout se d´eroulait au mieux pour moi tout au long de
ma th`ese. Merci ´egalement `a Yves Quemener, pour avoir fait un suivi
bien appr´eci´e de ma situation administrative durant ces trois ann´ees.
Je remercie Guillem Godoy, pour son accueil, sa bonne humeur et
ses id´ees ´eclairantes. Ces trois jours de travail en commun `a Barcelone
ont constitu´e une ´etape cruciale dans le d´eroulement de ma th`ese. Je
lui en suis redevable.
Si cette th`ese a pu voir le jour, c’est graˆce `a la bonne ambiance
qui r`egne dans les bˆatiments du LSV et aux personnes qui s’y trou-
vent, contribuant a` en faire un peu plus qu’un simple lieu de recherche.
Merci notamment `a ceux et celles avec qui j’ai partag´e un bureau, des
soir´ees, des repas, ou plus que cela. Une pens´ee donc pour Thomas,
´Pierre C., Etienne, Mathilde, Jules, Arnaud, Antoine, Diego, Am´elie,
Sylvain, Pierre B., Alban et Jean-Loup. D’autre part, je tiens a` re-
mercierGenevi`eve,Ahmad,Catherine,Audrey,VirginieetIsabellepour
tous les services rendus pendant mon s´ejour au LSV.
Ce manuscrit n’est pas que le r´esultat d’un travail en laboratoire,
mais doit beaucoup a` toutes les personnes que j’ai rencontr´ees ces
derni`eres ann´ees, et avec qui j’ai pu discuter en dehors de tout cadre
scientifique. Parmi elles se trouvent ´evidemment mes colocataires de
1
tel-00598494, version 1 - 6 Jun 20112
la rue Saint-Michel `a Lyon, des rues Bobillot, Crim´ee et de l’Ourcq a`
Paris, ainsi que de la rue Solf´erino a` Lille. Je l`eve un verre a` leur sant´e.
Enfin, il est quelques personnes qui me soutiennent depuis le d´ebut,
ce qui est d’autant plus appr´eci´e et courageux que la r´eciprocit´e n’est
pas mon fort. Pour cela, je pr´esente mes excuses et j’adresse toute mon
affection `a Fr´ed´erique, Gilles, Barbara, Marthe et Jacques.
tel-00598494, version 1 - 6 Jun 2011Introduction
In system and software verification, one classical problem is to modelize
infinite structures with only finitely many informations. Automata on
words have been used with this approach since decades. They are ba-
sically finite state machines that allow to represent potentially infinite
languages of words. An intuitive way to describe automata is to say
that they have a finite number of states, and each of these states will
correspond to a (potentially infinite) class of words that have the same
behavior when viewed as prefixes of other words. Then, the automaton
will have several transition rules that define the relations between all
these states. The languages recognized by automata are called regular.
The use of automata spread quickly and they are still widely used in
many fields of computer science. Among the most evident reasons of
their success, one can cite their expressiveness, the decidability of many
important problems, and the closure properties of regular languages.
Automata are as expressive as rational expressions: any language
that can be described as a rational expression can be described as an
automaton language. The problem to know whether a word can be
recognized by a given automaton, or whether there even exists such
a word, are decidable, in a reasonable complexity. Moreover, regular
languages can be combined, and automata can recognize the union or
intersection of two regular languages, and also the complement of a
regular language.
Automata have been quickly generalized from words to terms in or-
dertofinitelyrepresentinfinitelanguagesofstructuresshapedliketrees.
Most of the properties of automata on words are still true on trees. In
particular, the problems and properties mentioned above are still valid
for Tree Automata. They can be used to represent infinite sets of states
of a system or a program (in the latter case, a term can represent the
programitself),messagesexchangedinacommunicationprotocol,XML
documents... In these settings, the closure properties of TA languages
permit incremental constructions and verification problems can be re-
duced to TA problems decidable in polynomial time like emptiness (is
the language recognized by a given TA empty) and membership (is a
given term t recognized by a given TA).
Tree automata techniques are widely used in several domains
+like automated deduction (see e.g. [CLDG 07]), static analysis of
programs [BT05] or protocols [VGL07, FGT04], and XML process-
3
tel-00598494, version 1 - 6 Jun 20114
ing [Sch07]. Hence they are an important tool in security issues such
as communications protocol verification, or XML updates analysis. A
severe limitation of standard tree automata (TA) is however that they
are not able to test for equality (isomorphism) or disequality between
subterms in an input term. For instance, the language of terms de-
scribed by a non-linear pattern of the form f(x;x) is not regular (i.e.
there exists no TA recognizing this language). Such tests would also be
useful for expressing integrity constraints . Similar problems are also
frequent in the context of XML documents processing. Intuitively, an
XML document is a textual representation of the storage of data in a
tree structure; in other words, it is a finite labeled unranked tree. XML
documents are commonly represented as labeled trees, and they can be
constrained by XMLschemas, which define both typingrestrictions and
integrity constraints. All the typing formalisms currently used for XML
are based on finite tree automata. The key constraints for databases
are common integrity constraints expressing that every two distinct po-
sitions of a given type have different values (see e.g. [FL02]). This is
typically the kind of constraints that can not be characterized by TA.
One first approach to overcome this limitation of TA consists in
adding the possibility to make equality or disequality tests at each step
of the computation of the automaton. The tests are performed locally,
between subtrees at a bounded distance from the current computation
positionintheinputtree. Theemptinessproblem,whetherthelanguage
recognized by a given automaton is empty, is undecidable with such
tests [Mon81]. A decidable subclass is obtained by restricting the tests
+to sibling subtrees [BT92] (see [CLDG 07] for a survey).
Another approach to allow such tests is to add an auxiliary memory
containing a tree and permit memory comparison [CLC05]. Pushdown
tree automata [Gue83, CR07] also permit such tests. However, they are
also all limited to local tests, at a bounded distance from the current
position.
A new approach was proposed more recently in [FTT07, FTT08]
with the definition of tree automata with global equality and disequal-
ity tests (TAGED). The TAGED do not perform the tests during the
computation steps but globally on the tree, at the end of the compu-
tation, at positions which are defined by the states reached during the
computation. For instance, they can express that all the subtrees that
reachedagivenstateqareequal,orthateverytwosubtreesthatreached
0respectively the states q and q are different. The emptiness has been
shown decidable for several subclasses of TAGED [FTT07, FTT08], but