# REMaQE - Reverse Engineering Math Equations from Executables

Meet Udeshi Department of Electrical and Computer Engineering, NYU Tandon
School of Engineering, Brooklyn, NY, 11201<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>Prashanth Krishnamurthy11footnotemark: 1 Hammond
Pearce11footnotemark: 1 Ramesh Karri11footnotemark: 1 Farshad
Khorrami11footnotemark: 1

## Abstract

Cybersecurity attacks against industrial control systems and cyber-physical
systems can cause catastrophic real-world damage by infecting device binaries
with malware. Mitigating such attacks can benefit from reverse engineering
tools that recover sufficient semantic knowledge in terms of mathematical
operations in the code. Conventional reverse engineering tools can decompile
binaries to low-level code, but offer little semantic insight. This paper
proposes REMaQE, an automated framework for reverse engineering of math
equations from binary executables. REMaQE uses symbolic execution for dynamic
analysis of the binary to extract the relevant semantic knowledge of the
implemented algorithms. REMaQE provides an automatic parameter analysis pass
which also leverages symbolic execution to identify input, output, and
constant parameters of the implemented math equations. REMaQE automatically
handles parameters accessed via registers, the stack, global memory, or
pointers, and supports reverse engineering of object-oriented implementations
such as C++ classes. REMaQE uses an algebraic simplification method which
allows it to scale to complex conditional equations with ease. These features
make REMaQE stand out over existing reverse engineering approaches for math
equations. On a dataset of randomly generated math equations compiled to
binaries from C and Simulink implementations, REMaQE accurately recovers a
semantically matching equation for 97.53% of the models. For complex equations
with more operations, accuracy stays consistently over 94%. REMaQE executes in
0.25 seconds on average and in 1.3 seconds for more complex equations. This
real-time execution speed enables a smooth integration in an interactive
mathematics-oriented reverse engineering workflow.

##  1 Introduction

Embedded systems in industrial control systems (ICS), cyber-physical systems
(CPS), and the internet of things (IoT) are vulnerable to process aware
attacks that compromise the physical process of the system [12, 14]. Such
attacks can lead to breaches of safety-critical requirements, resulting in
real-world destruction and harm. For example, Stuxnet injected malware in the
programmable logic controllers (PLC) of a nuclear facility to adversely modify
the centrifuge motor frequencies [17]. The Aurora Generator Test demonstrated
another vulnerability by rapidly opening and closing circuit breakers when
out-of-phase and causing severe damage to a diesel generator [33]. The
BlackEnergy attack against Ukraine’s power grid opened several breakers at
once to cause a power outage [27]. Covert attacks are also possible:
Krishnamurthy et. al [15] develop a stealthy communication channel that
utilizes analog emissions from a Cyber-Physical System (CPS). This method
maintains the closed-loop process characteristics by factoring in controller
dynamics during attack design.

One can analyze the cybersecurity of embedded systems by leveraging semantic
understanding of the physical process features, such as mathematical models,
control algorithms, and dynamic behavior of the process. For example, Yang et.
al [34] derive control invariants of the physical process using PLC runtime
logs and detect changes in these invariants to signal an intrusion. The
Trusted Safety Verifier in [21] is implemented as a bump-in-the-wire and
verifies safety-critical code for PLCs by recovering a semantic graph of the
program and asserting safety-critical properties using model checking.
Alternatively, on the offensive side, McLaughlin [22] shows that recovering
boolean expressions of the PLC control code can be used to automatically
generate dynamic malware payloads, and the CLIK attack on PLCs [10] decompiles
the control logic to high-level automation languages [4], making malicious
code changes to disrupt the physical process.

Although there are many methods to reverse engineer embedded systems and
extract the semantic knowledge for cybersecurity, this paper focuses on the
analysis and reverse engineering of binary executables of the embedded devices
(e.g., PLC) which interact with physical sensors and actuators. Reverse
engineering the mathematical models and control algorithms implemented in
these binaries can reveal the semantic knowledge necessary to understand these
embedded systems. This semantic knowledge is useful for applications such as
(a) analyzing malicious changes injected in the binary by malware, (b)
examining adversarial systems, such as unmanned vehicles used for
reconnaissance, (c) identifying bugs and vulnerabilities in implemented
systems for patching or exploitation, (d) intellectual property (IP) violation
and its detection in the wild, and (e) recovering details of legacy systems
without source code.

###  1.1 Reverse Engineering of Binaries

While the binary compilation process works well in the forward direction
(i.e., from mathematical model to binary executable), reversing this process
is notoriously difficult. Math equations compiled into binaries are deployed
on a diverse range of embedded hardware platforms and target a variety of
processor architectures. The implementation of mathematical equations thus
involves many platform-specific details (e.g. for floating-point numbers),
which offer no semantic information. The reverse engineering approach should
refine and discard these implementation details before generating human-
friendly equations using conventional math symbols and operations.

Typical reverse engineering techniques such as disassembly or decompilation
extract information about the program and represent it in a low-level source
language like assembly or C [9]. The goal of decompilation is to reconstruct
the original source code from binary executables as accurately as possible
[9]. Decompilers intend to recover many implementation details of the program
such as variable types, memory layout, control flow, and data flow [3]. These
syntactical/semantic details are necessary when the recovered programs need to
be represented in languages like C or Java. However, due to the noisy and
obfuscating nature of compilation, decompilation is an indeterminate process;
hence, the recovered code may obscure the original high-level semantic
meaning.

###  1.2 Extracting Semantic Information

Disassembly and decompilation tools like IDA Pro [8] and Ghidra [6] are useful
for analysis of binaries, but they do not recover semantic information.
Recovering math equations from the binaries requires subject matter expertise
and manual effort of identifying and clustering code sequences, mapping them
to math primitives, and understanding how identified blocks will combine and
simplify. Approaches tailored to domains like ICS or CPS can use knowledge
about the compilation and implementation tool chain used by these domains and
make assumptions to build a better representation in domain-specific
languages. For example, executables from control system devices can be reverse
engineered to automation languages like Ladder Logic and Instruction List [10,
25, 18]. These methods offer better abstraction than languages like assembly
or C, but they too cannot represent the semantic information, therefore
necessitating additional domain expertise and manual effort to recover math
equations. Reverse engineering to low-level languages does not reveal the
semantics of the implemented algorithm. An automated framework which reverse
engineers math equations from binaries and presents them in a human-friendly
form is pivotal to understand the semantics of embedded systems.

Symbolic execution is a popular technique to gain semantic insight into a
binary. Symbolic execution tools capture the symbolic expression trees of
computation, and explore all execution paths through the program [29]. Their
primary use cases are automatic test generation [1, 30], automatic exploit
detection and generation [2, 28], and reverse engineering [5, 21]. The
symbolic expressions produced in this process are “solved” using constraint
solvers or satisfiability module theory (SMT) solvers to identify concrete
inputs. While test generation requires determining input sets for maximum
program coverage, exploit generation needs specific inputs to trigger bugs or
hijack control flow, and reverse engineering finds inputs for systematic
program exploration. Although these symbolic expressions are generated to
assist SMT solver tools, as discussed later in Section 5.5, they are not
presented as human-friendly mathematical equations.

A math equation can be represented as a computational flow graph, which is
mapped to both control flow and data flow when implemented. Given the nature
of math equations, control flow can range from simple function calls to
bounded loops to data-dependent conditional branches. Hence, dynamic control
and data flow analysis is required to capture the details of the implemented
math equation for reverse engineering. Previous methods depend on symbolic
execution of binaries for dynamic control and data flow analysis, obtaining
essential semantic understanding of the program. Symbolic execution is highly
valuable for extracting symbolic expressions representing the executable’s
computations and exploring branching execution paths. However, it alone cannot
present mathematical equations in a human-friendly form. To achieve this,
symbolic execution tools must be utilized effectively with detailed knowledge
of the binary.

###  1.3 Contributions

