An Approach for Safe and Secure Software Protection Supported by Symbolic Execution

This paper presents a novel copy-protection method for industrial control software that binds programs to specific hardware using Physically Unclonable Functions (PUFs) and employs symbolic execution to guarantee safety property preservation and security against reverse engineering.

The Gist

Imagine you own a very expensive, high-tech coffee machine. You want to sell the software that controls it, but you don't want people to steal that software and run it on a cheap, knock-off machine they built in their garage.

Usually, software is like a recipe: if you copy the recipe, you can bake the cake anywhere. But this paper proposes a new way to protect software so that it only works on the exact machine it was designed for. If you try to run it on a different machine, the software doesn't just crash or stop working; it keeps working, but it starts doing weird, unpredictable things that are still safe, just not useful to the thief.

Here is how they do it, broken down into simple concepts:

1. The "Digital Fingerprint" (The PUF)

Every physical object has tiny, microscopic imperfections. A fingerprint is unique to a person; a specific piece of computer memory (like DRAM) has unique physical quirks caused by the manufacturing process.

The authors use something called a PUF (Physically Unclonable Function). Think of the PUF as a magical lock on the machine.

• The Challenge: The software asks the machine a question (e.g., "What is the electrical resistance of this specific memory cell?").
• The Response: Because of the microscopic imperfections, the machine gives a unique answer.
• The Catch: You cannot clone this machine. Even if a thief builds an exact replica of the hardware, the microscopic imperfections will be slightly different, so the "answer" to the question will be wrong.

2. The "Safe-But-Weird" Strategy

In the past, if software detected it was on the wrong machine, it might just shut down or crash. But in industrial settings (like controlling a robot arm or a traffic light), a crash can be dangerous.

This paper introduces a "Safe-by-Design" approach.

• On the Real Machine: The software asks the PUF, gets the correct answer, and proceeds to the next step perfectly.
• On a Fake Machine: The software asks the PUF, gets the wrong answer, and realizes, "Oh, I'm not on the right machine." Instead of crashing, it enters a "Safe Mode."
  • Analogy: Imagine a traffic light controller. On the real machine, it turns the light Green, then Red, then Yellow. On a fake machine, the software gets confused and starts turning the lights Green, then Red, then Green again, or maybe it flashes them randomly.
  • The Result: The traffic still flows (safely), but it's chaotic and doesn't follow the intended schedule. The thief can't use the machine for its intended purpose, but no one gets hurt.

3. The "Crystal Ball" (Symbolic Execution)

How do the authors know that the "Safe Mode" won't accidentally cause an accident (like turning two traffic lights green at the same time)?

They use a technique called Symbolic Execution.

• The Metaphor: Imagine you are a director rehearsing a play. Instead of using real actors, you use "ghost actors" who represent every possible situation at once. You run the script through every possible combination of events to see if anything bad could happen.
• The Application: Before the software is even released, the authors run this "ghost rehearsal." They mathematically prove that no matter what wrong answer the fake machine gives, the software will never enter a state that causes a disaster. It guarantees that the "weird behavior" is always safe.

4. Why Thieves Can't Win

The paper argues that stealing this software is a nightmare for a hacker:

• Static Analysis (Reading the code): Even if the hacker steals the code and tries to read it, they can't figure out the correct answers to the PUF questions because those answers depend on the physical hardware, which they don't have.
• Dynamic Analysis (Running the code): If they try to run the code on a fake machine, it just behaves chaotically. To figure out the "right" path, they would have to reverse-engineer the entire logic of the machine from scratch.
• The Cost: It would take so much time and money to crack the protection that it's cheaper to just build a new machine from scratch.

Summary

This paper presents a security system that binds software to a specific piece of hardware using its unique physical "fingerprint." If the software is stolen and run on the wrong machine, it doesn't break; it just acts strangely but safely. The authors use advanced mathematical "rehearsals" to prove that this strange behavior will never cause an accident, making industrial software theft both difficult and economically unviable.

Technical Summary

Here is a detailed technical summary of the paper "An Approach for Safe and Secure Software Protection Supported by Symbolic Execution."

1. Problem Statement

The paper addresses the critical issue of Industrial Intellectual Property (IP) theft, specifically the reverse engineering and unauthorized copying of industrial control software.

• The Threat: While hardware replication is difficult, software can often be copied verbatim without reverse engineering. Attackers can decompile binaries to understand logic and replicate the system on different hardware.
• The Limitation of Existing Solutions: Previous hardware-software binding methods (e.g., using PUFs to determine jump addresses) often result in unsafe behavior or system crashes if the hardware response is incorrect or if the software runs on unauthorized hardware. In industrial settings, a crash or unsafe state is unacceptable.
• The Goal: Develop a copy-protection mechanism that binds software to specific hardware such that:
  1. The software executes correctly only on the target machine.
  2. If executed on unauthorized hardware (or if the PUF response is wrong), the software behaves differently (to hinder reverse engineering) but safely (adhering to safety constraints).
  3. Reverse engineering the protection is rendered economically unviable due to high complexity.

2. Methodology

The authors propose a novel approach combining Physically Unclonable Functions (PUFs) with Symbolic Execution applied to Control State Abstract State Machines (ASMs).

