Rewrite-Based Verification of XML Updates

Florent Jacquemard 1 Michael Rusinowitch 2
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a model for XML update primitives of the W3C XQuery Update Facility as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. These type inference algorithms are directly applicable to XML static typechecking, which is the problem of verifying whether, a given document transformation always converts source documents of a given input type into documents of a given output type. We show that typechecking for arbitrary sequences of XML update primitives can be done in polynomial time when the unranked tree automaton defining the output type is deterministic and complete, and that it is EXPTIME-complete otherwise. We then apply the results to the verification of access control policies for XML updates. We propose in particular a polynomial time algorithm for the problem of local consistency of a policy, that is, for deciding the non-existence of a sequence of authorized update operations starting from a given document that simulates a forbidden update operation.
Document type :
Conference papers
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/inria-00578916
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 4:30:53 PM
Last modification on : Thursday, February 7, 2019 - 5:29:23 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:50:41 AM

File

ppdp06a-jacquemard-HAL.pdf
Files produced by the author(s)

Identifiers

Citation

Florent Jacquemard, Michael Rusinowitch. Rewrite-Based Verification of XML Updates. 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), Jul 2010, Hagenberg, Austria. ⟨10.1145/1836089.1836105⟩. ⟨inria-00578916⟩

Share

Metrics

Record views

482

Files downloads

254