This paper proposes the REMaQE framework to reverse engineer math equations
from binary executables. Similar to the existing approaches, REMaQE relies on
symbolic execution for dynamic analysis of the program and to extract semantic
information. Instead of looking for patterns or semantic matches with well-
known algorithms, REMaQE refines and simplifies extracted information to a
math equation. REMaQE employs automatic parameter analysis of functions to
identify important metadata regarding the function arguments stored in
register, stack, global memory, or accessed via pointer. This way, REMaQE is
the first work able to reverse engineer a variety of function implementations,
including object-oriented C++ code. Simplification of math equations in REMaQE
is performed via math-aware algebraic methods. This overcomes limitations of
generic approaches such as machine learning methods for equation
simplification and enables REMaQE to simplify complex conditional equations.
Section 3 discusses the advantages of REMaQE over existing approaches.

REMaQE provides an application programming interface (API) in Python, which
allows the user to analyze the executable function by function and to control
various aspects of reverse engineering such as variable naming and function
inlining. The API can be used in Python scripts or in a Python command line
interface like I-Python or Jupyter for interactive reverse engineering, It can
also be integrated as a plugin into decompilation frameworks with a graphical
interface (to be addressed in future work). The contributions of this paper
are threefold:

  1. 1.

The REMaQE framework for reverse engineering mathematical equations from
executables, which offers two major improvements over existing approaches:

    1. (a)

Automatic parameter analysis to recognize input, output, and constant
parameters in the implemented equation. This enables reverse engineering of
object-oriented implementations, such as C++ classes and struct pointer based
C functions.

    2. (b)

Algebraic simplification to transform extracted symbolic expressions into
easily understandable mathematical equations. This handles much more complex
expressions than existing approaches with machine learning methods.

  2. 2.

A method for random generation of math equations of significant complexity
using directed acyclic graphs, and their implementation as C code and Simulink
models.

  3. 3.

A dataset of binary executables compiled from the generated C codes and
Simulink models, paired with the ground truth math equations, to evaluate
REMaQE.

The paper is organized as follows: Section 2 offers a motivating example for
employing REMaQE, Section 3 reviews related work, Section 4 provides a
background on symbolic execution, Section 5 details REMaQE’s implementation,
Section 6 explains the dataset generation methodology and presents the
results, Section 7 showcases a case study on reverse engineering a Support
Vector Machine (SVM) classifier using REMaQE, and Section 8 concludes and
explores future work.

##  2 Motivation

⬇

1float saturate(float x, float xmin, float xmax) {

2 if (x > xmax) x = xmax;

3 else if (x < xmin) x = xmin;

4 return x;

5}

6

7class PID {

8 float Kp, Ki, Kd, prev_err, integral, lo, hi;

9...

10 float update(float targ, float act, float dt) {

11 float err = targ - act;

12 integral += err * dt;

13 float p = Kp * error;

14 float i = Ki * integral;

15 float d = Kd * (err - prev_err) / dt;

16 prev_err = err;

17 return saturate(p + i + d, lo, hi);

18 }

19};

(a) PID controller implemented in C++.

⬇

1void __thiscall PID::update(PID *this,float param_1,float param_2,float
param_3) {

2 float fVar1;

3 float fVar2;

4 float fVar3;

5

6 fVar1 = param_1 - param_2;

7 fVar2 = *(float *)(this + 0xc);

8 *(float *)(this + 0xc) = fVar1;

9 fVar3 = *(float *)(this + 0x10) + fVar1 * param_3;

10 *(float *)(this + 0x10) = fVar3;

11 saturate(fVar3 * *(float *)(this + 4) + fVar1 * *(float *)this +

12 (*(float *)(this + 8) * (fVar1 - fVar2)) / param_3,*(float *)(this + 0x14),

13 *(float *)(this + 0x18));

14 return;

15}

(b) PID::update() decompiled by Ghidra.

⬇

1float saturate(float param_1,float param_2,float param_3) {

2 if ((param_1 < param_3) && (param_3 = param_1, param_1 < param_2)) {

3 param_3 = param_2;

4 }

5 return param_3;

6}

(c) saturate() decompiled by Ghidra.

⬇

<FP32 if (if fpLT(fpToFP(fpAdd(fpAdd(<...>, <...>), fpDiv(<...>, <...>)), DOUBLE), fpToFP(fpToFP(mem_ffffff18_9_32, FLOAT), DOUBLE)) then ((<...>[0:0] | <...> ^ <...>) ^ 1) == 0 else ((<...>[0:0] | <...> ^ <...>) ^ 1) == 0) then fpToFP((if (if fpLT(<...>, <...>) || fpLT(<...>, <...>) then <...>[3:3] == 0 else <...>[3:3] == 0) then fpToIEEEBV(fpAdd(fpAdd(<...>, <...>), fpDiv(<...>, <...>))) else mem_ffffff14_10_32), FLOAT) else fpToFP(mem_ffffff18_9_32, FLOAT)>

(d) Symbolic expression generated by Angr.

$\operatorname{saturate}(x_{0},x_{1},x_{2})=\begin{cases}x_{0}&\text{for}\>x_{0}\leq
x_{2}~{}\text{and}~{}x_{0}>x_{1}\\\ x_{1}&\text{for}\>x_{0}\leq x_{2}\\\
x_{2}&\text{otherwise}\end{cases}$ (1)
$\operatorname{update}(x_{0},...x_{9})=\operatorname{saturate}{\left(x_{3}\left(x_{0}-x_{1}\right)+x_{4}\left(x_{2}\left(x_{0}-x_{1}\right)+x_{7}\right)+\frac{x_{5}}{x_{2}}\left(x_{0}-x_{1}-x_{6}\right),x_{8},x_{9}\right)}$
(e) Math equations recovered by REMaQE.

Figure 1:  Reverse engineering the PID controller involves multiple stages:
(a) C source code, (b) PID::update function decompiled with Ghidra, (c)
saturate function decompiled with Ghidra, (d) symbolic expression generated
using Angr for symbolic execution, (e) math equations retrieved through
REMaQE.

This section presents the reverse engineering of an example to demonstrate the
motivation behind REMaQE and the need for extracting math equations. Figure
1(a) shows the C++ implementation of a Proportional-Integral-Derivative (PID)
controller, which implements two functions PID::update and saturate. This
example is compiled for the ARM 32-bit Hard-Float (ARM32-HF) target. For a
comparison, the generated binary is reverse engineered using different tools
namely, Ghidra for decompilation, Angr for symbolic execution, and REMaQE to
recover math equations.

The functions are decompiled using Ghidra to generate the C source shown in
Figure 1(b) and Figure 1(c). The decompiled saturate function is presented in
a complicated form which makes it difficult to understand, even with the
knowledge of what the source function implements. The if condition on line 2
of Figure 1(c) contains an assignment in the second condition, which is only
executed if the first condition is true, due to the left-to-right evaluation
of the && operator[7]. The decompiled PID::update function uses pointer
dereferencing, pointer value assignments, and type-casting, that appear
because this is how the original C++ class has been implemented in binary.
Ghidra has generated a faithful representation. However, these implementation
details present in the syntax are obscuring the semantic information of this
function. Thus, significant effort is required to clean up and extract a math
equation of the PID controller.

Figure 1(d) shows the symbolic expression generated by the symbolic execution
tool Angr. Even though the generated expression has recovered sufficient
semantic information about the source function to be utilized by SMT solvers
or constraint solvers, it is not presented in a simple human-friendly form and
makes it difficult to directly understand the implemented equation.

Figure 1(e) shows the math equations recovered by REMaQE for both the saturate
and PID::update functions. The conditional logic of the saturate function is
converted into a piecewise expression, which clearly demonstrates the cases
being checked. The equation for PID::update shows a call to saturate,
including what parameters the function is called with. REMaQE provides a
modular view of the math equations implemented function-by-function. This
example demonstrates the advantage of the automated reverse engineering
approach of REMaQE in providing a meaningful, semantically rich understanding
of the implemented math equations for binary analysis.

##  3 Related Work

As discussed in Section 2, disassembly and decompilation techniques are unable
to provide relevant semantic information of a program, while REMaQE is able to
portray the program as a semantically equivalent math equation. REMaQE is not
intended to replace decompilers or decompilation techniques. Instead, it can
be integrated with the user interface of decompilation tools to offer the
semantic information of equations alongside useful information extracted by
the decompiler, for example, the C code of a function along with the math
equation.

