Information flow control (IFC) provides confidentiality by enforcing noninterference, which ensures that high-secrecy values cannot affect low-secrecy values. Prior work introduces fine-grained IFC approaches that modify the programming language and use non-standard compilation tools, impose run-time overhead, or report false secrecy leaks—all of which hinder adoption. This paper presents Cocoon, a Rust library for static type-based IFC that uses the unmodified Rust language and compiler. The key insight of Cocoon lies in leveraging Rust’s type system and procedural macros to establish an effect system that enforces noninterference. A performance evaluation shows that using Cocoon increases compile time but has no impact on application performance. To demonstrate Cocoon’s utility, we retrofitted two popular Rust programs, the Spotify TUI client and Mozilla’s Servo browser engine, to use Cocoon to enforce limited confidentiality policies

Unit type errors, where values with physical unit types (e.g., meters, hours) are used incorrectly in a computation, are common in today’s unmanned aerial system (UAS) firmware. Recent studies show that unit type errors represent over 10% of bugs in UAS firmware. Moreover, the consequences of unit type errors are severe. Over 30% of unit type errors cause UAS crashes. This paper proposes SA4U: a practical system for detecting unit type errors in real-world UAS firmware. SA4U requires no modifications to firmware or developer annotations. It deduces the unit types of program variables by analyzing simulation traces and protocol definitions. SA4U uses the deduced unit types to identify when unit type errors occur. SA4U is effective: it identified 14 previously undetected bugs in two popular open-source firmware (ArduPilot & PX4.)

Control firmware in unmanned aerial vehicles (UAVs) uses sensors to model and manage flight operations, from takeoff to landing to flying between waypoints. However, sensors can fail at any time during a flight. If control firmware mishandles sensor failures, UAVs can crash, fly away, or suffer other unsafe conditions. In-situ model checking finds sensor failures that could lead to unsafe conditions by systematically failing sensors. However, the type of sensor failure and its timing within a flight affect its manifestation, creating a large search space. We propose Avis, an in-situ model checker to quickly uncover UAV sensor failures that lead to unsafe conditions. Avis exploits operating modes, i.e., a label that maps software execution to corresponding flight operations. Widely used control firmware already support operating modes. Avis injects sensor failures as the control firmware transitions between modes - a key execution point where mishandled software exceptions can trigger unsafe conditions. We implemented Avis and applied it to ArduPilot and PX4. Avis found unsafe conditions 2.4X faster than Bayesian Fault Injection, the leading, state-of-theart approach. Within the current code base of ArduPilot and PX4, Avis discovered 10 previously unknown software bugs that lead to unsafe conditions. Additionally, we reinserted 5 known bugs that caused serious, unsafe conditions and Avis correctly reported all of them.