From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Arthur Amorim; Lance Joneckis; Max Taylor; Paul Gazzillo

arxiv: 2604.03886 · v1 · submitted 2026-04-04 · 💻 cs.CR · cs.FL

From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Arthur Amorim , Paul Gazzillo , Max Taylor , Lance Joneckis This is my paper

Pith reviewed 2026-05-13 16:48 UTC · model grok-4.3

classification 💻 cs.CR cs.FL

keywords MAVLinksession typesruntime monitoringfinite state machinesprotocol verificationUAV securityC code synthesiscontextual validity

0 comments

The pith

Platum compiles minimal session types into verified flat C finite state machines for MAVLink monitoring

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that MAVLink protocol enforcement can be achieved by writing specifications in a minimal DSL and automatically verifying and compiling them to efficient C code. This addresses the limitations of prior work that required manual proofs and incompatible runtimes. A sympathetic reader would care because it enables practical deployment of runtime checkers on resource-constrained UAV hardware to prevent stealthy attacks from ill-timed commands. The approach reduces monitor latency by a factor of four while maintaining verification guarantees.

Core claim

Platum addresses both engineering failures of prior work with a minimal DSL requiring only the five semantic components of a global session type, whose structural well-formedness conditions are confirmed via reflective decision procedures, and compiles directly into flat, allocation-free C Finite State Machines that achieve a 4x reduction in total monitor latency.

What carries the argument

Minimal DSL with five components (sender, receiver, label, payload variable, refinement predicate) that carries the argument by enabling reflective verification and direct compilation to C FSMs.

If this is right

Monitors deploy as centralized proxies at the GCS/UAV communication boundary.
Well-formedness conditions are confirmed automatically via decision procedures.
Generated monitors achieve a 4x reduction in total latency and lower memory overhead.
Allocation-free FSMs run directly on embedded UAV hardware without managed runtime.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The synthesis approach could extend to enforcing sequence constraints in other communication protocols used by embedded systems.
Automated verification of refinements might help identify additional classes of contextual attacks not caught by syntax checks alone.
Results from simulation suggest direct measurement on physical flight hardware to confirm behavior under real timing conditions.

Load-bearing premise

The five-component DSL plus reflective decision procedures are sufficient to capture all contextual validity constraints of MAVLink and that the generated C FSMs preserve the semantics of the original session types.

What would settle it

Observe whether the generated C FSMs reject a crafted sequence of syntactically valid but semantically invalid MAVLink messages that would induce unsafe states, or if they allow such sequences to pass without performance regressions on target hardware.

Figures

Figures reproduced from arXiv: 2604.03886 by Arthur Amorim, Lance Joneckis, Max Taylor, Paul Gazzillo.

**Figure 1.** Figure 1: The Platum Workflow. The compile-time pipeline (above the dotted line) proceeds from F* specification, through AST decomposition and Meta-F* well-formedness checking, to C monitor synthesis. The runtime deployment (below the dotted line) shows the synthesized monitor operating as a centralized proxy: the GCS transmits MAVLink traffic to Platum, which enforces the global session type at the network boundar… view at source ↗