A. Formal Specification (Control State ASMs)

The target software is modeled as Control State ASMs. These are finite sets of transition rules where the system moves between control states based on conditions. This formalism is chosen because:

• It captures the behavior of industrial control programs (e.g., traffic lights, PLCs).
• It is executable and amenable to symbolic execution.
• It allows for precise definition of safety constraints.

B. Hardware Binding via PUFs

The method binds the software to a specific machine using a PUF (a hardware primitive that generates unique responses to challenges based on physical manufacturing variations).

• Challenge-Response: The software queries the PUF with a challenge derived from the current control state.
• State Transition Logic: Instead of a simple jump to a fixed address, the PUF response determines the next control state.
• The "Safe-by-Design" Mechanism:
  • If the software runs on the target machine, the PUF returns the expected response, and the program transitions to the intended next state.
  • If the software runs on unauthorized hardware (or the PUF fails), the response will likely be incorrect. Instead of crashing or jumping to a random (unsafe) location, the system enters a non-deterministic safe mode. It selects a next state from a pre-calculated set of safePhases that are guaranteed not to violate safety constraints (e.g., ensuring two traffic lights are never green simultaneously).

C. Symbolic Execution for Safety Verification

The core innovation is using symbolic execution to mathematically guarantee safety during the protection process.

1. Symbolic Assignment: Instead of concrete values, state variables are assigned symbolic values (e.g., $\alpha, \beta$).
2. Path Analysis: The system symbolically executes all possible transitions of the protected program.
3. Safety Condition Derivation: The system analyzes path conditions to identify which next states would violate the safety property $\Psi$ (e.g., $GoLight(1) \land GoLight(2)$).
4. Safe Set Construction: The set of safePhases (or safeCtlStates) is defined as the set of all possible next states excluding those that satisfy the violation condition.
5. Guarantee: The protection mechanism is constructed such that even if the PUF response is wrong, the non-deterministic choice is restricted only to the safePhases set.

D. The Automated Protection Algorithm

The paper outlines a 7-step mechanical process to transform a standard ASM specification into a protected one:

1. Mapping: Map control state transitions to PUF challenges.
2. Rule Definition: Define a ChooseCtlState rule that queries the PUF.
3. Replacement: Replace standard state transitions (ctlState := j) with the ChooseCtlState rule.
4. Guard Modification: Update state guards to match the new logic.
5. Symbolic Initialization: Assign symbolic values to all relevant state locations.
6. Symbolic Execution: Execute the modified program symbolically to generate path conditions and successor states.
7. Safety Set Calculation: Compute the set of safe states ($safeCtlStates$) by negating the conditions that lead to safety violations.

3. Key Contributions

1. Safe-by-Design Copy Protection: Unlike previous methods that risk crashes or unsafe states upon failure, this approach guarantees that unauthorized execution remains within the bounds of safety constraints.
2. Integration of Symbolic Execution and PUFs: This is the first known application of symbolic execution to support safe copy-protection via hardware binding. It automates the verification that the protection mechanism itself does not introduce safety bugs.
3. Formal Framework: The method is rigorously defined using Control State ASMs, providing a formal basis for proving that the protected algorithm preserves the safety properties of the original algorithm.
4. Reverse Engineering Resistance: By forcing the software into a non-deterministic but safe state on unauthorized hardware, the method makes it extremely difficult for attackers to deduce the correct logic flow, as they cannot distinguish between "correct" and "safe-but-wrong" behaviors without the specific PUF.

4. Results and Evaluation

• Case Study: The authors demonstrated the method using a one-way traffic light control algorithm. They successfully identified the set of safe phases and showed that the protected algorithm would never enter the "Go1Go2" (unsafe) state, even if the PUF response was incorrect.
• Security Analysis (Threat Model):
  • Static Analysis: Decompiling the binary reveals the logic of the ChooseCtlState rule but does not reveal the specific PUF responses required for correct execution. Reconstructing the logic manually is deemed time-consuming and economically unviable for complex systems.
  • Dynamic Analysis: Running the software on the target hardware allows an attacker to trace the flow, but this is slow for complex systems with many paths. Furthermore, dynamic analysis can interfere with time-dependent PUFs (like DRAM-based PUFs).
  • Conclusion: The protection is robust against standard reverse engineering techniques, making the effort to bypass it disproportionate to the value of the IP.

5. Significance

• Industrial Relevance: This approach directly addresses the needs of the industrial automation sector (e.g., the DEPS project context), where safety is paramount. It allows companies to protect their IP without compromising the fail-safe nature of their control systems.
• Paradigm Shift: It moves software protection from "obfuscation and crash prevention" to "safe degradation." The system is designed to fail gracefully (safely) rather than catastrophically when the hardware binding is broken.
• Future Impact: The authors plan to automate the identification of control states and safety constraints, and to integrate SMT solvers to handle the complexity of the logical formulas generated during symbolic execution, making the method scalable for large industrial applications.

In summary, the paper presents a rigorous, mathematically grounded method for securing industrial software that ensures security against theft without sacrificing safety of operation, leveraging the unique properties of PUFs and the analytical power of symbolic execution.