Tyrex | Project

Soundy Analysis Techniques for Web Development

XQuery [1] is the standard language language dedicated to XML data querying and manipulation. As opposed to other NoSQL languages (and e.g. XSLT in particular), it has been intended to feature strong static typing [5].

As emphasized in [4], "static program analysis is a key component of many software development tools, including compilers, development environments, and verification tools. Analyses are often expected to be sound in that their result models all possible executions of the program under analysis. Soundness implies that the analysis computes an over-approximation in order to stay tractable [5]; the analysis result will also model behaviors that do not actually occur in any program execution. The precision of an analysis is the degree to which it avoids such spurious results. Users expect analyses to be sound as a matter of course, and desire analyses to be as precise as possible, while being able to scale to large programs."

It was shown in [2] that sound yet precise static analyses are possible for an XQuery fragment [2], even for complex expressions that navigate in XML trees [2,3]. While soundness seems essential for any kind of static program analysis, approximations and omissions are usually required for language features when applied to real programs. This is coined by the recent concept of soundiness [4] which defines "soundy analyses": a soundy analysis aims to be as sound as possible without excessively compromising precision or scalability.

The goal of this internship is to investigate methods of code analysis which take advantage of sound verification systems developed for XQuery language fragments in the literature (such as [2]) to efficiently compute useful guarantees on real XQuery code used in production.

Specifically, the subject will consist of:

  • identifying different levels of static analyses corresponding to relevant language fragments;
  • supplementing sound analysis techniques with relevant approximations to make the most of them with real-world code;
  • investigating the concept of soundiness [4] in the context of XQuery;
  • implementing a prototype checker which is capable of running on real production code while indicating meaningful guarantees that can be provided.

Real-world XQuery code will be provided by a startup in the domain of XQuery-based web development frameworks.

NB: this is a topic where we can easily set the balance between applied research and theoretical research.

References:

  1. XQuery 3.0: An XML Query Language, W3C Recommendation 08 April 2014: https://www.w3.org/TR/xquery-30/
  2. XQuery and Static Typing: Tackling the Problem of Backward Axes. Pierre Geneves and Nils Gesbert. In International Conference on Functional Programming (ICFP) 2015 (https://hal.inria.fr/hal-01082635v2/document)
  3. Efficient Static Analysis of XML Paths and Types. Pierre Geneves, Nabil Layaida, Alan Schmitt. In ACM SIGPLAN conference on Programming language design and implementation (PLDI) 2007 (https://hal.inria.fr/inria-00502789/document)
  4. In Defense of Soundiness: A Manifesto. Ben Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh, Evan Chang, Sam Guyer, Uday Khedker, Anders Møller and Dimitrios Vardoulakis. In Communications of the ACM, 2015. http://soundiness.org/
  5. Course: Introduction to XQuery and Static Type-Checking. University Grenoble Alpes. Pierre Geneves. http://tyrex.inria.fr/courses/mosig2015/xquery.pdf

Contacts

Pierre Genevès (pierre.geneves@cnrs.fr), Nils Gesbert (nils.gesbert@grenoble-inp.fr), Nabil Layaïda (nabil.layaida@inria.fr)