How to verify an ASN.1 Protocol C-language Stack in Coq?
We describe our approach to verification of a mature open-source ASN.1 compiler, ASN1C (written in C), using the Coq proof assistant and Verified Software Toolchain. As a proof of concept, we verified data encoders and decoders for integer and boolean types of ASN1C, as well as important generic auxiliary functions that write and check tags and lengths of any encoded/decoded data. We summarize the results of this phase of the project and the verification architecture we settled on. Once completed, our project will provide state-of-the-art high assurance suitable for mission-critical systems. Furthermore, since formal verification will be layered atop a well-tested ASN.1 stack, it will combine the benefits of high-performance portable stack implementation with formal correctness guarantees. As an essential step in our approach, we provide a Coq formalization of a key part of the ASN.1 standard. Such formal specification could subsequently be used by others to analyze ASN.1 properties and validate other implementations.
|How to verify an ASN.1 Protocol C-language Stack in Coq? (slides) (POPL2021_presentation.pdf)||63KiB|