Foundations for Formally Verified Network Protocol Parsers in Lean 4: A Case Study with MQTT
Resumo
A significant portion of the Internet’s critical infrastructure relies on the precise implementation of network protocols, yet bridging the gap between formal verification and applied network engineering remains a challenge. In this paper, we present a case study in implementing and formally verifying a parser for the MQTT 5.0 protocol using Lean 4. Our approach includes three components: (I) correct-by-construction modeling of the packet format, leveraging dependent types to preclude invalid packets and encode data-dependent structural variations; (II) a layered, proof-carrying parser library utilizing state monads to process inputs whose exact layout depends on runtime parsed values; and (III) formal verification of parser completeness (roundtrip) and soundness (reconstruction) with respect to a serializer. Ultimately, this work serves as a foundational step toward a generalized, embedded domain-specific language for generating verified network protocol parsers.
Palavras-chave:
Formal Verification, Parser Combinators, Dependent Types, Network Protocols, Domain-Specific Languages, Lean 4
Referências
Sabina Akhtar and Ehtesham Zahoor. 2021. Formal Specification and Verification of MQTT Protocol in PlusCal-2. Wirel. Pers. Commun. 119, 2 (July 2021), 1589–1606. DOI: 10.1007/s11277-021-08296-4
Andrew Banks, Ed Hurlburt, and Rahul Gupta. 2019. MQTT Version 5.0. Technical Report. OASIS Standard. [link]
David Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, and Lenore D. Zuck. 2025. It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. Commun. ACM 68, 8 (July 2025), 50–61. DOI: 10.1145/3706572
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, and Bryan Parno. 2025. Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust. In Proceedings of the USENIX Security Symposium.
Nils Anders Danielsson. 2010. Total parser combinators. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP ’10). Association for Computing Machinery, New York, NY, USA, 285–296. DOI: 10.1145/1863543.1863585
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. 2019. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3, ICFP (July 2019), 82:1–82:29. DOI: 10.1145/3341686
Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and AndrewWells. 2024. HowWe Built Cedar: A Verification-Guided Approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024). Association for Computing Machinery, New York, NY, USA, 351–357. DOI: 10.1145/3663529.3663854
Amina Jandoubi, M. Bennani, Olfa Mosbahi, and Abdelaziz El Fazziki. 2024. Analyzing MQTT Attack Scenarios: A Systematic Formalization and TLC Model Checker Simulation:. In Proceedings of the 19th International Conference on Evaluation of Novel Approaches to Software Engineering. SCITEPRESS - Science and Technology Publications, Angers, France, 370–378. DOI: 10.5220/0012625600003687
Wei Lin, Sini Chen, and Huibiao Zhu. 2025. Formal verification and security analysis of MQTT-SN. International Journal on Software Tools for Technology Transfer 27, 1 (Feb. 2025), 5–19. DOI: 10.1007/s10009-025-00793-2
Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 625–635. DOI: 10.1007/978-3-030-79876-5_37
William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings of the 1991 ACM/IEEE Conference on Supercomputing (Albuquerque, New Mexico, USA) (Supercomputing ’91). Association for Computing Machinery, New York, NY, USA, 4–13. DOI: 10.1145/125826.125848
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. Everparse: verified secure zero-copy parsers for authenticated message formats. In Proceedings of the 28th USENIX Conference on Security Symposium (SEC’19). USENIX Association, USA, 1465–1482.
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, and Nikhil Swamy. 2025. Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS ’25). Association for Computing Machinery, New York, NY, USA, 2744–2758. DOI: 10.1145/3719027.3765120
Tillmann Rendel and Klaus Ostermann. 2010. Invertible syntax descriptions: unifying parsing and pretty printing. In Proceedings of the third ACM Haskell symposium on Haskell (Haskell ’10). Association for Computing Machinery, New York, NY, USA, 1–12. DOI: 10.1145/1863523.1863525
Alejandro Rodríguez, Lars Michael Kristensen, and Adrian Rutle. 2019. Formal Modelling and Incremental Verification of theMQTT IoT Protocol. In Transactions on Petri Nets and Other Models of Concurrency XIV, Maciej Koutny, Lucia Pomello, and Lars Michael Kristensen (Eds.). Vol. 11790. Springer Berlin Heidelberg, Berlin, Heidelberg, 126–145. DOI: 10.1007/978-3-662-60651-3_5, Series Title: Lecture Notes in Computer Science.
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022. Hardening attack surfaces with formally proven binary format parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 31–45. DOI: 10.1145/3519939.3523708
Ibtissem Talamali, Razika Lounas, and Mohamed Mezghiche. 2024. Formal Specification and Verification of MQTT Protocol Using CoQ Proof Assistant. In 2024 International Conference on Advanced Aspects of Software Engineering (ICAASE). 1–6. DOI: 10.1109/ICAASE64542.2024.10850926
Andrew Banks, Ed Hurlburt, and Rahul Gupta. 2019. MQTT Version 5.0. Technical Report. OASIS Standard. [link]
David Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, and Lenore D. Zuck. 2025. It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. Commun. ACM 68, 8 (July 2025), 50–61. DOI: 10.1145/3706572
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, and Bryan Parno. 2025. Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust. In Proceedings of the USENIX Security Symposium.
Nils Anders Danielsson. 2010. Total parser combinators. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP ’10). Association for Computing Machinery, New York, NY, USA, 285–296. DOI: 10.1145/1863543.1863585
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. 2019. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3, ICFP (July 2019), 82:1–82:29. DOI: 10.1145/3341686
Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and AndrewWells. 2024. HowWe Built Cedar: A Verification-Guided Approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024). Association for Computing Machinery, New York, NY, USA, 351–357. DOI: 10.1145/3663529.3663854
Amina Jandoubi, M. Bennani, Olfa Mosbahi, and Abdelaziz El Fazziki. 2024. Analyzing MQTT Attack Scenarios: A Systematic Formalization and TLC Model Checker Simulation:. In Proceedings of the 19th International Conference on Evaluation of Novel Approaches to Software Engineering. SCITEPRESS - Science and Technology Publications, Angers, France, 370–378. DOI: 10.5220/0012625600003687
Wei Lin, Sini Chen, and Huibiao Zhu. 2025. Formal verification and security analysis of MQTT-SN. International Journal on Software Tools for Technology Transfer 27, 1 (Feb. 2025), 5–19. DOI: 10.1007/s10009-025-00793-2
Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 625–635. DOI: 10.1007/978-3-030-79876-5_37
William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings of the 1991 ACM/IEEE Conference on Supercomputing (Albuquerque, New Mexico, USA) (Supercomputing ’91). Association for Computing Machinery, New York, NY, USA, 4–13. DOI: 10.1145/125826.125848
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. Everparse: verified secure zero-copy parsers for authenticated message formats. In Proceedings of the 28th USENIX Conference on Security Symposium (SEC’19). USENIX Association, USA, 1465–1482.
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, and Nikhil Swamy. 2025. Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS ’25). Association for Computing Machinery, New York, NY, USA, 2744–2758. DOI: 10.1145/3719027.3765120
Tillmann Rendel and Klaus Ostermann. 2010. Invertible syntax descriptions: unifying parsing and pretty printing. In Proceedings of the third ACM Haskell symposium on Haskell (Haskell ’10). Association for Computing Machinery, New York, NY, USA, 1–12. DOI: 10.1145/1863523.1863525
Alejandro Rodríguez, Lars Michael Kristensen, and Adrian Rutle. 2019. Formal Modelling and Incremental Verification of theMQTT IoT Protocol. In Transactions on Petri Nets and Other Models of Concurrency XIV, Maciej Koutny, Lucia Pomello, and Lars Michael Kristensen (Eds.). Vol. 11790. Springer Berlin Heidelberg, Berlin, Heidelberg, 126–145. DOI: 10.1007/978-3-662-60651-3_5, Series Title: Lecture Notes in Computer Science.
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022. Hardening attack surfaces with formally proven binary format parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 31–45. DOI: 10.1145/3519939.3523708
Ibtissem Talamali, Razika Lounas, and Mohamed Mezghiche. 2024. Formal Specification and Verification of MQTT Protocol Using CoQ Proof Assistant. In 2024 International Conference on Advanced Aspects of Software Engineering (ICAASE). 1–6. DOI: 10.1109/ICAASE64542.2024.10850926
Publicado
08/09/2026
Como Citar
PORTO, Eduardo Sandalo; MELO, Ana Cristina Vieira de.
Foundations for Formally Verified Network Protocol Parsers in Lean 4: A Case Study with MQTT. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 30. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 178-183.
DOI: https://doi.org/10.5753/sblp.2026.28568.
