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
  

• Translation diagram:
  
  
  

• 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

• JoseNunoOliveira
• MiguelFerreira [ miguel(at)di(dot)uminho(dot)pt ]
• SamuelSilva [ silva(dot)samuel(at)alumni(dot)uminho(dot)pt ]

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

• Overture - Open-source Tools for Formal Modelling
• VDMTools
• Alloy
• HOL

Conferences and Workshops

• ABZ call for papers on the POSIX pilot project in the Grand Challenge
• VDM-Overture 4th Workshop, FM08, Turku, 26 May 2008
• Pilot Projects for the Grand Challenge in Verified Software, FM08, Turku, 27 May 2008
• Workshop on the Verifiable File Store Mini-Challenge, BCS offices, London, 18 Dec 2007

Other

• Verified File-System
• OLVER (Open Linux VERification)
• Linux

Project Activities

• ProjectFiles at Trac

Research/VFS Web Utilities

-- MiguelFerreira - 15 Nov 2007