Binary Program

Definition

A binary program is a software program in its compiled, machine-code representation, consisting of processor instructions targeted at a specific instruction set architecture (ISA). In the µARCHIFI workflow, a binary program is one of the three primary inputs supplied alongside a hardware description (in Verilog) and an attacker model specifying the fault model [chunk: cc0353b3; chunk: e2d812bc]. The program must be compiled for the corresponding ISA of the processor under analysis so that its machine instructions can be symbolically interpreted against the hardware transition system [chunk: cc0353b3].

Role in Microarchitectural Fault-Injection Verification

Binary programs are analyzed by µARCHIFI to determine whether injected microarchitectural faults can induce a different system behavior that an attacker can exploit [chunk: 9f8e2ccc; chunk: e2d812bc]. The tool generates a formal transition system from the hardware design, the binary program, and the attacker model, and uses bounded model checking (BMC) to verify reachability of an attacker goal φ [chunk: e2d812bc].

Reported use cases exercise binary programs of varying complexity, including:

• VerifyPIN compiled with -Og and -Os for authentication-bypass analysis on CV32E40P and Secure Ibex cores [chunk: cc0353b3].
• KeySchedule (AES) compiled with -Os for analysis of expanded-key manipulation on the Ibex core [chunk: cc0353b3].

The reported µARCHIFI case studies encompass binary programs of hundreds of machine instructions running on complete microarchitectural designs of RISC-V processors representative of the embedded market [chunk: 9f8e2ccc].

Software-Level Fault Effects

Some research models and studies faults at the software level and analyzes fault effects on the control flow of binary programs [chunk: 9f8e2ccc]. Pure software analysis, however, struggles to model many subtle behavioral effects induced by fault injection; this motivates joint hardware/software analyses that incorporate the binary program as a first-class input [chunk: e2d812bc].

Binary Programs as Engineered Stimuli for PBIST (FTBE)

Beyond formal verification, binary programs can be specially engineered to act as periodic test stimuli that exercise processor internals and provoke hard-to-reach faults within low-latency windows. This role is explored in the context of a hardware Periodic Built-In-Self-Test (PBIST) countermeasure for a RISC-V microprocessor (the Potato SoC), where a binary program is stored in a BRAM-based emulated ROM and is used together with a small set of strategically placed node-monitoring counters [chunk: 31f5a067; chunk: fe5b92d1; chunk: 30985565].

The Fault Trigger Binary Executable (FTBE) is defined as a minimized set of instructions designed to recreate a processor state that leads to information leakage in the presence of a fault with minimal latency. Two FTBE generation strategies are described:

• Run-Cycle-Based FTBE (RCBE) — uses existing counter-based node-monitoring infrastructure to identify the run cycle in which faults become observable while a cryptography algorithm is executing, then crafts a binary that recreates the microprocessor state at that cycle [chunk: 30985565; chunk: fe5b92d1].
• ATPG-Based FTBE (ATPGB) — uses an Automatic Test Pattern Generation (ATPG) flow to produce high-coverage test vectors, which are then coerced into closely matched processor instructions and register-file values to form a coherent binary program [chunk: 30985565; chunk: fe5b92d1; chunk: fe5b92d1].

Because the resulting FTBE must be stored in on-chip memory for periodic execution, minimizing the binary size (e.g., to less than 100 instructions) is an important design goal [chunk: fe5b92d1]. The execution of an AES binary on the Potato platform spans 6,717,440 clock cycles, providing the baseline against which FTBE latency is measured [chunk: 30985565].

Reported effectiveness of these engineered binaries (against the SevereFaults class of information-leakage faults) is summarized below:

• The RCBE methodology produced three binaries (B0, B1, B2) generated from IFTCs 6,076,072; 1,728,512; and 550,800 respectively; B0 triggers nine faults, B1 triggers 113 faults, and B2 triggers the remaining 122 faults [chunk: cced7a1c].
• The ATPGB binary requires fewer instructions and has lower memory overhead than the RCBE, but detects fewer SevereFaults (188 in total) [chunk: cced7a1c].
• The Coremarks binary requires the most instructions in total and triggers 191 SevereFaults throughout a full program run [chunk: cced7a1c].
• A "hello world" binary, included as a baseline, has the smallest instruction count but only triggers one SevereFault [chunk: cced7a1c].

In terms of latency, the RCBE detects all SevereFaults within 4096 run clock cycles, and the ATPGB triggers 188 faults by the 4096-cycle index — substantially outperforming standard binaries, where severe faults can have latencies as high as 6 million cycles [chunk: cced7a1c; chunk: 30985565]. Combining multiple RCBEs into a single contiguous binary is achieved by overwriting registers that differ between binaries and then updating the corresponding instructions [chunk: cced7a1c].

The test harness uses the Processor Configuration Access Port (PCAP) interface to configure the FPGA fabric with an instrumented bitstream, and a side-load architecture (ERSE) overrides boot-memory locations with the executable binary under test [chunk: 30985565].

Binary Similarity Analysis

Binary programs are also the subject of binary similarity analysis, which determines whether two binary executables originate from the same source program. The PEM approach represents binary program semantics through a probabilistic execution engine that samples both the input space and the program-path space, achieving 96% precision on an evaluation spanning 9 real-world projects and 35k functions [arxiv:2308.15449v2].

Cryptographic Primitive Detection

Compiled binary programs are routinely analyzed to detect and classify cryptographic algorithms, an application motivated by malware that uses cryptography to disguise its actions. Machine-learning approaches have been demonstrated to successfully detect and identify cryptographic primitives in small single-purpose compiled binary programs [arxiv:1503.01186v1].

Tooling Considerations

In µARCHIFI, the verification complexity — and therefore the tractable size of the binary program under analysis — is governed by a trade-off between the size of the hardware design, the size of the analyzed program, and the complexity of the fault model; the user must find a "sweet spot" among these dimensions [chunk: 9f8e2ccc].

See Also

• µARCHIFI — formal fault-injection verification tool that consumes binary programs as input.
• FTBE (Fault Trigger Binary Executable) — specialized low-instruction-count binary designed to provoke hard-to-reach faults for PBIST.
• PBIST (Periodic Built-In-Self-Test) — countermeasure framework in which engineered binaries are periodically executed to detect information-leakage faults.