**Figure 2.** Figure 2: RMPST Formalization of the MAVLink Mission Protocol – Branching and Choice: The ⊕ operator represents internal choice; the sender selects a branch whose refinement constraint is satisfied. In the mission protocol, the UAV either requests the next item or acknowledges completion. The complete, value-dependent formalization of the mission protocol appears in [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** Figure 3: The reification pipeline. The meta-program inspects the F* AST (top), mapping logical operators like op_Logical_And to C’s &&, and resolving the variable x to its runtime location payload.x. We define the monitor state as a C structure containing the context variables identified during the AST analysis. The logic is encapsulated in a stateless step [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

read the original abstract

Standard communication protocols for Unmanned Aerial Vehicles (UAVs), such as MAVLink, lack the capability to enforce the contextual validity of message sequences. Autopilots therefore remain vulnerable to stealthy attacks, where syntactically correct but semantically ill-timed commands induce unsafe states without triggering physical anomaly detectors. Prior work (DATUM) demonstrated that global Refined Multiparty Session Types (RMPSTs) are an effective specification language for centralized MAVLink protocol enforcement, but suffered from two engineering failures: manual proof terms interleaved with protocol definitions, and an OCaml extraction backend whose managed runtime is incompatible with resource-constrained UAV hardware. We present Platum, a framework that addresses both failures with a minimal DSL requiring only the five semantic components of a global session type (sender, receiver, label, payload variable, refinement predicate), whose structural well-formedness conditions are confirmed via reflective decision procedures in Meta-F*. Confirmed specifications are compiled directly into flat, allocation-free C Finite State Machines (FSMs), deployed as centralized proxy monitors at the GCS/UAV communication boundary. Our evaluation demonstrates a 4x reduction in total monitor latency and lower memory overhead compared to DATUM, measured via ArduPilot SITL simulation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Platum gives a workable path from minimal session-type specs to allocation-free C monitors for MAVLink, but the end-to-end correctness link between DSL and generated FSMs is not shown.

read the letter

The main point is that this paper fixes the two practical blockers from the earlier DATUM work: it replaces manual proof terms with a tiny five-component DSL and swaps the OCaml backend for direct generation of flat C state machines that run without allocation or managed runtime. That combination lets the monitors sit as a proxy at the GCS-UAV boundary on real hardware constraints. The Meta-F* reflective checks for structural well-formedness are a clean engineering choice that avoids interleaving proofs with the protocol description. The claimed 4x latency drop in ArduPilot SITL is the sort of concrete number that matters for deployment, even if the raw data and test scenarios are not detailed here. Credit is due for shipping an actual compilation path that targets the resource limits of UAV code rather than stopping at an extracted interpreter. The soft spot is the missing correspondence between the DSL transitions plus predicates and the behavior of the generated C FSMs. The abstract states that confirmed specs compile directly to FSMs, yet there is no visible theorem, extracted proof, or even informal argument showing that payload decoding and predicate evaluation in C preserve the original RMPST semantics exactly. Any mismatch there would change what the monitor actually accepts. The evaluation claim also sits on unshown numbers, so it is hard to judge how robust the 4x figure is across different message loads or hardware. This work is aimed at people who need verified runtime checks for embedded communication protocols, particularly in UAV or other safety-critical settings. A reader already familiar with session types and Meta-F* will get the most out of the engineering details and the minimal DSL design. The paper deserves a serious referee because the practical advance is real and the formal gap is fixable rather than fatal; the core claim is worth checking against the full proofs and generated code.

Referee Report

2 major / 0 minor

Summary. The paper presents Platum, a framework that uses a minimal DSL consisting of the five semantic components of a global session type (sender, receiver, label, payload variable, refinement predicate) to specify MAVLink protocols. Structural well-formedness is checked via reflective decision procedures in Meta-F*, and specifications are compiled directly to flat, allocation-free C finite state machines deployed as centralized monitors at the GCS/UAV boundary. The work claims to resolve the manual-proof and runtime-incompatibility issues of prior DATUM work while delivering a 4x reduction in total monitor latency, measured in ArduPilot SITL simulation.

Significance. If the compilation preserves the semantics of the original RMPSTs (including refinement predicates) and the performance numbers hold under realistic conditions, the result would provide a practical route to verified, low-overhead protocol enforcement on resource-constrained UAV hardware, directly addressing stealthy command-sequence attacks that current anomaly detectors miss.

major comments (2)

[Abstract] Abstract: the central performance claim of a '4x reduction in total monitor latency' is stated without any quantitative data, error bars, exact test scenarios, or comparison baselines from the ArduPilot SITL runs; this datum is load-bearing for the claim that the C FSM backend is practically superior to DATUM.
[Abstract] Abstract and compilation section: no end-to-end correspondence theorem or machine-checked proof is provided that the generated flat C FSMs preserve the acceptance language and refinement-predicate semantics of the original RMPSTs under the minimal DSL; any mismatch in payload decoding or predicate evaluation would silently alter the monitored behavior.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on arXiv:2604.03886. We address each major comment below and indicate planned revisions to strengthen the manuscript.

read point-by-point responses

Referee: [Abstract] Abstract: the central performance claim of a '4x reduction in total monitor latency' is stated without any quantitative data, error bars, exact test scenarios, or comparison baselines from the ArduPilot SITL runs; this datum is load-bearing for the claim that the C FSM backend is practically superior to DATUM.

Authors: We agree that the abstract would be strengthened by including supporting quantitative details. The full evaluation section reports the ArduPilot SITL results with specific average latencies, standard deviations, exact test scenarios (including message sequences and payload sizes), and direct DATUM baselines that establish the 4x reduction. We will revise the abstract to incorporate these key figures and error bars. revision: yes
Referee: [Abstract] Abstract and compilation section: no end-to-end correspondence theorem or machine-checked proof is provided that the generated flat C FSMs preserve the acceptance language and refinement-predicate semantics of the original RMPSTs under the minimal DSL; any mismatch in payload decoding or predicate evaluation would silently alter the monitored behavior.

Authors: This is a fair observation. The compilation maps the five DSL components directly to C FSM states, transitions, and predicate evaluations to preserve semantics by construction, with Meta-F* ensuring well-formedness upfront. However, the current manuscript does not include a machine-checked correspondence theorem. We will expand the compilation section with a detailed informal semantic preservation argument covering acceptance languages and refinement predicates, while explicitly noting the lack of a formal theorem as a limitation. revision: partial

Circularity Check

0 steps flagged

No significant circularity; new DSL and compiler are independent of prior DATUM result

full rationale

The paper defines a new minimal DSL using only five semantic components of global session types, confirms well-formedness via reflective Meta-F* procedures, and compiles directly to flat allocation-free C FSMs. Performance claims rest on fresh ArduPilot SITL simulation measurements rather than any fitted parameters or equations derived from the same inputs. The reference to prior DATUM work provides context for the engineering failures being addressed but does not serve as a load-bearing premise that reduces the new contributions to self-citation or definition; the derivation chain from DSL to generated monitors remains self-contained and externally measurable.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Abstract-only review; the approach rests on the domain assumption that session types can express all relevant MAVLink sequencing constraints and that Meta-F* decision procedures correctly decide the well-formedness conditions. No free parameters or invented entities are mentioned.

axioms (2)

domain assumption Global session types with sender, receiver, label, payload variable, and refinement predicate are sufficient to specify contextual validity of MAVLink message sequences
Stated as the basis for the minimal DSL in the abstract
domain assumption Reflective decision procedures in Meta-F* correctly confirm structural well-formedness of the session-type specifications
Invoked to justify that confirmed specifications can be compiled without further manual proof

pith-pipeline@v0.9.0 · 5527 in / 1634 out tokens · 42585 ms · 2026-05-13T16:48:22.105217+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

[1]

1007/s10703-017-0275-x 20 A

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems | Formal Methods in System Design,https://link.springer.com/article/10. 1007/s10703-017-0275-x 20 A. Amorim et al

work page
[2]

In: 2019 15th International Wireless Communications & Mobile Computing Confer- ence (IWCMC)

Allouch, A., Cheikhrouhou, O., Koubâa, A., Khalgui, M., Abbes, T.: MAVSec: Securing the MAVLink protocol for ardupilot/PX4 unmanned aerial systems. In: 2019 15th International Wireless Communications & Mobile Computing Confer- ence (IWCMC). pp. 621–628. IEEE (2019)

work page 2019
[3]

In: Dutle, A., Humphrey, L., Titolo, L

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)

work page 2025
[4]

In: 2025 International Conference on Unmanned Aircraft Systems (ICUAS)

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: //ieeexplore.ieee.org/abstract/document/11007915

work page arXiv 2025
[5]

Science of Com- puter Programming205, 102610 (May 2021),https://www.sciencedirect.com/ science/article/pii/S0167642321000034

Ancona, D., Franceschini, L., Ferrando, A., Mascardi, V.: RML: Theory and practice of a domain specific language for runtime verification. Science of Com- puter Programming205, 102610 (May 2021),https://www.sciencedirect.com/ science/article/pii/S0167642321000034

work page 2021
[6]

ArduPilot: MissionPlanner Issue #1248: Add support for new flight modes (2024), https://github.com/ArduPilot/MissionPlanner/issues/1248

work page 2024
[7]

In: 2020 IEEE 92nd Vehicular Technology Conference (VTC2020-Fall)

CHAARI,L.,CHAHBANI,S.,REZGUI,J.:MAV-DTLStowardSecurityEnhance- ment of the UAV-GCS Communication. In: 2020 IEEE 92nd Vehicular Technology Conference (VTC2020-Fall). pp. 1–5 (Nov 2020),https://ieeexplore.ieee.org/ document/9348584, iSSN: 2577-2465

work page arXiv 2020
[8]

In: 2024 4th International Con- ference on Digital Futures and Transformative Technologies (ICoDT2)

Hamza, M.A., Mohsin, M., Khalil, M., Kazmi, S.M.K.A.: MAVLink Protocol: A Survey of Security Threats and Countermeasures. In: 2024 4th International Con- ference on Digital Futures and Transformative Technologies (ICoDT2). pp. 1–8. IEEE (2024)

work page 2024
[9]

Applied Soft Computing83, 105650 (Oct 2019),https: //www.sciencedirect.com/science/article/pii/S1568494619304302

Khan, S., Liew, C.F., Yairi, T., McWilliam, R.: Unsupervised anomaly detection in unmanned aerial vehicles. Applied Soft Computing83, 105650 (Oct 2019),https: //www.sciencedirect.com/science/article/pii/S1568494619304302

work page 2019
[10]

In: NDSS (2021)

Kim, H., Ozmen, M.O., Bianchi, A., Celik, Z.B., Xu, D.: PGFUZZ: Policy-Guided Fuzzing for Robotic Vehicles. In: NDSS (2021)

work page 2021
[11]

In: 28th USENIX Security Symposium (USENIX Security 19)

Kim, T., Kim, C.H., Rhee, J., Fei, F., Tu, Z., Walkup, G., Zhang, X., Deng, X., Xu, D.: RVFuzzer: Finding Input Validation Bugs in Robotic Vehicles through Control- Guided Testing. In: 28th USENIX Security Symposium (USENIX Security 19). pp. 425–442. USENIX Association, Santa Clara, CA (Aug 2019),https://www. usenix.org/conference/usenixsecurity19/present...

work page 2019
[12]

IEEE Access6, 43203–43212 (2018),https://ieeexplore.ieee.org/document/8425627

Kwon, Y.M., Yu, J., Cho, B.M., Eun, Y., Park, K.J.: Empirical Analysis of MAVLink Protocol Vulnerability for Attacking Unmanned Aerial Vehicles. IEEE Access6, 43203–43212 (2018),https://ieeexplore.ieee.org/document/8425627

work page arXiv 2018
[13]

In: Piskac, R., Rakamarić, Z

Li, E., Stutz, F., Wies, T., Zufferey, D.: Sprout: A Verifier for Symbolic Multiparty Protocols. In: Piskac, R., Rakamarić, Z. (eds.) Computer Aided Verification. pp. 304–317. Springer Nature Switzerland, Cham (2025)

work page 2025
[14]

In: Towards Autonomous Robotic Systems: 26th Annual Conference, TAROS 2025, York, UK, August 20–22, 2025, Proceedings

Luckcuck, M., Ferrando, A., Faruq, F.: Varanus: Runtime Verification for CSP. In: Towards Autonomous Robotic Systems: 26th Annual Conference, TAROS 2025, York, UK, August 20–22, 2025, Proceedings. pp. 259–272. Springer-Verlag, Berlin, Heidelberg (Aug 2025),https://doi.org/10.1007/978-3-032-01486-3_21

work page doi:10.1007/978-3-032-01486-3_21 2025
[15]

In: Eu- ropean Symposium on Programming

Martínez, G., Ahman, D., Dumitrescu, V., Giannarakis, N., Hawblitzel, C., Hriţcu, C., Narasimhamurthy, M., Paraskevopoulou, Z., Pit-Claudel, C., Protzenko, J., others: Meta-F: Proof Automation with SMT, Tactics, and Metaprograms. In: Eu- ropean Symposium on Programming. pp. 30–59. Springer International Publishing Cham (2019) From High-Level Types to Low-...

work page 2019
[16]

MAVLink Development Team: MAVLink: Micro Air Vehicle Communication Pro- tocol (2024),https://mavlink.io/

work page 2024
[17]

In: Sharygina, N., Veith, H

Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Sym- bolic Analysis of Security Protocols. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. pp. 696–701. Springer, Berlin, Heidelberg (2013)

work page 2013
[18]

Proceedings of the ACM on Programming Languages1(ICFP), 1–29 (2017)

Protzenko, J., Zinzindohoué, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-Béguelin, S., Delignat-Lavaud, A., Hriţcu, C., Bhargavan, K., Fournet, C., others: Verified low-level programming embedded in F. Proceedings of the ACM on Programming Languages1(ICFP), 1–29 (2017)

work page 2017
[19]

Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., others: Dependent types andmulti-monadiceffectsinF.In:Proceedingsofthe43rdannualACMSIGPLAN- SIGACTSymposium on Principles of Programming Languages. pp. 256–270 (2016)

work page 2016
[20]

In: 2025 Annual Computer Se- curity Applications Conference Workshops (ACSAC Workshops)

Taylor, M., Amorim, A., Joneckis, L.: Securing Modbus-Based Industrial Control Systems with Refined Multiparty Session Types. In: 2025 Annual Computer Se- curity Applications Conference Workshops (ACSAC Workshops). pp. 99–109 (Dec 2025),https://ieeexplore.ieee.org/abstract/document/11418027

work page arXiv 2025
[21]

In: 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

Taylor, M., Chen, H., Qin, F., Stewart, C.: Avis: In-situ model checking for un- manned aerial vehicles. In: 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). pp. 471–483. IEEE (2021)