Recent approaches to extract high-level semantic information [31, 13, 11] have
used domain knowledge and assumptions to match the extracted information to
predefined mathematical structures. MISMO [31] employs a template of popular
control algorithms and performs semantic matching on expressions extracted
using symbolic execution to determine which control algorithm is implemented.
DisPatch [13] targets controllers for robotic aerial vehicles, and identifies
customized implementations of the proportional-integral-derivative (PID)
controller. These methods are tailored to a domain and can be sensitive to
alterations in implementation that might breach domain-specific assumptions.
Although they extract semantic information similar to REMaQE, implementing and
effectively deploying such techniques necessitates combining expert-derived
domain knowledge with reverse engineering. These methods may fail on outlier
cases. In contrast, REMaQE provides a versatile approach based on a
fundamental set of assumptions that can be readily expanded, enabling its
application to various domains with minimal adaptation.

To overcome the aforementioned problems in prior methods, PERFUME [32] follows
a generic approach which does not rely on semantic pattern matching, yet is
able to present the underlying math equation pertaining to the implemented
algorithm in a human-friendly form. In terms of the approach, PERFUME is most
similar to REMaQE among existing literature. PERFUME uses symbolic execution
to extract the semantic information in the form of symbolic expressions, and
trains a machine learning based sequence-to-sequence machine translation model
to “translate” that symbolic expression into a simplified, human-friendly math
equation. The framework is offered as a plugin for Ghidra, which augments
decompiled output with additional semantic information and integrates well
with an interactive reverse engineering workflow.

PERFUME can handle functions with parameters in registers, but is unable to
manage parameters accessed through global memory or pointers. In contrast,
REMaQE employs a parameter analysis pass, which collects metadata about each
parameter’s storage location. Thus, it can handle registers, stacks, global
memory, and pointer dereferencing. This capability enables REMaQE to reverse
engineer a wider variety of functions, including those found in object-
oriented implementations in real-world programs, such as C++ classes and
struct pointers. PERFUME cannot handle the PID example presented in Section 2,
because the function uses a class pointer to dereference inputs.

While PERFUME’s machine translation model struggles to simplify long and
complex symbolic expressions arising from floating-point comparisons, REMaQE’s
algebraic simplification stage adopts a math-aware algorithmic approach. Using
well-known strategies, it can handle complex expressions generated from
functions with floating-point comparisons and conditional logic. This
deterministic simplification scales based on the complexity of the simplified
expression, not the input expression. PERFUME’s machine translation model
cannot simplify the complex conditional expression generated for the saturate
function in Figure 1(d), whereas REMaQE produces a compact, human-friendly
equation. REMaQE’s parameter analysis and algebraic simplification features
set it apart from PERFUME and other existing symbolic execution-based
approaches.

##  4 Background: Symbolic Execution

This section introduces symbolic execution and its application in REMaQE.
Symbolic execution involves running a program in an emulated environment using
symbols instead of concrete values. This process generates symbolic expression
trees (ETs), a type of abstract syntax tree. When conditional branches depend
on symbolic data, the execution forks to follow both taken and not taken
paths, adding a constraint or predicate to each path based on the branch
condition. Constraints accumulate as the execution progresses through each
branch. Upon reaching an equivalence point, such as a function return
statement, the ETs can be combined into one, utilizing the constraints
gathered along each path. For example, symbolic execution of the binary code
of the saturate function shown in Figure 1(a) leads to forking of paths on the
branch instruction on Line 2, leading to two execution paths, one which takes
the branch and the other which does not take the branch. These paths are
merged into one at the function return, and the ET for the return value is
simplified by REMaQE into a piecewise form as shown in Figure 1(e).

In the context of reverse engineering math equations, symbolic execution
offers two big advantages. First, operations representing the math equation
are naturally captured and tracked. Second, the forking on branches ensures
that all code is explored during execution, which gives a full picture of the
implemented math equation. Code coverage is an important requirement, as
failing to explore the entire codebase can extract a math equation that is
undefined for certain input values.

REMaQE relies on the Angr binary analysis framework [29] for dynamic analysis
and symbolic execution. Angr operates on a symbolic state of execution, that
records register and memory contents during execution. Execution proceeds in
steps of a single basic block. When execution paths fork, the execution states
are replicated and relevant constraints are added to each state. Constraints
on a state captures the branch conditions which need to be satisfied to take
that execution path. These constraints apply to every register and memory
location which is initialized in that state. When execution paths merge, a
merged state is created by combining ETs as explained.

##  5 Implementation

###  5.1 Assumptions and Limitations

We focus our evaluation in this paper on the widely-used 32-bit ARM
architecture with hardware floating point support (ARM32-HF), although it is
straightforward to extend the REMaQE framework to other architectures
supported by symbolic execution frameworks. We assume that all math
computations in the binaries are performed in 32-bit floating point type. This
is done to avoid issues with datatype and precision conversion, and to focus
the evaluation on extracting and simplifying the equations. While certain
integer calculations like pointer arithmetic and array indexing are supported,
calculations which represent a part of the math equation as datatype
conversions are not supported (e.g. a floor111floor($x$) is defined as
greatest integer less than or equal to $x$. operation implemented by casting a
floating-point value to integer). We also assume that conditional checks
performed in the executable are comprised of simple comparisons, as justified
in Section 5.5—complicated condition checks, for example a bit-wise operation
checking the sign bit of a floating-point to implement a comparison with 0,
are currently out of scope.

###  5.2 Overview of REMaQE

Figure 2: Overview of the REMaQE framework. Average execution time of the
pipeline is 0.25 seconds, from when the user provides which function to
reverse engineer, to when REMaQE returns the math equations.

Figure 2 presents an overview of the REMaQE framework. REMaQE focuses on
reverse engineering math equations of one function at a time. This allows
reverse engineering to proceed in a modular fashion, similar to the approach a
human may follow manually. REMaQE first extracts a callgraph of the functions
present in the executable. The user then selects a function for REMaQE to
analyze. The function runs through the parameter analysis stage to gather
information about input, output and constant parameters that express the math
equation. This information is packaged into the parameter metadata. The
symbolic execution stage then runs the function with initialized inputs and
extracts the symbolic ETs for each output. The output ETs are simplified by
the algebraic simplification stage to generate the final math equation.

REMaQE’s function-by-function approach enables control over whether to
represent function calls as-is or substitute them in the extracted equation.
For instance, trigonometric functions might be implemented using approximating
polynomials or platform-specific hardware extensions in libraries. However,
such implementation details don’t provide valuable information and may even
cloud the equation’s meaning. In such cases, it’s better to represent these as
function calls in the generated equation. Conversely, in some situations, it
could be beneficial to substitute a called function’s equation into the caller
function’s equation.

When reverse engineering a function, a callback hook is added to the Angr
execution engine. This hook activates when the function is called and directly
returns the extracted math equation by replacing input arguments from the
call. Therefore, it’s crucial for REMaQE to start with the inner-most
functions and then proceed outward. Figure 3 shows the REMaQE pipeline to
reverse engineered and extract math equations. The PID controller example in
Figure 1 is used to explain the REMaQE pipeline. The PID::update function is
selected for analysis. Snippets of intermediate outputs of each stage of the
pipeline are elaborated in Sections 5.3, 5.4, and 5.5.

Figure 3: REMaQE reverse engineering pipeline. The PID::update function from
Figure 1 is used as an example, and intermediate outputs are shown for each
stage through the pipeline: (a) Parameter analysis automatically identifies
the input, output and constant parameters of the function along with their
kind and storage location, (b) Symbolic execution runs the function with
properly initialized symbolic inputs and gathers the output symbolic ETs, and
(c) Algebraic simplification converts the output ET to a human-friendly math
equation.

###  5.3 Parameter Analysis

Table 1: Parameter metadata generated for the PID example in Figure 1. The
input and output parameters are listed, along with storage kind and location.

I/P | Kind | Location
---|---|---
$x_{0}$ | reg | s0
$x_{1}$ | reg | s1
$x_{2}$ | reg | s2
$x_{3}$ | pointer | r0[0x0]
$x_{4}$ | pointer | r0[0x4]

I/P (cont.) | Kind | Location
---|---|---
$x_{5}$ | pointer | r0[0x8]
$x_{6}$ | pointer | r0[0xc]
$x_{7}$ | pointer | r0[0x10]
$x_{8}$ | pointer | r0[0x14]
$x_{9}$ | pointer | r0[0x18]

