A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links

Authors

  • Ran Chen Institute of Software, Chinese Academy of Science, Beijing
  • Martin Clochard LRI (CNRS & Univ. Paris-Sud), Université Paris-Saclay
  • Claude Marché Inria Saclay-Ile-de-France

DOI:

https://doi.org/10.6092/issn.1972-5787/6767

Keywords:

Formal Specification, Deductive Verification, Program Verifier Why3, Unix file system, Path resolution

Abstract

In 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.

References

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.

Downloads

Published

2017-11-22

How to Cite

Chen, R., Clochard, M., & Marché, C. (2017). A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. Journal of Formalized Reasoning, 10(1), 51–66. https://doi.org/10.6092/issn.1972-5787/6767

Issue

Vol. 10 No. 1 (2017)

Section

Articles

License

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.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy