摘要：TLS is such a widespread security protocol that errors in its implementation can have disastrous consequences. This responsibility is mostly borne by programmers, caught between specifications with the ambiguities of natural language and error-prone low-level parsing of network packets. We report here on the construction in the Coq proof-assistant of libraries to model, specify, and verify C programs to process TLS packets. We provide in particular an encoding of the core subset of C whose originality lies in its use of dependent types to guarantee statically well-formedness of datatypes and correct typing. We further equip this encoding with a Separation logic that enables byte-level reasoning and also provide a logical view of data structures. We also formalize a significant part of the RFC for TLS, again using dependent types to capture succinctly constraints that are left implicit in the prose document. Finally, we apply the above framework to an existing implementation of TLS (namely, PolarSSL) of which we specify and verify a parsing function for network packets. Thanks to this experiment, we were able to spot ambiguities in the RFC and to correct bugs in the C source code.
