Research » VFS » WebHome

Verifiable Filesystem

The formal methods community has decided to challenge software developers to use formal methods techniques, in order to specify/model "big" software systems. Such software artifacts would then be a part of the Verifiable Software Repository.

One of the challenges released intended to specify the standard POSIX 1003.1, which is in fact an enormous task. So, Rajeev Joshi and Gerard J. Holzmann have proposed a so-called mini-challenge that focus on building a verifiable file system that follows the POSIX guide lines. Furthermore, the proponents of the mini-challenge have also introduced a project carried out at NASA Jet Propulsion Laboratory, whose goal is to build such a verifiable file system but designed for use directly in Flash Memories.

The main goal of this project is to respond to such a mini-challenge, taking in account the Flash Memory specific aspects including hardware support for the file system, following established techniques as well as new insights on how to use and apply formal methods in a system wide development.

Publications

  • (pdf) Presentation on the VDM-Overture Workshop, FM08, Turku, 26 May 2008
  • M.A. Ferreira, J.N. Oliveira: An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model. SBMF 2009: 153-169
  • M.A. Ferreira: Verifying Intel (R) Flash File System Core. Master Thesis, Minho University, 2009.
  • J.N. Oliveira. Hands on a Verification Challenge: Proving a Journaled File System Correct. Inforum 2010 (invited talk), 10-Sep 2010.
  • J.N. Oliveira and M.A. Ferreira. Alloy Meets the Algebra of Programming: a Case Study. Journal paper. IEEE Trans. on Soft. Engineering, 2012 (in print).

Modeling and Verifying a File System with Journaling

In a simplified approach, we used Alloy and point free manual proofs to build and verify a file system model with journaling functionality. We started with a high level file system model and refined it into a low-level implementation over an array of nodes. See J.N. Oliveira and M.A. Ferreira. Alloy Meets the Algebra of Programming: a Case Study. Journal paper. IEEE Trans. on Soft. Engineering, 2012 (in print) for a full explanation of the Alloy model.

All-in-one Verification Life-cycle

Our approach resorts to the VDMTools proof obligation generator and the VDM to HOL translator developed by Sander Vermolen. The VDM to Alloy conversion is manual. In this "all-in-one" approach, modeling and testing takes place in the VDM phase. Alloy is particularly helpful in finding counter examples to proof obligations.

  • First approach
    boneco1.png

  • Translation diagram:


    translations_diagram.png
Read arrows mean hand-translation.

  • Second approach
    In the second approach to the project we decided to reduce the complexity of the tool-chain and focus on the two bottom blocks --- Alloy model written in the "navigation-syle" so as to match with PF relation algebraic proofs. This implied that a focus on particular aspects of the problem, namely the journaling mechanism.

Verifying Intel Flash File System Core

File System Layer Models

There has been a restructuring of all models, and for that, some of them aren't available yet. If you are looking for any thing ins specific please contact us.

VDM++

  • src_vdm.tar.bz: FileSystemLayer (VDM++)
    • Implemented Operations:
      • FS_DeleteFileDir
      • FS_OpenFileDir
      • FS_WriteFile
    • Operations to be implemented:
      • FS_ReadFileDir
      • FS_Init

Alloy

  • src_alloy.tar.bz: FileSystemLayer (Alloy)
    • Implemented Operations:
      • FS_DeleteFileDir
    • Operations to be implemented:
      • FS_OpenFileDir
      • FS_WriteFile
      • FS_ReadFileDir
      • FS_Init

VDM++ adapted for VdmHolTranslator and HOL translation

Model
  • src_vdm2hol.tar.gz: FileSystemLayer (VDM2HOL)
    • Implemented Operations:
      • FS_DeleteFileDir
    • Operations to be implemented:
      • FS_OpenFileDir
      • FS_WriteFile
      • FS_ReadFileDir
      • FS_Init

Proof Obligations

  • The VDMTools generated 13 Proof Obligations, from which:
    • 3 aren't translatable to HOL with the VdmHolTranslator. These can be found in the excluded.pog file
    • 10 where translated to HOL by the VdmHolTranslator. These can be found in the FileSystemLayerAlg.vpp.pog file.
      • 7 of these Proof Obligations where discharged in HOL using the Overture Automated Proof Support
      • for the remaining 3 Proof Obligations HOL attempted to prove for more than 5 minutes and was manually interrupted.

  • HOL model and Proof Obligations can be found in the:
    • FileSystemLayerAlg.vpp.pog.hol (for the unmodified version)
    • FileSystemLayerAlg.vpp.pog.hol.mod (for the executable version)

HOL (hand written)

  • Will be published soon

Proof attempts by hand (point free style)

  • Calculation of weakest pre-condition for preservation of referential integrity invariant on open files can be found here, on Lecture 5 (page 144).

VDM to HOL model and proof obligation translation

One recent addition to the Overture project is an Automatic Proof Support system, developed by Sander Vermolen.

In our work we make much use of this system's translator, as well as the proof tactics.

We have contributed in widening the translator VDM++ syntax knowledge, implementing some basic (but essential to have recursive functions translated) operators like hd (head), tl (tail), len (length) and ^(concatenation).

Another contribution is the pre-processing script and parsers, that allow us to automaticaly pre process a VDM++ model to be translated (including its proof obligations), the complete package with source can be found here.

Team

Web References

Flash File System

  • (pdf) Intel Flash File System Core Reference Guide (Version 1)

POSIX File Store (GC)

  • (pdf) Morgan and Sufrin's paper on the Unix filing system. (Z)
  • (pdf) POSIX file store in Z/Eves: an experiment in the verified software repository
  • (ppt) Formal Modeling and Analysis of a Flash Filesystem in Alloy.
  • (pdf) Verifiable POSIX file store, technical report. (VDM)
  • (pdf) Open Nand Flash Interface, technical report. (VDM)

Formal Methods Projects and Tools

Conferences and Workshops

Other

Project Activities PICK

Research/VFS Web Utilities

-- MiguelFerreira - 15 Nov 2007

Links

News Flash

  • Refresh at public area projet information MiguelFerreira - 8 Mar 2008

  • Added the first files for the Intel Flash File System Core specification

  • Added new references on the flash memory subject MiguelFerreira - 6 Dez 2007

  • Added POSIX extracts of some system interfaces (open, mkdir, opendir, close, closedir, rmdir, unlink) MiguelFerreira - 30 Nov 2007

  • Added alloy library and updated bib file SamuelSilva - 19 Nov 2007

r43 - 02 Jul 2012 - 20:55:38 - JoseNunoOliveira
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM