Discovering Blind-Trust Vulnerabilities in PLC Binaries via State Machine Recovery

Discovering Blind-Trust Vulnerabilities in PLC Binaries via State Machine Recovery

Speakers: Fangzhou Dong

Conference: NDSS Symposium

YouTube: https://www.youtube.com/watch?v=u4GdgdjKYgM

Overview

Programmable Logic Controllers (PLCs) are the industrial computers running critical infrastructure -- traffic lights, warehouse lifters, conveyor systems, water treatment plants. This talk introduces a new class of safety vulnerability called Blind Trust Vulnerabilities (BTVs), which are logic bugs caused by PLC programmers placing blind trust in assumptions about system inputs without sufficient sanitization or validation. When a system receives an input outside these assumptions -- whether from faulty sensors or adversarial manipulation -- it can cause catastrophic safety failures.

The researchers present Taviran, a static analysis framework that automatically discovers BTVs by recovering finite state machines (FSMs) from PLC binaries (without source code access) and applying model checking against safety policies. Evaluated across 22 PLC binaries from 9 categories compiled from 4 toolchains and 5 architectures, Taviran found 23 policy violations with 17 confirmed BTVs grouped into 6 root cause categories. The tool also discovered BTVs in real-world robotic vehicle binaries including ArduCopter and a rover system. All artifacts are open-sourced on GitHub.

Background

▶ Watch: Introduction to PLCs and the blind trust vulnerability concept (0:00)

PLCs are embedded industrial computers used to automate physical processes in critical infrastructure. They execute programs in a cyclic scan pattern, repeatedly reading inputs from sensors, executing control logic, and writing outputs to actuators. The control logic is typically implemented as a state machine, though this structure is compiled away in the resulting binary.

The danger of blind trust in sensor inputs is not theoretical. The talk references the Boeing 737 MAX crashes of 2018-2019, which killed 346 people because the flight control system trusted a single faulty Angle of Attack (AOA) sensor without cross-referencing the redundant sensor. The MCAS system, relying on the faulty data, repeatedly pushed the aircraft's nose down until pilots lost control. If the flight controller had compared readings from both AOA sensors, it would have detected the discrepancy and avoided trusting the faulty data.

Existing approaches to PLC security focus primarily on implementation-level bugs that can be found through traditional testing or formal verification. BTVs are fundamentally different -- they are logic bugs that arise from incomplete handling of the input space, not from coding errors. Direct application of model checking to PLC binaries faces the state explosion problem due to the potentially infinite state space of real programs.

Key Findings

▶ Watch: Challenges: state explosion and infinite state space in PLC analysis (4:00)

• 17 confirmed BTVs discovered across 22 PLC binaries, grouped into 6 root cause categories:

1. Incomplete range handling: Programs that don't handle the full range of possible input values (e.g., a warehouse lifter that checks if current_rack == assigned_rack but doesn't handle current_rack > assigned_rack, causing indefinite upward movement)
2. Incorrect input check: Validation logic that checks the wrong condition
3. Unhandled input combination: Failure to account for specific combinations of multiple sensor inputs
4. Unchecked input acceptance: Accepting inputs without any validation
5. Missing input handling: States that don't process certain inputs at all
6. Wrong action: Correct state transition but incorrect output action

• ArduCopter BTV: The copter's flip mode does not check altitude before executing, allowing a flip at any altitude -- even below the minimum safe altitude, which would cause a ground crash
• Rover BTV: Blindly accepting user commands causes the rover to repeatedly restart its mission, significantly deviating from the specified route
• Cross-architecture coverage: Taviran works across 5 architectures (x86-64, ARM, MIPS, PowerPC, AVR8) and 4 toolchains (OpenPLC, Beremiz, Simulink, Arduino)
• Formal completeness guarantee: The FSM recovery algorithm has a formal proof of completeness, ensuring that if environment models and state variables are correctly identified, the recovered FSM is complete

Technical Deep Dive

▶ Watch: FSM recovery via concolic execution with abstract states (8:00)

Taviran operates as a three-step static analysis framework:

Step 1 - Preprocessing: Given a PLC binary (without source code), Taviran first identifies the scan cycle function that implements the FSM. It then identifies state variables -- the variables used to record and track the program's internal states. The system also takes an environment model specifying input/output variables (e.g., sensor readings as inputs, actuator controls as outputs) and a set of safety policies serving as bug oracles.