work page 2021
[22]

In: Aldrich, J., Sal- vaneschi, G

Vassor, M., Yoshida, N.: Refinements for Multiparty Message-Passing Proto- cols: Specification-Agnostic Theory and Implementation. In: Aldrich, J., Sal- vaneschi, G. (eds.) 38th European Conference on Object-Oriented Program- ming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 313, pp. 41:1–41:29. Schloss Dagstuhl – Leibniz-...

work page doi:10.4230/lipics.ecoop.2024.41 2024
[23]

In: MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM)

Wray,T.,Wang,Y.:PAVE-MAVLink:FormalVerificationofMAVLink2forSecure UAV Communications. In: MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM). pp. 1389–1395 (Oct 2025),https://ieeexplore.ieee. org/document/11310743

work page arXiv 2025
[24]

In: Trustworthy Global Computing: 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers 8

Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble protocol language. In: Trustworthy Global Computing: 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers 8. pp. 22–41. Springer (2014)

work page 2013
[25]

Zhou, F.: Refining Multiparty Session Types. Ph.D. thesis, Imperial College Lon- don, London, UK (2024),https://doi.org/10.25560/110416

work page doi:10.25560/110416 2024
[26]

Proceedings of the ACM on Programming Lan- guages4(OOPSLA), 1–30 (2020)

Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refine- ments for multiparty protocols. Proceedings of the ACM on Programming Lan- guages4(OOPSLA), 1–30 (2020)

