Verifiable Filesystem

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

The last challenge released intents to specify the standard POSIX 1003.1, which is in fact an enourmous 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. Further more, the proponents of the mini-challenge, have also introduced a project, that is being carried out at NASA Jet Propulsion Laboratory, which goal is to build such a verifiable file system but designed for use directly in Flash Memories.

The goal of this project is to respond to the mini-challenge, taking in account the Flash Memory specificity has hardware support for the file system. Following established techniques , as well as new in sights 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

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
  

• Point free structuring approach
  

• Translation diagram:
  
  
  

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