Re: [MirageOS-devel] Security Protocol Analyzers

[Thomas Gazagnaire <thomas@xxxxxxxxxxxxxx>]

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 :-)

Best,
Thomas
[1]: https://nqsb.io/
_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel