Rewrite based Verification of XML Updates
Florent Jacquemard (INRIA Saclay - Ile de France), Michael Rusinowitch, (INRIA Lorraine - LORIA / LIFC)

TL;DR
This paper presents a method for verifying XML document updates by reducing access control and safety property checks to hedge automata type checking, ensuring document validity after updates.
Contribution
It introduces a novel approach to static type checking for XML updates using hedge automata, addressing safety and policy consistency problems.
Findings
Type checking reduces to hedge automata computations
Ensures preservation of document types after updates
Detects policy violations through automata analysis
Abstract
We consider problems of access control for update of XML documents. In the context of XML programming, types can be viewed as hedge automata, and static type checking amounts to verify that a program always converts valid source documents into also valid output documents. Given a set of update operations we are particularly interested by checking safety properties such as preservation of document types along any sequence of updates. We are also interested by the related policy consistency problem, that is detecting whether a sequence of authorized operations can simulate a forbidden one. We reduce these questions to type checking problems, solved by computing variants of hedge automata characterizing the set of ancestors and descendants of the initial document type for the closure of parameterized rewrite rules.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Advanced Data Storage Technologies · Distributed systems and fault tolerance