work page 2020

[1] [1]

1007/s10703-017-0275-x 20 A

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems | Formal Methods in System Design,https://link.springer.com/article/10. 1007/s10703-017-0275-x 20 A. Amorim et al

work page

[2] [2]

In: 2019 15th International Wireless Communications & Mobile Computing Confer- ence (IWCMC)

Allouch, A., Cheikhrouhou, O., Koubâa, A., Khalgui, M., Abbes, T.: MAVSec: Securing the MAVLink protocol for ardupilot/PX4 unmanned aerial systems. In: 2019 15th International Wireless Communications & Mobile Computing Confer- ence (IWCMC). pp. 621–628. IEEE (2019)

work page 2019

[3] [3]

In: Dutle, A., Humphrey, L., Titolo, L

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)

work page 2025

[4] [4]

In: 2025 International Conference on Unmanned Aircraft Systems (ICUAS)

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: //ieeexplore.ieee.org/abstract/document/11007915

work page arXiv 2025

[5] [5]

Science of Com- puter Programming205, 102610 (May 2021),https://www.sciencedirect.com/ science/article/pii/S0167642321000034

Ancona, D., Franceschini, L., Ferrando, A., Mascardi, V.: RML: Theory and practice of a domain specific language for runtime verification. Science of Com- puter Programming205, 102610 (May 2021),https://www.sciencedirect.com/ science/article/pii/S0167642321000034

