Towards formal verification of TLS network packet processing written in C

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 provide new Coq libraries for the formal verification of TLS packet processing written in C. The originality of our encoding of the core subset of C is 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 of which we specify and verify a parsing function for network packets. Though not yet completed, this experiment already led us to spot correctness issues with the RFC and the C source code.