O/P | Kind | Location
---|---|---
$y_{0}$ | reg | s0
$y_{1}$ | pointer | r0[0xc]
$y_{2}$ | pointer | r0[0x10]

To invoke symbolic execution of a function, it is important that the execution
entry state is correctly initialized with symbolic parameters placed in the
expected locations. Also, to read the output ET, it is necessary to know where
the function places the outputs. A math equation may also use certain
constants, which the tool should distinguish from inputs and try to extract
their hard-coded value. Parameter analysis stage collects the relevant
information of the storage location of parameters.

The parameters of a function are defined as the inputs, outputs and constants
which are used to express the implemented math equation. Temporary variables
which may be used in the function implementation are not considered as
parameters. Function arguments and return values need not represent parameters
in case they hold pointer addresses. In the PID example, the PID::update
function takes the class pointer as an argument, then dereferences the seven
float parameters for computation. This pointer is not considered a parameter
by REMaQE, instead each of the seven class members are identified as input
parameters. Similarly, the members prev_err and integral are considered as
output parameters as they are written to by the function, even though they are
not part of the function’s return value.

The memory layout of data at the pointer address is unimportant since each
dereferenced struct member is considered a distinct parameter. Only the offset
is necessary. This distinction helps to abstract different implementation
details, allowing for a clean math equation extraction. The metadata for each
parameter contains the following information: (i) Parameter name, (ii) Storage
kind, and (iii) Storage location. Storage location, depending on kind, is
either the architectural name of Register, Stack offset, Global address, or
Pointer address and offset. The storage location of the pointer address is
also necessary, since a concrete address pointing to memory containing
symbolic parameters must be passed as an argument to the function.

Algorithm 1 describes the procedure for parameter analysis that takes a
function as input. The parameter analysis pass has no knowledge of function
parameters, so it does not initialize the symbolic execution state and relies
on Angr to fill in uninitialized values when accessed. The “SymbolicExecute”
call performs this uninitialized execution and records an execution trace. The
execution trace is parsed and read/write accesses to each storage location are
recorded in a sequential history. The “GetReadsWrites” call gathers this
access history for each storage location. Locations with a first access as
read are marked as inputs. These input locations are filtered and labeled as
constant if they have no write access and contain an initialized value.
Uninitialized locations would be filled with a symbolic value by Angr,
differentiating inputs from constants since constant parameters should be
hard-coded in the binary. Locations with at least one write access throughout
history are marked as output. A single location can be both input and output,
as the implementation may reuse storage locations, particularly registers.

The Table 1 shows the parameter metadata obtained for the PID::update
function. Inputs $x_{0}$-$x_{2}$ are assigned to ARM floating point registers
s0-s2. Inputs $x_{3}$-$x_{9}$ are dereferenced from the pointer stored in
register r0 with the corresponding offsets. The output $y_{0}$ is written back
to the same register s0, from which input $x_{0}$ is read, yet they are
distinguished as separate parameters. During the subsequent symbolic execution
stage, register s0 is initialized as the symbolic input $x_{0}$ at the start
and the ET for $y_{0}$ is read from it at the end. Similarly, the outputs
$y_{1},y_{2}$ reside in the same location as inputs $x_{6},x_{7}$ and are
handled accordingly.

Algorithm 1 Parameter analysis

procedure AnalyzeParams($F$: function)

$T$: execution trace $\leftarrow$ SymbolicExecute$(F)$

$Inputs,Outputs,Constants\leftarrow$ empty lists

for $A$: action in $T$ do

$L\leftarrow$ StorageLocation$(A)$

$Reads,Writes\leftarrow$ GetReadsWrites$(L)$

if $Writes$ is empty and $L$ is initialized then

$V\leftarrow$ GetValue$(L)$

Append $(L,V)$ to $Constants$

else if first$(Reads)<$ first$(Writes)$ then

Append $L$ to $Inputs$

end if

if $Writes$ is not empty then

Append $L$ to $Outputs$

end if

end for

return $Inputs,Outputs,Constants$

end procedure

Algorithm 2 Simplify conditional ETs

procedure SimplifyConditional($ET$)

for each comparison $C$ in $ET$ do

$LHS,RHS\leftarrow$ CanonicalOrder$(C)$

$LT\leftarrow LHS<RHS$

$EQ\leftarrow LHS==RHS$

$BE\leftarrow$ BoolExp$(C,LT,EQ)$

Replace $C$ with $BE$ in $ET$

end for

$S\leftarrow$ QuineMcCluskey$(ET)$

for each boolean $B$ in $S$ do

$C\leftarrow$ GetComparison$(B)$

Replace $B$ with $C$ in $S$

end for

return $S$

end procedure

###  5.4 Symbolic Execution

The symbolic execution stage initializes the symbolic state with appropriate
symbols for each parameter, using the metadata generated during the parameter
analysis stage. The execution runs till the function returns, at which point
all execution paths are merged into a final state. The parameter metadata is
ised to read the output ET from the correct storage locations in the final
state. Due to the proper initialization in this stage, the output ET depends
on the appropriate symbols, hence a meaningful math equation can be derived
for the output. Constants are also treated as symbols during reverse
engineering and are optionally substituted in the final equation, to ensure
that the value of the constants are not unnecessarily changed by any
computation during execution or simplification. This ensures that REMaQE
recovers the most accurate depiction of the constants which are hard-coded in
the binary and how they are expressed in the math equation.

###  5.5 Algebraic Simplification

The equations generated by reverse engineering have an order of operations
which follows the order in which the function performs the computations. There
may be a better way to represent the same order of operations, which leads to
a simplified equation. The definition of simplification is quite subjective,
so equations may have more than one representation which can be deemed as
simplified. REMaQE uses the Sympy symbolic processing engine [23] to simplify
equations. Sympy performs rule-based modifications on the equation to simplify
or cancel terms. It uses the number of operations as a heuristic to quantify
simplification level. The expressions are converted from the internal format
of Angr to a math equation with additional transformations/simplifications:
if-then-else statements are converted to piecewise functions
(sympy.Piecewise); function call hooks are replaced by appropriate function
syntax with call arguments; optionally, function calls can be inlined, in
which case the hook is replaced by the equation with input parameters
substituted for call arguments.

Sympy fails to simplify complex conditional expressions with deeply nested if-
then-else statements. Such expressions can result when merging execution paths
with constraints as described in Section 4. Figure 1(d) shows the internal
representation of the ET obtained after symbolic execution of PID::update. The
complex expression is generated because of the conditional statements in
saturate function. Even though saturate has only two conditions, the generated
ET represents the order of operations performed during symbolic execution
which semantically represent the conditions in the function. The order of
operations is determined by two factors. First, when the C function is
compiled to a target ISA, the conditional branches can be represented using a
variety of instruction sequences as decided by the compiler. Second, Angr maps
every instruction in the executable to an intermediate representation required
by it’s symbolic execution engine. This further modifies the order of
operations from what the binary’s instructions describe. The only guarantee is
that these modifications and mappings are semantically correct and represent
the original function. When the condition involves a comparison, a separate
instruction performs the comparison and updates bits in a flag register.
Later, conditional instructions check these bits of the flag register. When
these instructions are mapped to the IR, Angr can generate bit-wise operations
to perform checks, so these operations end up in the final expression.

The if-then-else operation of Angr requires a condition, a true clause, and a
false clause. The condition ET must yield a boolean value. In the context of
mathematical equations, it is logical to presume that the condition consists
of a comparison or several comparisons combined with basic boolean operations.
REMaQE takes advantage of this to streamline the condition ET before producing
the mathematical equation.

Each condition ET discovered in the full expression is simplified by the
procedure in Algorithm 2. The “CanonicalOrder” function gives an ordered pair
of the left-hand and right-hand side of the comparison $C$. Two booleans, $LT$
and $EQ$, are generated to represent less-than and equal-to comparisons. They
are combined to form the representative boolean expression $B$ by the
”BoolExp” function, and $C$ is replaced with $B$. The ordering of $LHS$ and
$RHS$, along with representing the comparison using $LT$ and $EQ$, helps
generate a canonical form of the comparison. For example, the condition (x <
y) && (y >= x) converts to LT_x_y && (LT_x_y || EQ_x_y), which simplifies to
LT_x_y and converts back to x < y. The Quine-McCluskey algorithm [26, 20] is
used to simplify the boolean expression $ET$ to $S$. This algorithm does not
scale to expressions with a large number of boolean variables. Based on our
assumption that math equations involve simple boolean expressions with few
comparisons, we typically handle only a few boolean variables, making this
algorithm suitable. The boolean variables in $S$ are replaced back with the
equivalent floating-point comparisons and returned to be processed further by
Sympy. Equations 2a-2c show the final simplified equations generated by REMaQE
for the outputs of the PID::update function.