work page 2021

[6] [6]

ArduPilot: MissionPlanner Issue #1248: Add support for new flight modes (2024), https://github.com/ArduPilot/MissionPlanner/issues/1248

work page 2024

[7] [7]

In: 2020 IEEE 92nd Vehicular Technology Conference (VTC2020-Fall)

CHAARI,L.,CHAHBANI,S.,REZGUI,J.:MAV-DTLStowardSecurityEnhance- ment of the UAV-GCS Communication. In: 2020 IEEE 92nd Vehicular Technology Conference (VTC2020-Fall). pp. 1–5 (Nov 2020),https://ieeexplore.ieee.org/ document/9348584, iSSN: 2577-2465

work page arXiv 2020

[8] [8]

In: 2024 4th International Con- ference on Digital Futures and Transformative Technologies (ICoDT2)

Hamza, M.A., Mohsin, M., Khalil, M., Kazmi, S.M.K.A.: MAVLink Protocol: A Survey of Security Threats and Countermeasures. In: 2024 4th International Con- ference on Digital Futures and Transformative Technologies (ICoDT2). pp. 1–8. IEEE (2024)

work page 2024

[9] [9]

Applied Soft Computing83, 105650 (Oct 2019),https: //www.sciencedirect.com/science/article/pii/S1568494619304302

