Showing 1–4 of 4 results for author: Kann, T

Covert Communication over Physically-Degraded Alarm Two-Way Channels

Authors: Tuna Erdoğan, Tyler Kann, Aria Nosratinia, Matthieu Bloch

Abstract: We study covert communications over binary-input discrete memoryless alarm two-way channels, in which two users interact through a two-way channel and attempt to hide the presence of their communication from an eavesdropping receiver. The alarm two-way channel is one in which simultaneous transmissions by both users trigger an alarm at the eavesdropper, which captures the challenges and opportunit… ▽ More We study covert communications over binary-input discrete memoryless alarm two-way channels, in which two users interact through a two-way channel and attempt to hide the presence of their communication from an eavesdropping receiver. The alarm two-way channel is one in which simultaneous transmissions by both users trigger an alarm at the eavesdropper, which captures the challenges and opportunities of cooperation beyond interference management. In particular, by characterizing the covert capacity region of two-way channels when using public time sharing, we show how cooperation strictly improves achievable covert communication throughputs. While our analysis falls short of characterizing the two-way covert capacity region for all two-way channels, we provide general achievable and converse bounds that illuminate the cooperation mechanisms that benefit covertness and are tight for a physically-degraded alarm two-way channels. Because of the unique nature of covert communications, our analysis also shows that the coordination required to avoid triggering alarms comes asymptotically "for free". The key technical challenge that we address is how to appropriately design auxiliary random variables in a multi-user covert communication setting subject to the square root law. △ Less

Submitted 19 June, 2025; originally announced June 2025.

UAV Resilience Against Stealthy Attacks

Authors: Arthur Amorim, Max Taylor, Trevor Kann, Gary T. Leavens, William L. Harrison, Lance Joneckis

Abstract: 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 done to prevent an attacker who has either compromised a ground control station or parts of a UAV's software from sabotaging the vehicle, but not both. We present an architecture running a UAV software stack with runtime… ▽ More 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 done to prevent an attacker who has either compromised a ground control station or parts of a UAV's software from sabotaging the vehicle, but not both. We present an architecture running a UAV software stack with runtime monitoring and seL4-based software isolation that prevents attackers from both exploiting software bugs and stealthy attacks. Our architecture retrofits legacy UAVs and secures the popular MAVLink protocol, making wide adoption possible. △ Less

Submitted 14 April, 2025; v1 submitted 21 March, 2025; originally announced March 2025.

Comments: To be featured in ICUAS'25 proceedings

Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types

Authors: Arthur Amorim, Max Taylor, Trevor Kann, William L. Harrison, Gary T. Leavens, Lance Joneckis

Abstract: 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 characterize, because message interfaces in standard languages specify each individual message separately but do not specify safe sequences of messages. We present initial results from ongoing work applying refined multiparty s… ▽ More 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 characterize, because message interfaces in standard languages specify each individual message separately but do not specify safe sequences of messages. We present initial results from ongoing work applying refined multiparty session types as a mechanism for expressing and enforcing proper message usage to exclude unsafe sequences. We illustrate our approach by using refined multiparty session types to mitigate safety and security issues in the MAVLink protocol commonly used in UAVs. △ Less

Submitted 14 March, 2025; v1 submitted 30 January, 2025; originally announced January 2025.

Comments: To be featured in proceedings of The 17th NASA Formal Methods Symposium

Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation

Authors: Arthur Amorim, Trevor Kann, Max Taylor, Lance Joneckis

Abstract: Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individually, each action seems innocuous. But taken together, they cause the system to enter an unsafe state. These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catast… ▽ More Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individually, each action seems innocuous. But taken together, they cause the system to enter an unsafe state. These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catastrophes. This paper introduces a methodology that restricts actions using protocols. These protocols only allow safe actions to execute. Protocols are written in a domain specific language we have embedded in an interactive theorem prover (ITP). The ITP enables formal, machine-checked proofs to ensure protocols maintain safety properties. We use dynamic attestation to ensure ICSs conform to their protocol even if an adversary compromises a component. Since protocol conformance prevents unsafe actions, the previously mentioned cyber attacks become impossible. We demonstrate the effectiveness of our methodology using an example from the Fischertechnik Industry 4.0 platform. We measure dynamic attestation's impact on latency and throughput. Our approach is a starting point for studying how to combine formal methods and protocol design to thwart attacks intended to cripple ICSs. △ Less

Submitted 18 December, 2024; originally announced December 2024.

Comments: This paper was accepted into the ICSS'24 workshop