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

Re: [MirageOS-devel] Security Protocol Analyzers

Le mardi, 15 dÃcembre 2015 Ã 00:27, Thomas Gazagnaire a Ãcrit :
> 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 :-)
Well I can provide you with many tautological formalisations for any component 
of MirageOS, hence I bet you are not interested about *any* formalisation.

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.  


MirageOS-devel mailing list



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