Khan, S., Liew, C.F., Yairi, T., McWilliam, R.: Unsupervised anomaly detection in unmanned aerial vehicles. Applied Soft Computing83, 105650 (Oct 2019),https: //www.sciencedirect.com/science/article/pii/S1568494619304302

work page 2019

[10] [10]

In: NDSS (2021)

Kim, H., Ozmen, M.O., Bianchi, A., Celik, Z.B., Xu, D.: PGFUZZ: Policy-Guided Fuzzing for Robotic Vehicles. In: NDSS (2021)

work page 2021

[11] [11]

In: 28th USENIX Security Symposium (USENIX Security 19)

Kim, T., Kim, C.H., Rhee, J., Fei, F., Tu, Z., Walkup, G., Zhang, X., Deng, X., Xu, D.: RVFuzzer: Finding Input Validation Bugs in Robotic Vehicles through Control- Guided Testing. In: 28th USENIX Security Symposium (USENIX Security 19). pp. 425–442. USENIX Association, Santa Clara, CA (Aug 2019),https://www. usenix.org/conference/usenixsecurity19/present...

work page 2019

[12] [12]

IEEE Access6, 43203–43212 (2018),https://ieeexplore.ieee.org/document/8425627

Kwon, Y.M., Yu, J., Cho, B.M., Eun, Y., Park, K.J.: Empirical Analysis of MAVLink Protocol Vulnerability for Attacking Unmanned Aerial Vehicles. IEEE Access6, 43203–43212 (2018),https://ieeexplore.ieee.org/document/8425627

work page arXiv 2018

[13] [13]

In: Piskac, R., Rakamarić, Z

Li, E., Stutz, F., Wies, T., Zufferey, D.: Sprout: A Verifier for Symbolic Multiparty Protocols. In: Piskac, R., Rakamarić, Z. (eds.) Computer Aided Verification. pp. 304–317. Springer Nature Switzerland, Cham (2025)

work page 2025

[14] [14]

In: Towards Autonomous Robotic Systems: 26th Annual Conference, TAROS 2025, York, UK, August 20–22, 2025, Proceedings

