search

microsoft / Ironclad

The MSR Ironclad project builds provably secure and reliable systems.
http://research.microsoft.com/en-us/projects/ironclad/
Other
242 stars 56 forks source link

Organization of this repo #6

Open gshanemiller opened 3 years ago

gshanemiller commented 3 years ago

I ran into Dafny from a post in https://blog.acolyer.org/2015/10/15/ironfleet-proving-practical-distributed-systems-correc/ which I found to be of great interest. However, I found this repo to be difficult to understand ... there doesn't seem to be well defined boundaries between examples where they start or stop ... it's unclear how to load any of these examples ... I have a sense there's Dafny library code here that might be re-used but that's not entirely clear either. Can we reorg this or can the maintainers give a road map of what this is supposed to communicate?

Somewhat unrelated ... does Dafny come with Verdi's formally proved library which represents error free, exactly once delivery of messages, or possibly droppep/dup messages? See https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf for the description there. Also see: https://github.com/uwplse/verdi. Dafny seems to go further than other formal tools at continuously refining down from spec to more runnable code and it'd be a shame to let this work flounder. Verdi also wants to improve here, but Verdi doesn't do liveness checks.

Finally, is Dafny supposed to be a model checker ala SPIN/TLA+ or proof oriented ala Coq/Verdi? Dafny seems to be proof oriented.

Regards

parno commented 3 years ago

This repository is mostly capturing the code involved in two research projects on building verified code. Both make use of Dafny, which is a separate language and tool with its own repository. That repository is much more accessible and has lots of pointers on documentation and how to get started with Dafny, so I would encourage you to check that out.

Verdi is a separate project from the University of Washington. It is formalized in a language/tool called Coq, which is quite different from Dafny, although both are designed to be sound verification tools, as opposed to model checkers.. Our IronFleet work does include a provably safe "reliable delivery" layer that's similar to Verdi's, although ours is integrated (somewhat intimately) with our sharded hash table, rather than cleanly factored out as in Verdi.

I hope this helps clarify the various relationships involved here.