$y_{0}=\operatorname{saturate}{\left(x_{3}\left(x_{0}-x_{1}\right)+x_{4}\left(x_{2}\left(x_{0}-x_{1}\right)+x_{7}\right)+\frac{x_{5}}{x_{2}}\left(x_{0}-x_{1}-x_{6}\right),x_{8},x_{9}\right)}$
(2a) $y_{1}=x_{0}-x_{1}$ (2b) $y_{2}=x_{2}\left(x_{0}-x_{1}\right)+x_{7}$ (2c)

##  6 Evaluation

We assess REMaQE based on the accuracy and human-friendliness of the reverse-
engineered equation and the time taken for reverse engineering.

Accuracy. The recovery is accurate if REMaQE runs without errors and the
equation semantically matches the ground-truth. Two equations are a semantic
match when they give the exact same output for the entire range of inputs. If
the recovered equation has certain inaccuracies, such as floating point errors
in constant values, this definition is violated. In that case, the floating
point values are approximately matched with some tolerance. However, the
equations need to have the same structure, otherwise the constants cannot be
paired correctly for approximate matching. This may lead to false negatives
when the recovered equation is a semantic match upto the floating point
tolerance, but does not have the same structure. The results show high
accuracy, so the false negatives are not a major concern.

Execution time is measured individually for the parameter analysis, symbolic
execution, and simplification stages.

Human friendliness. An equation may be considered human-friendly if its
complexity is similar to the original equation, based on its appearance.
Evaluating the complexity of a math equation is subjective and cannot be
precisely measured. So determining whether an equation is fully simplified is
not feasible. A heuristic measure of complexity is defined by the number of
operations in the math equation. The sympy.count_ops function measures the
number of operations in an equation. If the reverse-engineered equation has a
similar number of operations as the original one, we consider them to have
comparable complexity. We quantify human-friendliness as the ratio of the
number of operations, with a ratio closer to 1 indicating more human-
friendliness.

###  6.1 Dataset Generation

Assessing accuracy can be performed with executables for which the original
math equation is known. For this, we generate a dataset of random math
equations. For each generated equation, we create a C function and a Simulink
[19] model. The C function is compiled into an ARM32-HF target executable
using the LLVM clang compiler [24]. The Simulink model is compiled for the
same ARM32-HF target using Simulink’s code generation feature. Both
compilations use the ”-O2” level of optimization. This approach provides a
dataset with the math equation and two distinct binary implementations.

To facilitate direct conversion to Simulink models, which are computational
graphs, the math equations are generated as directed-acyclic graphs (DAG),
where each node is a parameter or a math operation. The required number of
input nodes are initialized first. Then, math operation nodes are picked from
a pool of operations, with repeats allowed. Edges are randomly added between
the nodes to connect the entire graph, while ensuring that no cycles are
created and the graph stays as a DAG. Finally, nodes with no outgoing edge are
connected by inserting add or multiply operation nodes to get to one output.
This final step ensures there are no ”dead” operations (node with no outgoing
edges, essentially wasted computation which does not reach any output).

This approach contrasts with approaches in [32, 16] to randomly generate math
equations which generate expression trees instead of DAGs. Generating
expression trees helps control the complexity of the random equation. This is
important for the two papers as their analysis is based on machine learning
and can handle a finite amount of tokens. Our simplification stage is rule-
based and does not have this limitation. Hence, generating longer and complex
equations is desirable. In our assessment, DAGs offer two advantages: (1) they
can be converted into Simulink models and (2) they generate complex equations
in terms of number of operations.

A textual representation of the math equation is derived by performing an in-
order traversal of the generated DAG. For the C function, a standalone C file
is produced using a template, which is then populated with the equation’s C
implementation. For the Simulink model, the DAG nodes and edges correspond
directly to Simulink blocks and lines. The Simulink model is generated as a
“.mdl” file from a template that includes the necessary code generation and
build parameters, with the block and line details filled in. Each generated
equation is simplified by REMaQE simplification algorithm of Sympy. The
equation is marked invalid and discarded if the simplification either reduces
to a constant, contains complex or infinite values, or cancels out one of the
inputs. The valid equations and their corresponding compiled binaries form the
dataset. Each model in the dataset has a generated equation, a simplified
ground-truth equation, a binary compiled from the C code, and a binary
compiled by Simulink.

Table 2 shows the parameters available for random DAG generation. All the
different combinations of the parameters are used for generation so that the
dataset has a wide variety of equations for evaluation. Selecting number of
nodes up to 20 is enough to create equations with 100s of operations, and this
increase is due to the random connections in the DAG.

Table 2: Parameters for random DAG generation and options available for each parameter. Parameter | Options
---|---
Type of operations | Arithmetic, Trigonometric, Exponential
Number of inputs | 1,2
Number of nodes | 5, 10, 15, 20

###  6.2 Results

####  6.2.1 Accuracy

Table 3: Accuracy of REMaQE across different generation and implementation parameters. Operations | I/P | Implementation | Models | Recovered | Matched
---|---|---|---|---|---
Arith | 1 | C | 4063 | 4063 | 100% | 3972 | 97.76%
Simulink | 4063 | 4063 | 100% | 4030 | 99.19%
2 | C | 3011 | 3011 | 100% | 2954 | 98.11%
Simulink | 3011 | 3011 | 100% | 2991 | 99.34%
Arith, Trig, Exp. | 1 | C | 1574 | 1574 | 100% | 1541 | 97.9%
Simulink | 1574 | 1455 | 92.44% | 1424 | 90.47%
2 | C | 1177 | 1177 | 100% | 1158 | 98.39%
Simulink | 1177 | 1101 | 93.54% | 1095 | 93.03%
Total |  |  | 19650 | 19455 | 99.01% | 19165 | 97.53%

(a) Generated nodes

(b) Operations in generated equation

(c) Operations in simplified ground-truth equation

Figure 4: % of models categorized by their outcomes (semantic match, failed to
match, or failed to recover) based on (a) generated blocks, (b) operations in
generated expression, and (c) operations in simplified expression.

Table 3 shows the accuracy of REMaQE across different generated parameters and
the C and Simulink implementations. The accuracy is tabulated in stages as (1)
recovered when REMaQE generates a symbolic ET and simplifies it to a math
equation and (2) matched when the recovered equation is a semantic match of
the simplified ground-truth equation. Between these we indicate the level of
reverse engineering as only a recovered equation can be semantically matched.

REMaQE reverse engineers a variety of equations. The recovery percentage of
99.01% is high, with most cases showing 100% recovery. The models with
trigonometric and exponential operations compiled for Simulink show a dip.
This is because Simulink adds bounds checks for inputs of certain
trigonometric functions like sin-1 and cos-1. REMaQE fails to simplify the
complex ET generated for these bounds checks. The 97.53% matched percentage
demonstrates the success of the REMaQE framework in retrieving precise
mathematical equations. Comparable reductions are observed for Simulink’s
trigonometric and exponential models, which, however, fail in recovery.

In Table 3, models with different numbers of nodes or operations are grouped
and a common accuracy result is reported. The histograms in Figure 4 analyze
REMaQE’s accuracy concerning the number of nodes and operations in the
generated equations. Nodes directly correlate with Simulink blocks or C code,
subsequently with computation instructions in the binary. Generated equation
operations correspond to symbolic ET operations extracted during the symbolic
execution stage. After the simplification stage, the recovered equation is
comparable to the simplified ground-truth equation in number of operations.
Both the recovery rate (semantic match + matching failed) and the matching
rate slightly decrease with increasing nodes or operations, but are not
correlated at higher numbers. This indicates that REMaQE recovers semantically
correct equations equally well across various equation complexities. Figure
4(a) shows a higher success rate for the last three bars because there are few
models with 20 or more nodes, which skews recovery and matching rates.

