Papers
Published
-
From High-Level Types to Low-Level Monitors, Synthesizing Verified Runtime Checkers for MAVLink
Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis NFM 2026 · Springer -
Enforcing MAVLink Safety & Security Properties via Refined Multiparty Session Types
Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis NFM 2025 · Springer -
UAV Resilience Against Stealthy Attacks
Max Taylor, Arthur Amorim ICUAS 2025 · IEEE -
Securing Modbus-Based Industrial Control Systems with Refined Multiparty Session Types
Max Taylor, Arthur Amorim ICSS 2025 · IEEE -
Enhancing Cyber-Physical System Dependability via Synthesis: Challenges and Future Directions
Max Taylor, Arthur Amorim DSN-W 2025 · IEEE -
Towards Provable Security in Industrial Control Systems via Dynamic Protocol Attestation
Arthur Amorim et al. ICSS 2024
CV
Arthur Amorim
Arthur.Amorim@ucf.edu GitHub LinkedIn Google Scholar
Orlando, FL · U.S. Citizen · Eligible for DoD Secret Clearance
Summary
Ph.D. intern who defended a dissertation in July 2026, with four years of applied work at Idaho National Laboratory. I build machine-checked security infrastructure for embedded systems and lead development of SPECTRE, a framework for verified cyber-physical protocols. My work spans protocol formalization, proof mechanization in F*, C synthesis for legacy retrofit, and physical testbed validation. I have accepted a Research Scientist, System Security Researcher position at MIT Lincoln Laboratory.
Education
Research Experience
- Built SPECTRE (~9,000 lines of F*), a formally verified safety framework for cyber-physical protocols. Its implemented deployment work includes Platum C finite state machine monitors for legacy retrofit and Facet OCaml distributed protocol enforcement from projected local protocol graphs.
- Designed and mechanized Facet: the first fully mechanized RMPST metatheory in F*, proving subject reduction, deadlock freedom, progress, and projectability via computational reflection. Certified extraction ensures the proved object is the deployed object.
- Built Platum: a direct AST-to-C synthesis pipeline generating allocation-free, O(1)-memory FSM monitors deployable on ARM microcontrollers; achieved 4× latency reduction over prior work (~13.3 µs/message).
- Composed monitors with seL4 microkernel isolation to defend against adversaries who have simultaneously compromised the OS-level network stack and ground control station.
- Validated on MAVLink (ArduPilot, PX4) and Modbus: formalized >8,000 lines of MAVLink in F*; demonstrated 100% detection of domain-specific behavioral attacks on a physical chemical mixing testbed at <10% latency overhead.
- Held a joint appointment with INL addressing evolving cybersecurity threats in manufacturing systems.
- Focused on making DATUM practical and deployable in widely used industrial protocols, including Modbus.
- Collaborated with industry partners to retrofit legacy manufacturing systems with provable security mechanisms.
- Performed modeling and translation from functional specifications to executable low-level code.
- Bridged theoretical formal methods research with practical implementation requirements for critical infrastructure applications.
Technical Skills
- Verification & Proof
- F* / Meta-F*, Z3 (SMT), nuXmv (model checking)
- Systems & Protocols
- seL4 microkernel, MAVLink, Modbus, ARM embedded, ArduPilot/PX4
- Languages
- F*, OCaml, C/C++, Python, Rust, LaTeX
- Security Domains
- Threat modeling, embedded systems security, ICS/SCADA security, runtime enforcement, protocol verification