|
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] Re: [MirageOS-devel] Security Protocol Analyzers
On 15 Dec 2015, at 09:00, Michele Orrà <lists@xxxxxxxxxxxxxxx> wrote: > > Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx> writes: > >> So my question to you and Michele is what properties are you actually >> interested to prove ? The notion of "full formal proof" for itself >> doesn't make much sense. >> >> This even more that most standard protocols out there neither have a >> formal model of legal message exchange beyond a few ambiguous natural >> language assertions, nor do they come up with an actual model in which >> the properties they are supposed to guarantee can be asserted. > > This may be right, but - and please correct me if I'm wrong - for > example you can still try to prove formally that a Dolev-Yao adversary > is never able to retrieve the shared key in a DH key exchange, or in a > TLS session the master secret is never leaked. > It's not much as it doesn't require a statistical or computational > assumptions, but it's a start isn't it? > >  by "prove formally X" I specifically mean "show that the closure on the > reductions (specified by $MODEL adversary) of the messages transmitted > has property $PROPERTY". MirageOS is composed of a series of OCaml libraries, and some of those are amenable to mechanised reasoning. There are no whole system proofs. Some examples: - SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems Tom Ridge, David Sheets, Thomas Tuerk, Anil Madhavapeddy, Andrea Giugliano and Peter Sewell in the 25th ACM Symposium on Operating Systems Principles (SOSP), October 2015 http://anil.recoil.org/papers/2015-sosp-sibylfs.pdf - Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation David Kaloper Mersinjak, Hannes Mehnert, Anil Madhavapeddy and Peter Sewell to appear in the 24th USENIX Security Symposium (UseSec15), August 2015 http://anil.recoil.org/papers/2015-usenixsec-nqsb.pdf Raft Refloated: Do We Have Consensus? Heidi Howard, Malte Schwarzkopf, Anil Madhavapeddy and Jon Crowcroft in ACM SIGOPS Operating System Review special issue on Repeatability and Sharing of Experimental Artifacts, January 2015 http://anil.recoil.org/papers/2014-sigops-raft.pdf (this one is more geared towards model checking than theorem proving) Hope that helps, Anil _______________________________________________ MirageOS-devel mailing list MirageOS-devel@xxxxxxxxxxxxxxxxxxxx http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
|
 |
Lists.xenproject.org is hosted with RackSpace, monitoring our |