Hi! I'm Eduardo.

I'm an MSc student at Universidade Federal de Minas Gerais (UFMG) researching formal methods, under the supervision of Haniel Barbosa. Previously, I graduated in Computer Science at Universidade de São Paulo (USP). My current work focuses on the Lean programming language and automated program verifiers.

I'm interested in software engineering, formal verification, and programming language research and application. I enjoy working with functional and statically-typed languages, and I find it important to pursue strong theoretical foundations for software development in addition to practical knowledge.

Publications

• Foundations for Formally Verified Network Protocol Parsers in Lean 4: A Case Study with MQTT
  Eduardo Sandalo Porto, Ana C. V. de Melo
  30th Brazilian Symposium on Programming Languages (SBLP 2026)
  [paper] [slides] [code]
  abstract

  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.

• Integrating NWDAF and Federated Learning for Privacy-Preserving Intrusion Detection in B5G IoHT Networks
  E. K. Cruz Ortega, Eduardo Sandalo Porto, Ana C. V. de Melo, Daniel Macêdo Batista
  IEEE Networking Letters, vol. 8, pp. 273–276
  [doi]
  abstract

  The combination of Federated Learning and the Network Data Analytics Function (NWDAF) enables new possibilities for smart, secure, and privacy-aware network analysis in Beyond 5G (B5G) environments. In this work, we present a framework that explores this analysis to support distributed intrusion detection in the Internet of Healthcare Things (IoHT) scenario. Experimental results show that the system achieves stable convergence, with accuracy levels around 90% and high recall for major attack classes. Additionally, server-side Differential Privacy mechanisms maintain a reasonable privacy-utility balance. These findings demonstrate the feasibility of performing practical intrusion detection while preserving confidentiality in B5G-enabled IoHT environments.

Contact

You can reach me at:

• Email: [email protected]
• Academic email: [email protected]
• LinkedIn: linkedin.com/in/edusporto
• GitHub: github.com/edusporto

Posts

• De onde vem o RegEx? (rascunho) - August 9, 2023 (in Portuguese)

...you can find more here.