####  6.2.2 Semantic matching

Examination of models that fail to match reveals that most of them have
constant parameters not accurately identified by REMaQE, thus not converted to
constant symbols. This occurs when constants are hard-coded as immediate
values in instructions instead of being loaded from memory. Constant values
may experience minor changes due to floating-point representation and rounding
errors, resulting in a semantic mismatch between the ground-truth and
recovered equation. REMaQE’s parameter analysis can be expanded to identify
these constants and substitute them with constant symbols during symbolic
execution.

Recovered equations are matched with the ground-truth at three levels.
Structural match is when they have the same order of operations and variables.
This is checked by comparing Sympy’s internal tree representation of both
equations. Semantic match is when they are mathematically equivalent, but do
not have the same structure. This is checked by taking the difference of both
equations and running Sympy’s simplification to see if they cancel out to
zero. Approximate match is when they have the same structure but differ in
certain constant values due to floating point errors. Again, the tree is
compared, but constants are matched approximately using a tolerance of
$10^{-7}$. Table 4 gives examples of the three levels of matching, along with
a failure case. In example 1, the equations are exactly same. In example 2,
the recovered equation has an extra constant $k_{2}$, whose value is 0, which
changes the structure of the equation. Substituting $k_{2}=0$ and simplifying
the difference gives zero. In example 3, the constant value 8.61 shows a
floating point error in the recovered equation, but the equation structure is
the same. In example 4, the equations are matched. However, the division by
$3.5$ in ground-truth has changed to multiplication with $0.3076923$, which is
an approximation of $1/3.5$. Even though these equations should be an
approximate match, the structure has changed, hence matching fails. However,
it is seen that the recovered expression does indeed correctly correspond to
ground truth; hence, the numbers for % Matched in Table 3 are underestimates
and REMaQE’s actual accuracy can be even better than the numbers in Table 3.

Table 4: Examples to demonstrate the different levels of equation matching. | Match | Ground truth | Recovered
---|---|---|---
1 | Structural | $k_{0}-k_{2}\left(k_{0}+k_{1}+x_{0}-\sin{\left(k_{0}+x_{0}\right)}\right)+k_{3}+x_{0}$ | $k_{0}-k_{2}\left(k_{0}+k_{1}+x_{0}-\sin{\left(k_{0}+x_{0}\right)}\right)+k_{3}+x_{0}$
2 | Semantic | $\frac{\left(-k_{0}x_{0}\left(k_{1}+1\right)-2x_{1}\right)\tan{\left(k_{1}x_{0}\right)}}{x_{0}\left(k_{1}+1\right)}$ | $\frac{\left(-k_{2}-k_{0}\left(k_{2}+k_{1}x_{0}+x_{0}\right)-2x_{1}\right)\tan{\left(k_{1}x_{0}\right)}}{k_{2}+k_{1}x_{0}+x_{0}}$
3 | Approx. | $-k_{1}-k_{2}(k_{3}+8.61(k_{0}-x_{0}))$ | $-k_{1}-k_{2}(k_{3}+8.609999656677246(k_{0}-x_{0}))$
4 | Fail | $\frac{-3.25k_{0}}{x_{0}}+\frac{x_{0}x_{1}}{3.25}$ | $\frac{-3.25k_{0}}{x_{0}}+0.3076923{x_{0}x_{1}}$
Table 5: Average execution time (seconds) of REMaQE stages across different generation parameters. Majority of the execution time is spent on simplification, while the rest is split between parameter analysis and symbolic execution. Average execution time is less than 0.25 seconds, which means REMaQE is capable of reverse engineering in real time. Operations | I/P | Implementation | Parameter analysis | Symbolic execution | Simplifcation | Total
---|---|---|---|---|---|---
Arith | 1 | C | 0.017 | 6.8% | 0.013 | 5.0% | 0.224 | 88.2% | 0.254
Simulink | 0.049 | 18.3% | 0.040 | 15.1% | 0.178 | 66.6% | 0.267
2 | C | 0.018 | 7.9% | 0.013 | 5.8% | 0.198 | 86.2% | 0.229
Simulink | 0.053 | 21.0% | 0.042 | 16.8% | 0.159 | 62.3% | 0.255
Arith, Trig, Exp. | 1 | C | 0.038 | 27.7% | 0.030 | 21.7% | 0.069 | 50.6% | 0.136
Simulink | 0.096 | 30.3% | 0.135 | 42.4% | 0.086 | 27.2% | 0.318
2 | C | 0.037 | 23.3% | 0.029 | 18.3% | 0.094 | 58.4% | 0.161
Simulink | 0.078 | 28.9% | 0.089 | 33.0% | 0.102 | 38.1% | 0.269
Average |  |  | 0.042 | 17.3% | 0.040 | 16.3% | 0.162 | 66.4% | 0.244

####  6.2.3 Execution Time

Execution time of each of REMaQE’s three stages is measured for the generated
dataset on an Intel® Core™ i7-8665U CPU. Only one instance of REMaQE is run on
a single core to collect the timing measurements. Table 5 shows the execution
time of the stages across the different generation parameters. On average, the
full reverse engineering takes less than 250ms, of which 66% is consumed by
the simplification stage and the rest is equally split between parameter
analysis and symbolic execution. Almost all of the simplification time is
consumed by Sympy. Simulink implementations take longer for parameter analysis
and symbolic execution, but complete simplification in similar or lesser time.
This is because the Simulink implementation relies on global memory access,
which may take longer to simulate in symbolic frameworks, but generates a
similar or less complex ET for the simplification stage.

Figure 6 displays how execution time changes with number of nodes in the
generated model. Execution time for parameter analysis and symbolic execution
increases linearly with number of nodes, whereas time for simplification
increases exponentially. This is expected as Sympy’s simplification tries
known transformation rules for many combinations of operations in the
equation. The total execution time ranges from 0.15s to 1.3s across different
number of nodes. Overall, REMaQE completes reverse engineering over a wide
range of equations in real time. This makes it suitable as an interactive tool
that can easily integrate with a GUI-based reverse engineering workflow and
deliver recovered equations effectively at latencies comparable to human click
speeds.

Figure 5: Average execution time in seconds per stage binned by number of
nodes.

Figure 6: Average ratio of equation complexity binned with the number of
operations in the simplified ground-truth equation. The box indicates
$\mu\pm\sigma$ ($\mu$ is mean, $\sigma$ is standard deviation), while the line
and whiskers indicate range.

####  6.2.4 Human-friendliness

Figure 6 demonstrates the human-friendliness of reverse engineered outputs of
REMaQE. The successfully recovered models are evaluated for equation
complexity in terms of number of operations. The average ratio of number of
operations in the recovered equation over the simplified ground-truth equation
is plot as a histogram. Standard deviation and range of each bin is displayed
as the box and whiskers plot. The average ratio is very close to 1 across the
range of equation complexity, with a tight standard deviation of 0.15,
demonstrating that REMaQE performs well on the human-friendliness metric for a
variety of equations. The high maximum ratios indicate there are some outliers
where REMaQE recovers a more complex equation. The maximum is larger for the
lower bins. Algebraic simplification cannot shrink the recovered equation
beyond a point. But the ground-truth equation is simpler for the lower bins,
hence the ratio grows larger. The minimum is close to 0.5 throughout. These
outliers exist because the C and Simulink compilers optimize the
implementation, sometimes more than what Sympy can achieve. The recovered
equation ends up being less complex than the ground-truth.

##  7 Case Study: SVM classifier

We assess the reverse engineering of a Support-Vector-Machine (SVM) classifier
implemented in C and compiled for the ARM32-HF target using the REMaQE
framework. Figure 8 displays the pertinent C++ class and global variables.
Within the executable, symbols are retained to preserve original function
names, and although global variable names are accessible, their presence is
not assumed. Analysis for a stripped executable means function names must be
inferred manually.

⬇

1typedef struct { float x; float y;} Point;

2Point sv[3] = {

3 {1.2f, 2.3f}, {5.4f, -3.6f}, {-7.2f, -2.0f}};

4float a[3] = {2.7f, 3.1f, 1.4f};

5float y[3] = {1.0f, -1.0f, -1.0f};

6float s = 25.6f, b = 0.4f;

7

