4 papers
From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
Arthur Amorim, Paul Gazzillo, Max Taylor +1
Standard communication protocols for Unmanned Aerial Vehicles (UAVs), such as MAVLink, lack the capability to enforce the contextual validity of message sequences. Autopilots there…
UAV Resilience Against Stealthy Attacks
Arthur Amorim, Max Taylor, Trevor Kann +3
Unmanned aerial vehicles (UAVs) depend on untrusted software components to automate dangerous or critical missions, making them a desirable target for attacks. Some work has been d…
Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
Arthur Amorim, Max Taylor, Trevor Kann +3
A compromised system component can issue message sequences that are legal while also leading the overall system into unsafe states. Such stealthy attacks are challenging to charact…
Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation
Arthur Amorim, Trevor Kann, Max Taylor +1
Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individu…