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 [email protected] http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
