Directed Symbolic Execution

In this project, we targeted embedded systems. We looked at how program analysis can be used to find sensor spoofing vulnerabilities in embedded system firmware. A sensor spoofing attack is a type of of attack in which an adversary modifies the physical environment in a certain way so as to force an embedded system into unwanted or unintended behaviors. For example, an attacker controlling speech recognition interfaces with nonsensical noise which is erroneously interpreted as commands by the firmware algorithm.

In this project, we targeted systems powered by MSP430 family of microcontrollers from Texas instruments that are used by a large number of embedded devices; and we developed a new symbolic execution framework, called DrE, that can be used to find such signal spoofing vulnerabilities in embedded code firmware.

Sensor spoofing

The explosion in the popularity of embedded systems is fueled in large part by their ability to sense, interpret, and react to physical environments. For example, gesture recognition systems measure signals and interpret them as user commands, cameras that sense motion or light help autonomous systems navigate, and temperature sensors inform household HVAC systems. Software controlling embedded systems is often designed assuming a benign environment, for example, a device owner interacting with his own device. In real-world deployments, however, it is necessary to consider sensor spoofing threats. An attacker with direct or indirect access to the physical environment can emit physical signals that maliciously force unwanted or unintended behaviors in the victim software and, consequently, in the system controlled by this software.

Some of the examples include disrupting the flight of autonomous drones using sound generated by off-the-shelf computer speakers or laser pointers, injecting bogus signals into medical devices, controlling speech recognition interfaces with nonsensical noise, and many others. These attacks are usually developed by manual reverse engineering and experimentation.

Synthesizing sensor spoofing attacks.

In this project, we initiated research on software analysis tools that can help discover and exploit sensor spoofing vulnerabilities in embedded software. We focused on a popular class of embedded systems: lightweight microcontrollers attached to one or more sensor components. The sensors convert physical readings (temperature, light, sound, electromagnetic signals, etc.) into digital values that are read by the microcontroller’s firmware. Such systems are ubiquitous in so-called Internet-of-Things (IoT) applications, autonomous vehicles, and elsewhere. In sensor spoofing attack, the adversary’s goal is to infer which digital inputs to the firmware will force the behavior the adversary wants.

Symbolic execution for embedded systems

We wanted to build a tool that can automatically discover sequences of digital sensor readings that drive the firmware to an adversarially chosen state. This includes possible sequences that the firmware designers did not expect. This is a problem well-suited for symbolic execution, given its ability to automatically generate inputs that drive the program into particular execution paths. As a result, we developed DrE (Directed Execution), a symbolic execution tool specifically engineered to analyze embedded firmware code with respect to signal input spoofing.

Directed

To handle the challenges of analyzing embedded firmware, DrE uses a modular approach that takes advantage of both directed and compositional symbolic execution. Instead of attempting to explore all code paths, directed symbolic execution starts with a target, i.e., a particular point of interest in the program. In our context, these points are sections of the firmware code corresponding to the control actions that the attacker wants to firmware to take. The output of a successful directed symbolic execution is a path, defined as a set of constraints on inputs (i.e., sensor readings) that, if satisfied, will drive the program to the designated point.

Compositional

To mitigate path explosion, we devised a modular strategy to efficiently find paths to program points of interest. It uses a combination of call graph and control flow graph analysis with compositional symbolic execution. DrE starts by finding possible call chains from the program’s entry point to the function containing the target line. It then symbolically executes the function containing the target point and proceeds through a call chain backwards. Each function along the way is symbolically executed independently. To generate inter-procedural path constraints, DrE then stitches together the execution paths of individual functions. To do this, DrE collects, rewrites, and propagates the relevant constraints and performs a forward pass to check them. For efficiency, DrE employs several additional heuristics. DrE biases state selection towards shorter paths leading to the target program point and employs a state-pruning strategy to break out of infinite wait loops.