[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [MirageOS-devel] Security Protocol Analyzers

Hi Michele,

> Reading Mirage's FAQ <https://mirage.io/wiki/faq> I noticed that mirage
> has been a bit involved with the formal methods community.
> I would be super-interested in knowing if anybody has ever produced an
> (automated) formal proof of the security of component X in mirage, or if
> there's any interest in doing this; unfortunately I couldn't find
> anything on the inter web. 

To my knowledge, no components of MirageOS have a full formal proof. There are 
various on-going formalisation efforts around TLS[1] and TCP (lead by David and 
Hannes) and few other people have expressed interest into formalising packet 
parsing code with Coq but this hasn't lead to something concrete yet.

I am very interested by anything going into that direction, so any 
formalisation contribution is *very* welcome :-)

[1]: https://nqsb.io/
MirageOS-devel mailing list



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