See recent updates and contact information at:
http://locore.cs.washington.edu/yggdrasil/
We have tested it using the following setup:
Install these packages before proceeding. Other platforms or versions may not work.
To compile:
$ make all prod
To mount:
$ python2 yav_xv6_main.py -o max_read=4096 -o max_write=4096 -s a -- /dev/sXX
To run verification:
$ make verify
If your system doesn't have cython2
, you may want to change it
to cython
in the makefile (similarly for python2
).
The proof is that a file system implementation is a crash refinement of its specification. See the OSDI'16 paper for details.
Note that this does not mean that a verified file system in Yggdrasil has zero bugs. There can be bugs in the specification (or things not modeled by the specification, like error code), the verification toolchain, and the unverified part (e.g., the glue code to FUSE, FUSE itself, and the Linux kernel).
This implementation of Yxv6 is a clean-up version. It mostly follows the design described in the OSDI'16 paper, with a few differences:
You may notice changes in runtime performance and verification time depending on your platform and tools (e.g., Z3).
Yxv6 is a research prototype. The implementation has the following limitations:
We don't think they are necessarily fundamental limitations of the toolkit---feel free to send us pull requests if you add some of these features.