8float thresh(float x) {

9 return x > 0 ? 1.0f : -1.0f;

10}

11

12class SVM {

13public:

14 float kernel(Point p1, Point p2) {

15 float d = powf((p1.x - p2.x), 2)

16 + powf((p1.y - p2.y), 2);

17 return expf(-d/s);

18 }

19

20 float classify(Point p) {

21 float f = 0;

22 for (int i=0; i<3; i++) {

23 float k = kernel(p, sv[i]);

24 f += a[i] * y[i] * k;

25 }

26 f += b;

27 return thresh(f);

28 }

29};

Figure 7: Snippets of the C++ code implementing an SVM classifier.

Figure 8: Callgraph extracted for the SVM classifier binary.

We start by extracting the callgraph of the executable starting from the main
function. The callgraph is shown in Figure 8. We see the three functions of
interest, SVM::classify, SVM::kernel, and thresh. Note that expf is the math
library function to compute exponential. We start reverse engineering the
inner-most functions (SVM::kernel, thresh) first, then move to SVM::classify.

Table 8 shows the parameter metadata for the SVM::kernel function. Equation 3
show the equation obtained for output $y_{0}$. The equation computes the
Gaussian function $e^{-x^{2}/\sigma^{2}}$. The numerator of the exponent
resemble the formula for Euclidian distance squared,
$(a_{x}-b_{x})^{2}+(a_{y}-b_{y})^{2}$, for two points $(a_{x},a_{y})$ and
$(b_{x},b_{y})$. That is, the four inputs correspond to $(x,y)$ co-ordinates
of two points and $k_{0}=\sigma^{2}$. Thus, the SVM classifier uses a Gaussian
kernel. The classifier works on 2D points as the kernel function takes 2D
input. We obtain the value for $\sigma$ from the identified constants.

Table 6: Parameters of thresh.

I/P | Kind | Location
---|---|---
$x_{0}$ | reg | s0
O/P | Kind | Location
$y_{0}$ | reg | s0

Table 7: Parameters of SVM::kernel.

I/P | Kind | Location
---|---|---
$x_{0}$ | reg | s0
$x_{1}$ | reg | s1
$x_{2}$ | reg | s2
$x_{3}$ | reg | s3
O/P | Kind | Location
$y_{0}$ | reg | s0

Const | Kind | Location | Val
---|---|---|---
$k_{0}$ | global | 0x408fc | 25.6

Table 8: Parameters of SVM::classify.

I/P | Kind | Location
---|---|---
$x_{0}$ | reg | s0
$x_{1}$ | reg | s1
O/P | Kind | Location
$y_{0}$ | reg | s0
$y_{1}$ | stack | stack[0x4]
… |  |

Const | Kind | Location | Value
---|---|---|---
$k_{0}$ | global | 0x206d0 | 0
$k_{1}$ | global | 0x408cc | 1.2
$k_{2}$ | global | 0x408d0 | 2.3
$k_{3}$ | global | 0x408d4 | 5.4
$k_{4}$ | global | 0x408d8 | -3.6
$k_{5}$ | global | 0x408dc | -7.2
… |  |  |

$y_{0}=\operatorname{exp}\left({\frac{-\left(x_{0}-x_{2}\right)^{2}-\left(x_{1}-x_{3}\right)^{2}}{k_{0}}}\right)$
(3)

Table 8 shows the parameter metadata for thresh function. Equation 4 shows the
equation obtained for output $y_{0}$. Conditional ET generated after symbolic
execution is shown in Figure 9. REMaQE simplifies it to a piecewise
representation using a single comparison. thresh function discretizes the
input to $\\{1.0,-1.0\\}$ with a threshold of $0$, indicating this is an SVM
binary classifier.

$y_{0}=\begin{cases}-1.0&\text{for}\>x_{0}<0\\\
1.0&\text{otherwise}\end{cases}$ (4)

⬇

<FP32 if 1 + (0 .. 0xffffffff + ((if <...> then <...> else <...>) .. ~<...> .. 0x0)[31:29]) + 15 * ~(~(<...> | <...>) | (7 .. ~<...>) | 14)[2:2] == 1 || !(1 + (0 .. <...> + <...>[31:29]) + 15 * ~(<...> | <...> | <...>)[3:3] == 1 == (0xffffffff + ((if <...> || <...> then 0 else 1) .. ~(if <...> then <...> else <...>) .. 0x0)[29:29] == ~(~(if fpLT(<...>, <...>) then 1 else (if <...> then <...> else <...>)) | ~(if <...> || <...> then 0 else 1)))) then FPV(-1.0, FLOAT) else FPV(1.0, FLOAT)>

Figure 9: The conditional ET generated after symbolic execution of the thresh
function. The expression has been truncated using placeholders (<...>) for
brevity.

Once the two inner functions SVM::kernel and thresh are reverse engineered,
REMaQE creates hooks which trigger when the functions are called during
subsequent symbolic execution, and return the obtained equation directly
without executing. The SVM::classify function can now be reverse engineered.
Table 8 shows the parameter metadata for the SVM::classify function. REMaQE
identifies several outputs located on the stack, although they are not
actually function outputs but callee-saved registers which are spilled to the
stack. However, the actual output in register s0 is correctly identified.
Equation 5 shows the equation obtained for this output $y_{0}$.

$y_{0}=\operatorname{thresh}(k_{13}+k_{0}+k_{10}k_{7}\operatorname{kernel}{\left(x_{0},x_{1},k_{1},k_{2}\right)}\\\
+k_{11}k_{8}\operatorname{kernel}{\left(x_{0},x_{1},k_{3},k_{4}\right)}+k_{12}k_{9}\operatorname{kernel}{\left(x_{0},x_{1},k_{5},k_{6}\right)})$
(5)

In the equation, the function calls to SVM::kernel and thresh are shown with
the appropriate arguments included. Based on our understanding of the
SVM::kernel function, inputs $(x_{0},x_{1})$, and constant pairs
$(k_{1},k_{2}),(k_{3},k_{4}),(k_{5},k_{6})$ are 2D points. These constant
pairs represent the support vectors for the given SVM, while the inputs
symbolize a point being classified by the SVM. The original source code
contains a for-loop to iterate over all support vectors; however, this loop
has been unfolded in the equation. This is due to symbolic execution carrying
out all loop iterations during its exploration process, which results in a
single expression tree (ET) that incorporates the operations from each
iteration.

##  8 Conclusion

This paper presents REMaQE, a framework for automatically reverse engineering
mathematical equations from executables. It consists of three main stages:
parameter analysis, symbolic execution, and algebraic simplification.
Parameter analysis allows REMaQE to identify whether input, output and
constant parameters of the math equation are stored in the register, on the
stack, in global memory or accessed via pointers. REMaQE effectively uses this
metadata to reverse engineer a wide variety of implementations, such as C++
classes that use class pointers, or Simulink compiled binaries that use global
memory. This is a significant improvement over existing approaches that only
handle simple functions implemented using registers. Algebraic simplification
allows REMaQE to simplify complex conditional expressions involving floating-
point comparisons, that are frequently generated by symbolic execution even
for simple equations. Existing approaches are limited in this regard as they
rely on machine learning models that have limits on the input expression size,
thus cannot handle the long complex expressions generated by conditional
computations.

Additionally, the paper introduces an alternative method for randomly
generating diverse equations using directed acyclic graphs. REMaQE
demonstrates high accuracy of 97.53% on the generated dataset. Accuracy is
consistently over 94% even for the most complex equations, indicating that
REMaQE handles various equation complexities effectively. REMaQE achieves an
average execution time of 0.25 seconds and increases only to as high as 1.3
seconds for the most complex equations. Such a small reverse engineering time
makes REMaQE effective for a highly interactive reverse engineering workflow,
and would demonstrate one-click latency when integrated with GUI frameworks.
When comparing the complexity of the recovered equations with the original
equations, REMaQE shows an average ratio of 1 through a range of equation
complexities, with a standard deviation of 0.15. Thus, REMaQE can extract
human-friendly equations from binary executables.

