A Coq formalization of RDF and its applications

Abstract

El Marco de Descripci´on de Recursos (del ingl´es Resource Description Framework, RDF) es un modelo de datos basado en grafos que enriquece los documentos de la World Wide Web con datos entendibles por m´aquinas. Durante sus m´as de dos d´ecadas de desarrollo, RDF se ha adaptado a los nuevos desaf´ıos tecnol´ogicos. Esta adaptaci´on de RDF ha permitido su aplicaci´on en contextos cr´ıticos donde se necesitan garant´ıas de seguridad, como calcular sumas de verificaci´on o firmar digitalmente grafos RDF. Los asistentes de prueba son herramientas de verificaci´on formal capaces de proveer certificaciones de software s´olidas, proporcionando un puente entre la programaci´on y la l´ogica. En particular, Coq ha influido en los m´etodos formales, la verificaci´on de programas, y matem´aticas formales mediante el desarrollo de software confiable utilizando argumentos l´ogicos rigurosos. Visualizamos un est´andar RDF con software certificado siguiendo un enfoque mecanizado mediante el uso de asistentes de prueba. En este trabajo presentamos CoqRDF: una librer´ıa mecanizada que especifica formalmente el modelo RDF, proveyendo una base de datos de lemas formalmente mecanizados sobre RDF. CoqRDF nos permite definir operaciones como el re-etiquetado de nodos en blanco e isomorfismo RDF y razonar sobre ellos mec´anicamente. Yendo m´as lejos, utilizamos la librer´ıa para implementar el algoritmo κ-mapping, un algoritmo para detectar grafos RDF que son isomorfos. Desarrollamos una t´ecnica de prueba para trazabilizar el re-etiquetado de nodos en blanco durante la computaci´on. Usando esta t´ecnica y CoqRDF demostramos dos propiedades sobre κ-mapping: que para cualquier grafo, κ-mapping retorna un grafo isomorfo al grafo de entrada; y que dos grafos resultan en conjuntos iguales al aplicarles κ-mapping, si y solo si, los grafos de entrada son isomorfos. Estas pruebas nos permiten concluir que κ-mapping es un algoritmo iso-canonico con una prueba completamente mecanizada. Una perspectiva posible para CoqRDF ser´ıa mecanizar otros est´andares construidos sobre RDF. Creemos haber contribuido con una primera piedra hacia una cadena de herramientas mecanizada de est´andares web basada en RDF.

The Resource Description Framework (RDF) is a graph data model enriching the documents of the World Wide Web with machine-readable data. For over two decades of development, RDF has been adapted to the new technological challenges. This adaptation of RDF has enabled its application in critical contexts where security guarantees are needed, such as computing checksums or digitally signing RDF graphs. Proof assistants are formal verification tools allowing a robust certification of software, providing a bridge between programming and logic. In particular, Coq has influenced formal methods, program verification, and formal mathematics through the development of reliable software using rigorous logical arguments. We envision an RDF standard with certified software by following a mechanized approach using proof assistants. In this work we present CoqRDF: a mechanized library formally specifying the RDF model, with a database of formally mechanized lemmas about RDF. CoqRDF allows us to define operations such as blank node relabeling, and RDF isomorphism and reason about them mechanically. Going further, we use the library to implement κ-mapping, an algorithm for detecting isomorphic RDF graphs. We develop a proof technique to keep track of blank node relabeling through computation. Using this technique and CoqRDF we prove two properties of κ-mapping: that κ-mapping returns a graph, which is isomorphic to input; and that two graphs give a set-equal result under κ-mapping, if and only if, the input graphs are isomorphic. These two properties allows us to conclude that κ-mapping is an iso-canonical algorithm, with a fully mechanized proof. A possible perspective for CoqRDF would be to mechanize standards built on top of RDF. We believe that we have contributed with a first stone towards a mechanized toolchain of web standards based on RDF.