A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links
Keywords:Formal Specification, Deductive Verification, Program Verifier Why3, Unix file system, Path resolution
AbstractIn the context of file systems like those of Unix, path resolution is the operation that given a character string denoting an access path, determines the target object (a file, a directory, etc.) designated by this path. This operation is not trivial because of the presence of symbolic links. Indeed, the presence of such links may induce infinite loops. We consider a path resolution algorithm that always terminate, detecting if it enters an infinite loop and reports a resolution failure in such a case. We propose a formal specification of path resolution and we formally prove that our algorithm terminates on any input, and is correct and complete with respect to our formal specification.
Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657–683, September 2001.
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let’s verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709–727, 2015. See also http://toccata.lri.fr/gallery/fm2012comp.en.html.
Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016.
Ran Chen and Jean-Jacques Lévy. A semi-automatic proof of strong connectivity. In 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Heidelberg, Germany, July 2017.
Jean-Christophe Filliâtre and Andrei Paskevich. Why3 — where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125–128. Springer, March 2013.
IEEE and The Open Group. POSIX.1-2008/Cor 1-2013. http://pubs.opengroup.org/onlinepubs/9699919799/.
Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer.
Gian Ntzik and Philippa Gardner. Reasoning about the POSIX file system: Local update and global pathnames. In Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOP-SLA, pages 201–220. ACM, 2015.
Tom Ridge, David Sheets, Thomas Tuerk, Anil Madhavapeddy, Andrea Giugliano, and Peter Sewell. SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. In 25th ACM Symposium on Operating Systems Principles, 2015.
How to Cite
Copyright (c) 2017 Ran Chen, Martin Clochard, Claude Marché
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.