Unmanned Aerial Vehicles as a service (UAVaaS) has increased the field deployment of Robotic Aerial Vehicles (RAVs) for different services such as transportation and terrain exploration. These RAVs are controlled by firmware, which is often closed-source, developed by vendors, and flashed into the ROM. While these binary blobs enable off-the-shelf management of RAVs, end users (individuals or organizations) have no idea if the control firmware is designed and implemented correctly, and can only rely on firmware updates from vendors when any vulnerability is discovered. This paper proposes DisPatch, the first reverse engineering and patching framework for understanding and improving controller design and implementation within RAV firmware. DisPatch first decompiles binary instructions and recovers controller functions and core controller variables by combining control theory with program analysis using symbolic execution and data flow analysis. End users can then write a patch in a domain-specific language (DSL), which will be translated and injected into the binary firmware by DisPatch automatically. We have applied DisPatch to two instances of commodity firmware from3DR IRIS+ and MantisQ RAVs and demonstrated 100% and 80.7% accuracy respectively in the controller decompilation. We have also shown the ability to prevent severe controller performance degradation by patching two real-world bugs with in the firmware and without breaking other functionality. Finally, we show that DisPatch introduces less than 0.53% of space overhead and 1.48% of runtime overhead without violating the soft real-time deadlines. DisPatch provides the first step towards an RAV binary firmware reverse engineering and patching system to customize controller design and implementation.

Rapid prototyping makes additive manufacturing (or 3D printing) useful in critical application domains such as aerospace, automotive, and medical. The rapid expansion of these applications should prompt the examination of the underlying security of 3D printed objects. In this paper, we present Mystique, a novel class of stealthy attacks on printed objects that leverage the fourth dimension of emerging 4D printing technology to introduce embedded logic bombs through manufacturing process manipulation. Mystique enables visually benign objects to behave maliciously upon the activation of the logic bomb during operation. It leverages the manufacturing process to embed a physical logic bomb that can be triggered with specific stimuli to change the physical and mechanical properties of the printed objects. These changes in properties can potentially cause catastrophic operational failures when the objects are used in critical applications such as drones, prosthesis, or medical applications.

STereoLithography (STL) files describe the geometry of objects to be printed in additive manufacturing. Previous studies have shown that the STL files that describe functional objects can be attacked such that the objects appear normal during inspection, but fail during operation. Such attacks lead to damage to systems that use the objects and possibly loss of life. The detection of any defects caused due to the attacks nowadays is limited to the quality control process after the objects are manufactured.We present a Trusted Integrity Verifier (TIV) to detect such attacks on 3D printed objects in the early stage of the manufacturing process. These type of new attacks cannot be detected by traditional software security mechanisms since they only focus on the printers and do not consider the inputs (STL design files) to the printer. Early detection of attacks prevents from printing malicious objects resulting in saving time, resources and manufacturing efforts. TIV detects malicious STL files using multidisciplinary approaches unlike the traditional integrity verification techniques. TIV develops a void detection module based on computer vision techniques to identify the internal defects such as voids. Some of these features could be from the design and some could be due to the attack. To differentiate the malicious features from the design features, TIV develops safety verification module based on a numerical method. TIV's safety verification module is used to differentiate the malicious features from the design features by calculating the load bearing mechanical stress on the objects. These mechanical stresses are compared to the safety operational conditions to determine if the printed object will break or fail during its normal operation.To illustrate TIV's generality and scalability, we conducted a large-scale analysis on 16,000 real-world 3D print STL files. TIV verified the STL files successfully as either safe or malicious with high accuracy of 92% for object classification and 96.5% for void detection.

Recent major attacks against unmanned aerial vehicles (UAV) and their controller software necessitate domain-specific cyber-physical security protection. Existing offline formal methods for (untrusted) controller code verification usually face state-explosion. On the other hand, runtime monitors for cyber-physical UAVs often lead to too-late notifications about unsafe states that makes timely safe operation recovery impossible.

Automated vulnerability assessment and exploit generation for computing systems have been explored for decades. However, these approaches are incomplete in assessing industrial control systems, where networks of computing devices and physical processes interact for safety-critical missions. We present an attack synthesis algorithm against such cyber-physical electricity grids. The algorithm explores both discrete network configurations and continuous dynamics of the plant's embedded control system to search for attack strategies that evade detection with conventional monitors. The algorithm enabling this exploration is rooted in recent developments in the hybrid system verification research: it effectively approximates the behavior of the system for a set of possible attacks by computing sensitivity of the system's response to variations in the attack parameters. For parts of the attack space, the proposed algorithm can infer whether or not there exists a feasible attack that avoids triggering protection measures such as relays and steady-state monitors. The algorithm can take into account constraints on the attack space such as the power system topology and the set of controllers across the plant that can be compromised without detection. With a proof-of-concept prototype, we demonstrate the synthesis of transient attacks in several typical electricity grids and analyze the robustness of the synthesized attacks to perturbations in the network parameters.

Trustworthy operation of industrial control systems depends on secure and real-time code execution on the embedded programmable logic controllers (PLCs). The controllers monitor and control the critical infrastructures, such as electric power grids and healthcare platforms, and continuously report back the system status to human operators. We present Zeus, a contactless embedded controller security monitor to ensure its execution control flow integrity. Zeus leverages the electromagnetic emission by the PLC circuitry during the execution of the controller programs. Zeus's contactless execution tracking enables non-intrusive monitoring of security-critical controllers with tight real-time constraints. Those devices often cannot tolerate the cost and performance overhead that comes with additional traditional hardware or software monitoring modules. Furthermore, Zeus provides an air-gap between the monitor (trusted computing base) and the target (potentially compromised) PLC. This eliminates the possibility of the monitor infection by the same attack vectors.