An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing
Keywords:C language, TLS protocol, Coq
AbstractTLS 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.
How to Cite
Affeldt, R., & Sakaguchi, K. (2014). An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. Journal of Formalized Reasoning, 7(1), 63–104. https://doi.org/10.6092/issn.1972-5787/4317
Copyright (c) 2014 Reynald Affeldt, Kazuhiko Sakaguchi
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy