[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

- 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

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 
(this one is more geared towards model checking than theorem proving)

Hope that helps,

MirageOS-devel mailing list



Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.