Future work involves extending REMaQE to integrate it into existing GUI
decompilation tools, support various datatypes, handle datatype conversions,
and enhance reverse engineering capabilities to recognize advanced
mathematical structures for improved representation. Integration with GUI
tools will yield a better reverse engineering workflow for users compared to
the Python API and the command line interface. Support of datatypes, such as
fixed-point and integer, will increase applicability of REMaQE to more real-
world programs. Once it supports integer and bitwise computations, REMaQE can
also be applied to other domains like reverse engineering of cryptographic
algorithms. In the domain of embedded systems, algorithms can employ advanced
mathematical structures such as dynamic loops, summation, integration,
differentiation, and high dimensional data such as vectors and matrices.
Currently in REMaQE, such structures are unrolled and represented as long
chains of scalar computations, whereas a truly simplified human-friendly
representation should use advanced mathematical operations (e.g., dot product,
matrix multiply) to represent them. These refinements and extensions are the
proposed future work for REMaQE.

## References

  * [1] Cristian Cadar, Daniel Dunbar, and Dawson Engler.  KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs.  In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI), page 209–224, USA, 2008. USENIX Association.
  * [2] Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley.  Unleashing mayhem on binary code.  In IEEE Symposium on Security and Privacy, pages 380–394, USA, 2012\. IEEE.
  * [3] Cristina Cifuentes.  Reverse compilation techniques.  PhD thesis, Queensland University of Technology, Brisbane, 1994.
  * [4] International Electrotechnical Commission.  Iec 61131-3:2013.  https://webstore.iec.ch/publication/4552, 2013.  Accessed: 2023-03-22.
  * [5] Robin David, Sébastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, and Jean-Yves Marion.  BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis.  In IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER), volume 1, pages 653–656, Japan, 2016. IEEE.
  * [6] NSA Research Directorate.  Ghidra.  https://ghidra-sre.org/, 2023.  Accessed: 2023-03-22.
  * [7] Internation Organization for Standardization (ISO) and International Electrotechnical Commision (IEC).  ISO/IEC 9899:TC3.  https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf, 2023\.  Accessed: 2023-03-22.
  * [8] Hex-Rays.  Ida pro disassembler.  https://hex-rays.com/ida-pro/, 2023.  Accessed: 2023-03-22.
  * [9] R. N. Horspool and N. Marovac.  An Approach to the Problem of Detranslation of Computer Programs.  The Computer Journal, 23(3):223–229, 1980.
  * [10] Sushma Kalle, Nehal Ameen, Hyunguk Yoo, and Irfan Ahmed.  Clik on plcs! attacking control logic with decompilation and virtual plc.  In Workshop on Binary Analysis Research (BAR), USA, 2019. The Internet Society.
  * [11] A. Keliris and M. Maniatakos.  ICSREF: A framework for automated reverse engineering of industrial control systems binaries.  In Network and Distributed System Security Symposium (NDSS), USA, 2019. The Internet Society.
  * [12] Farshad Khorrami, Prashanth Krishnamurthy, and Ramesh Karri.  Cybersecurity for control systems: A process-aware perspective.  IEEE Design & Test, 33(5):75–83, 2016.
  * [13] Taegyu Kim, Aolin Ding, Sriharsha Etigowni, Pengfei Sun, Jizhou Chen, Luis Garcia, Saman Zonouz, Dongyan Xu, and Dave (Jing) Tian.  Reverse engineering and retrofitting robotic aerial vehicle control firmware using DisPatch.  In Proceedings of the 20th Annual International Conference on Mobile Systems, Applications and Services (MobiSys), page 69–83, USA, 2022\. ACM.
  * [14] Charalambos Konstantinou, Michail Maniatakos, Fareena Saqib, Shiyan Hu, Jim Plusquellic, and Yier Jin.  Cyber-physical systems: A security perspective.  In IEEE European Test Symposium (ETS), pages 1–8, USA, 2015. IEEE.
  * [15] Prashanth Krishnamurthy, Farshad Khorrami, Ramesh Karri, David Paul-Pena, and Hossein Salehghaffari.  Process-aware covert channels using physical instrumentation in cyber-physical systems.  IEEE Transactions on Information Forensics and Security, 13(11):2761–2771, 2018.
  * [16] Guillaume Lample and François Charton.  Deep learning for symbolic mathematics.  In International Conference on Learning Representations (ICLR), 2020\.
  * [17] Ralph Langner.  Stuxnet: Dissecting a cyberwarfare weapon.  IEEE Security & Privacy, 9(3):49–51, 2011.
  * [18] Xuefeng Lv, Yaobin Xie, Xiaodong Zhu, and Lu Ren.  A technique for bytecode decompilation of plc program.  In 2017 IEEE 2nd Advanced Information Technology, Electronic and Automation Control Conference (IAEAC), pages 252–257, USA, 2017. IEEE.
  * [19] MathWorks.  Simulink - Simulation and Model-based Design.  https://www.mathworks.com/products/simulink.html, 2023.  Accessed: 2023-03-22.
  * [20] E. J. McCluskey Jr.  Minimization of boolean functions.  The Bell System Technical Journal, 35(6):1417–1444, 1956.
  * [21] Stephen McLaughlin, Saman Zonouz, Devin Pohly, and Patrick McDaniel.  A trusted safety verifier for process controller code.  In Network and Distributed System Security Symposium (NDSS), USA, 2014. The Internet Society.
  * [22] Stephen E. McLaughlin.  On dynamic malware payloads aimed at programmable logic controllers.  In Proceedings of the 6th USENIX conference on Hot topics in security, USA, 2011. ACM.
  * [23] Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B. Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, Štěpán Roučka, Ashutosh Saboo, Isuru Fernando, Sumith Kulal, Robert Cimrman, and Anthony Scopatz.  Sympy: symbolic computing in python.  PeerJ Computer Science, 3:e103, 2017.
  * [24] The LLVM Project.  LLVM Clang C Compiler.  https://clang.llvm.org/, 2023.  Accessed: 2023-03-22.
  * [25] Syed Ali Qasim, Juan Lopez, and Irfan Ahmed.  Automated reconstruction of control logic for programmable logic controller forensics.  In Zhiqiang Lin, Charalampos Papamanthou, and Michalis Polychronakis, editors, Information Security, pages 402–422, Cham, 2019. Springer International Publishing.
  * [26] W. V. Quine.  The problem of simplifying truth functions.  The American Mathematical Monthly, 59:521–531, 1952.
  * [27] Tim Conway Robert M. Lee, Michael J. Assante.  Analysis of the cyber attack on the ukrainian power grid.  https://media.kasperskycontenthub.com/wp-content/uploads/sites/43/2016/05/20081514/E-ISAC_SANS_Ukraine_DUC_5.pdf, 2016\.
  * [28] Yan Shoshitaishvili, Ruoyu Wang, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna.  Firmalice - automatic detection of authentication bypass vulnerabilities in binary firmware.  In Network and Distributed System Security Symposium (NDSS), USA, 2015. The Internet Society.
  * [29] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna.  SOK: (state of) the art of war: Offensive techniques in binary analysis.  In 2016 IEEE Symposium on Security and Privacy (SP), pages 138–157, USA, 2016. IEEE.
  * [30] Nick Stephens, Jessie Grosen, Christopher Salls, Audrey Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna.  Driller: Augmenting fuzzing through selective symbolic execution.  In Network and Distributed System Security Symposium (NDSS), USA, 2016. The Internet Society.
  * [31] Pengfei Sun, Luis Garcia, and Saman Zonouz.  Tell me more than just assembly! reversing cyber-physical execution semantics of embedded iot controller software binaries.  In IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pages 349–361, USA, 2019. IEEE.
  * [32] Nicolaas Weideman, Virginia K. Felkner, Wei-Cheng Wu, Jonathan May, Christophe Hauser, and Luis Garcia.  PERFUME: Programmatic extraction and refinement for usability of mathematical expression.  In Research on Offensive and Defensive Techniques in the Context of Man At The End (MATE) Attacks (Checkmate), page 59–69, USA, 2021. ACM.
  * [33] Wikipedia.  Aurora generator test.  https://en.wikipedia.org/wiki/Aurora_Generator_Test, 2007.  Accessed 2023-03-22.
  * [34] Zeyu Yang, Liang He, Hua Yu, Chengcheng Zhao, Peng Cheng, and Jiming Chen.  Detecting plc intrusions using control invariants.  IEEE Internet of Things Journal, 9(12):9934–9947, 2022.