Luckcuck, M., Ferrando, A., Faruq, F.: Varanus: Runtime Verification for CSP. In: Towards Autonomous Robotic Systems: 26th Annual Conference, TAROS 2025, York, UK, August 20–22, 2025, Proceedings. pp. 259–272. Springer-Verlag, Berlin, Heidelberg (Aug 2025),https://doi.org/10.1007/978-3-032-01486-3_21

work page doi:10.1007/978-3-032-01486-3_21 2025

[15] [15]

In: Eu- ropean Symposium on Programming

Martínez, G., Ahman, D., Dumitrescu, V., Giannarakis, N., Hawblitzel, C., Hriţcu, C., Narasimhamurthy, M., Paraskevopoulou, Z., Pit-Claudel, C., Protzenko, J., others: Meta-F: Proof Automation with SMT, Tactics, and Metaprograms. In: Eu- ropean Symposium on Programming. pp. 30–59. Springer International Publishing Cham (2019) From High-Level Types to Low-...

work page 2019

[16] [16]

MAVLink Development Team: MAVLink: Micro Air Vehicle Communication Pro- tocol (2024),https://mavlink.io/

work page 2024

[17] [17]

In: Sharygina, N., Veith, H

Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Sym- bolic Analysis of Security Protocols. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. pp. 696–701. Springer, Berlin, Heidelberg (2013)

work page 2013

[18] [18]

Proceedings of the ACM on Programming Languages1(ICFP), 1–29 (2017)

Protzenko, J., Zinzindohoué, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-Béguelin, S., Delignat-Lavaud, A., Hriţcu, C., Bhargavan, K., Fournet, C., others: Verified low-level programming embedded in F. Proceedings of the ACM on Programming Languages1(ICFP), 1–29 (2017)

work page 2017

[19] [19]

Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., others: Dependent types andmulti-monadiceffectsinF.In:Proceedingsofthe43rdannualACMSIGPLAN- SIGACTSymposium on Principles of Programming Languages. pp. 256–270 (2016)

work page 2016

[20] [20]

In: 2025 Annual Computer Se- curity Applications Conference Workshops (ACSAC Workshops)

Taylor, M., Amorim, A., Joneckis, L.: Securing Modbus-Based Industrial Control Systems with Refined Multiparty Session Types. In: 2025 Annual Computer Se- curity Applications Conference Workshops (ACSAC Workshops). pp. 99–109 (Dec 2025),https://ieeexplore.ieee.org/abstract/document/11418027

work page arXiv 2025

[21] [21]

In: 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

Taylor, M., Chen, H., Qin, F., Stewart, C.: Avis: In-situ model checking for un- manned aerial vehicles. In: 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). pp. 471–483. IEEE (2021)

work page 2021

[22] [22]

In: Aldrich, J., Sal- vaneschi, G

Vassor, M., Yoshida, N.: Refinements for Multiparty Message-Passing Proto- cols: Specification-Agnostic Theory and Implementation. In: Aldrich, J., Sal- vaneschi, G. (eds.) 38th European Conference on Object-Oriented Program- ming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 313, pp. 41:1–41:29. Schloss Dagstuhl – Leibniz-...

work page doi:10.4230/lipics.ecoop.2024.41 2024

[23] [23]

In: MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM)

Wray,T.,Wang,Y.:PAVE-MAVLink:FormalVerificationofMAVLink2forSecure UAV Communications. In: MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM). pp. 1389–1395 (Oct 2025),https://ieeexplore.ieee. org/document/11310743

work page arXiv 2025

[24] [24]

In: Trustworthy Global Computing: 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers 8

Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble protocol language. In: Trustworthy Global Computing: 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers 8. pp. 22–41. Springer (2014)

work page 2013

[25] [25]

Zhou, F.: Refining Multiparty Session Types. Ph.D. thesis, Imperial College Lon- don, London, UK (2024),https://doi.org/10.25560/110416

work page doi:10.25560/110416 2024

[26] [26]

Proceedings of the ACM on Programming Lan- guages4(OOPSLA), 1–30 (2020)

Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refine- ments for multiparty protocols. Proceedings of the ACM on Programming Lan- guages4(OOPSLA), 1–30 (2020)

work page 2020