Certified Synthesis of High-Assurance Protocols and Monitors

ABSTRACT

Communication protocols govern every safety-critical cyber-physical system, yet the gap between a formally verified protocol model and the code that actually executes has remained an open problem [4,3]. Tools such as TLA+ [7] verify models in isolation, session type frameworks provide structural guarantees but cannot prove application-specific safety properties, and no prior work has mechanized the metatheory of Refined Multiparty Session Types (RMPSTs) [8,6], leaving correctness guarantees resting on hand-written proofs. Addressing the HCSS theme of Verifiable Automatic Code Generation, we present a unified F* framework that closes this gap: safety properties proved over a shared formal model extend to every artifact the framework synthesizes.

The framework displayed in Figure 1 comprises three composing contributions. Facet provides the first mechanized RMPST metatheory, proving eight core theorems, including deadlock freedom, subject reduction, and runtime soundness, by construction for any protocol written in our DSL. F*ACT is a proof automation framework that connects protocol conformance to application specific physical safety: given a protocol specification and a system model with a distinguished Wrong state encoding unsafe configurations, F*ACT proves via bisimulation that no conforming execution trace reaches Wrong, using automated nuXmv model generation for finite-state protocols and Meta-F* tactics dispatching to Z3 for protocols with larger data domains. Platum synthesizes allocation-free C finite state machines directly from verified F* specifications, enabling deployment on resource-constrained hardware with 13.3 µs per-message overhead and no garbage collection.

The composition theorem is the central result: because all three tools extract from the same RCFSM deep embedding over which safety is proved, verified implementations, distributed runtime monitors, and C proxy monitors for legacy systems all inherit the safety guarantee without independent re-verification. We demonstrate the framework on MAVLink and Modbus [1,2,5], two of the most widely deployed industrial protocols, showing that stealthy attacks – sequences of individually valid commands that drive a system into an unsafe state – are blocked at runtime.

Fig. 1:  A single high-level specification feeds a safety proof framework and generates three verified artifacts: static OCaml implementations, distributed TCP/IP monitors, and C runtime monitors

References

  • Amorim, A., Taylor, M., Kann, T., Harrison, W.L., Leavens, G.T., Joneckis, L.: Enforcing MAVLink Safety & Security Properties via Refined Multiparty Session Types. In: Dutle, A., Humphrey, L., Titolo, L. (eds.) NASA Formal Methods. pp. 1–10. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/978-3-031-93706-4_ 1 
  • Amorim, A., Taylor, M., Kann, T., Leavens, G.T., Harrison, W.L., Joneckis, L.: UAV Resilience Against Stealthy Attacks. In: 2025 International Conference on Unmanned Aircraft Systems (ICUAS). pp. 994–1001 (May 2025). https://doi.org/10.1109/ICUAS65942.2025.11007915, https://ieeexplore.ieee.org/abstract/ document/11007915 3. 
  • Kulik, T., Dongol, B., Larsen, P.G., Macedo, H.D., Schneider, S., Tran-Jørgensen, P.W.V., Woodcock, J.: A Survey of Practical Formal Methods for Security. Form. Asp. Comput. 34(1), 5:1–5:39 (Jul 2022). https://doi.org/10. 1145/3522582, https://dl.acm.org/doi/10.1145/3522582 
  • Lee, E.A.: The past, present and future of cyber-physical systems: a focus on models. Sensors 15(3), 4837–4869 (Feb 2015). https://doi.org/10.3390/s150304837 
  • Taylor, M., Amorim, A., Joneckis, L.: Securing Modbus-Based Industrial Control Systems with Refined Multiparty Session Types. In: 2025 Annual Computer Security Applications Conference Workshops (ACSAC Workshops). pp. 99–109 (Dec 2025). https://doi.org/10.1109/ACSACW69556.2025.00016, https://ieeexplore.ieee.org/ abstract/document/11418027 
  • Vassor, M., Yoshida, N.: Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation. In: Aldrich, J., Salvaneschi, G. (eds.) 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 313, pp. 41:1– 41:29. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, Dagstuhl, Germany (2024). https://doi.org/10.4230/ LIPIcs.ECOOP.2024.41, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.41 
  • Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods. pp. 54–66. CHARME ’99, Springer-Verlag, Berlin, Heidelberg (Sep 1999) 
  • Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proceedings of the ACM on Programming Languages 4(OOPSLA), 1–30 (2020)

BIO

Arthur Amorim is a Ph.D. candidate in Computer Science at the University of Central Florida, advised by Dr. Gary T. Leavens, with an expected graduation of July 2026. Since 2022, he has been a formal methods researcher at Idaho National Laboratory's National and Homeland Security Directorate, where he leads development of SPECTRE: a framework for specification, verification, and deployment of safe cyber-physical protocols utilizing the F* theorem prover. His research focuses on closing the gap between formally verified protocol models and deployed code, with applications to UAV systems (MAVLink/ArduPilot/PX4) and industrial control systems (Modbus). His work spans the full stack: RMPST metatheory mechanized in F*, system-specific safety proofs, and the extraction of high-assurance protocol implementations and runtime monitors.
Submitted by Katie Dey on