I took a look at the deep specs site, as it seemed like this would be related to that project, but I didn’t see anything directly. The existence of deepspecs (and the project to make a formally verified web server) indicates to me that this is probably still an area of active research/development, but I’d love to know what the state of the art is, and what theory theory is backing things up. I’m really curious what a formally verified protobufs would look like, especially how the boundary of “this is verified” and “this can’t be” comes into play given the nature of communication over a network…Coq can verify the actions taken by the client, but it can make absolutely no guarantees about the bits it gets, and I’m not sure how you’d model that (or if it would be worthwhile to model?)
Hi @jco, I’m not very familiar with the technical details of the deepspec project so I will leave that part to insiders (maybe @Lyxia ?), but with respect to the question “how to specify a piece of network stack” I can bring your attention to the project everest whose goal is to build a fully formal HTTPS stack (not in Coq though, in F*). In particular they do use verified parser to validate the input data they get from clients and enforce the invariants they require dynamically (and there are libraries for writing verified parser in Coq, for instance Narcissus seems to provide that kind of feature).
Hope it is not too much of a sidetrack.
Totally seems relevant! Not a sidetrack! (though honestly I also always like me a good side track) I imagine they’re producing papers and whatnot that would be directly relevant to what I’m interested in. I have no clue what F* is like but can’t help to explore a bit
I’m really curious what a formally verified protobufs would look like
Check out A Verified Protocol Buffer Compiler, Qianchuan Ye and Benjamin Delaware (https://www.cs.purdue.edu/homes/bendy/Narcissus/index.html) https://www.cs.purdue.edu/homes/bendy/Narcissus/VerifiedProtoBuff.html)