GitXplorerGitXplorer
m

fscq

public
234 stars
20 forks
5 issues

Commits

List of commits on branch master.
Unverified
231cf25829d399f467c9e23fd593d5f5c74399b1

Remove python2 dependency

ttchajed committed 3 years ago
Unverified
19b13f4ae3943260d92f71c8cec86f76b41f836b

Implement ftruncate correctly in Coq

ttchajed committed 5 years ago
Unverified
2e95abaa1da43f0d64fce1a5ee47e85dae9985ab

add a warning that fscq is not maintained

zzeldovich committed 5 years ago
Unverified
09317a991a5d2ee653ce0d1cd224bb7d4180823a

Improve debug output

ttchajed committed 5 years ago
Unverified
59bbd4c31b21d012bce375bda9103c41a6d22a17

Print disk layout information in mkfs

ttchajed committed 5 years ago
Unverified
2e16c020f4d57f4e50bd9efcb4cc289693d7f48d

Fix issues with latest Coq master

ttchajed committed 5 years ago

README

The README file for this repository.

FSCQ

FSCQ is a file system written and verified in the Coq proof assistant.

Unmaintained research prototype

Warning: the FSCQ software is not maintained. FSCQ's core is verified in Coq, but FSCQ also includes components written in Haskell for interacting with FUSE, and depends on FUSE and Haskell bindings for FUSE, none of which are verified. The unverified portions are likely to have bugs, and we do not recommend that anyone use the FSCQ research prototype in practice.

Although the overall software is not maintained, we would be interested in hearing from others that discover issues with the verified portions of FSCQ.

Branches

There are several branches in this repository, corresponding to different FSCQ-related projects.

  • The master branch contains the source code for the DFSCQ file system, roughly corresponding to the SOSP 2017 paper.

  • The security branch contains the source code for the SFSCQ file system and the DiskSec sealed block framework, roughly corresponding to the OSDI 2018 paper.