Verifiable file system

Why a filesystem

• Interface is very well-defined (POSIX)
  creat, open, close, read, write ...
• Specification is not likely be too hard to formalize and write
  • either as reference implementation
    or as a set of logical properties
• Amenable to different approaches
  • either a posteriori verification of EXT3, JFFS2, ReiserFS,
    or correct-by-construction approaches
• Modern filesystems are complex
  • multi-threaded; must be reset-tolerant, secure
    many common filesystems are buggy: see paper by [Yang,Twohey,Engler,Musuvathi] in OSDI 2004
• Verification would have an impact
  since all our data is stored on filesystems
• Low risk: could make formal specifications and verifier(s) openly available to all future filesystem designers for validating their implementations

Roadmap

• Write a formal specification: need to disambiguate and formalize POSIX prose
• Publish an open challenge inviting candidate implementations? -- many thorny issues (e.g., specification & implementation languages, hardware platform)
• What should be the verification criteria? -- e.g., random testing against a reference implementation
• Note: cannot ignore performance!

See also the VSTTE position paper.