Step 2 - FSM Recovery: This is the core technical contribution. The CFG of the scan cycle function looks nothing like a state machine because PLC programs execute cyclically, using boolean flags to track state activations within each scan cycle. Taviran recovers the FSM using two key techniques:

• State deduplication via abstract states: Rather than tracking every concrete state (which would cause state explosion), Taviran derives abstract states by grouping concrete states with equivalent behavior. Starting from an initialized concrete state, it performs concolic execution on the scan cycle function, derives abstract states from the results, and adds new states and transitions to the FSM graph.
• Meaningful input value discovery: Instead of checking every possible input value (infinite for numerical sensors), Taviran extracts constraints on input variables during concolic execution and uses only the meaningful boundary values. For example, if a water level sensor check compares against a threshold, only the values above and below that threshold matter.

The algorithm iterates: execute the scan cycle concretely, extract abstract state, discover new input constraints, add to worklist, repeat until the worklist is empty. Initial concrete state is obtained by running initialization functions identified through heuristics between the binary entry point and the scan cycle function.

Step 3 - BTV Discovery: The recovered FSM is model-checked against provided safety policies (e.g., "when water level is high, pump must be off"). Violations are reported with the input sequence leading to the unsafe state.

Demo / Proof of Concept

▶ Watch: Evaluation: 17 BTVs found across 22 binaries on 5 architectures (10:00)

Taviran was evaluated on a custom dataset of 22 PLC binaries representing 9 categories of industrial control systems (warehouse lifter, launcher board systems, and others), compiled from 4 toolchains across 5 architectures. This dataset has been open-sourced on GitHub since no public dataset of PLC binaries with finite state machines previously existed.

Taviran completed analysis within minutes on all but two very large binaries. The FSM recovery step consumes over 60% of total analysis time, with duration proportional to FSM size (number of iterations) and scan cycle function complexity. Once the FSM is recovered, policy checking is very fast.

The real-world validation on robotic vehicle binaries is particularly compelling. The ArduCopter flip mode BTV -- allowing flips at any altitude including below minimum safe altitude -- represents a genuine safety hazard. The rover mission restart BTV demonstrates how blind trust in user commands can cause significant operational deviation.

The Q&A session addressed several important questions: commercial PLC support (limited by proprietary binary formats without available disassemblers), safety policy definition completeness (acknowledged as a dependency, with potential for NLP or LLM-assisted extraction from manuals), initial state concretization strategy, and the single-sensor-at-a-time threat model assumption.

Defensive Implications

▶ Watch: Q&A: safety policy definition and commercial PLC challenges (16:00)

Taviran has immediate relevance for industrial control system security:

• Binary-level analysis: By working directly with compiled PLC binaries rather than source code, Taviran enables security assessment of third-party PLC programs where source code is unavailable -- a common scenario in industrial supply chains.
• Safety policy enforcement: The framework provides a systematic way to verify that PLC programs correctly handle all possible input scenarios, including sensor failures and adversarial manipulation, against explicitly defined safety policies.
• Cross-toolchain coverage: Support for programs compiled from OpenPLC, Beremiz, Simulink, and Arduino means the tool is applicable across a wide range of industrial development environments.
• Sensor redundancy validation: The Boeing 737 MAX case study powerfully illustrates the consequences of single-sensor trust. Taviran can systematically identify programs that fail to cross-reference redundant sensors.
• Open-source dataset: The released PLC binary dataset with ground truth FSMs enables future research in PLC binary analysis and industrial control system security.

Key Takeaways

• Blind Trust Vulnerabilities (BTVs) are a new class of logic bug where PLC programs trust sensor inputs without adequate validation or cross-referencing
• The Boeing 737 MAX crashes that killed 346 people exemplify the catastrophic consequences of blind trust in faulty sensor data
• Taviran recovers finite state machines from PLC binaries using concolic execution with abstract state deduplication, avoiding state explosion
• 17 BTVs discovered across 22 PLC binaries spanning 5 architectures and 4 toolchains, including real-world ArduCopter and rover systems
• The FSM recovery algorithm has a formal proof of completeness
• All artifacts including the first public PLC binary dataset with FSMs are open-sourced on GitHub

About the Speaker(s)

Fangzhou Dong (Bonnie Dong) is a researcher at Arizona State University. The research is a collaboration between Arizona State University and New Mexico State University. Dong delivered a clear, well-structured presentation with confident handling of technical questions from researchers at USC, Dartmouth College, and MIT Lincoln Laboratory, demonstrating deep understanding of both the formal methods and the practical ICS security implications.