Re: [MirageOS-devel] Security Protocol Analyzers

[Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx>]

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.  

Daniel



_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel