Skip to main content
warning

The plugin presented in this tutorial is still in development.

Fault injection

Fault injection is an attack technique that physically perturbs the executing hardware — using methods such as clock or power glitches, or laser pulses — to alter program execution behavior. Through these perturbations, an attacker can bypass security mechanisms in otherwise defect-free software.

In this tutorial, we will use BINSEC's Adversarial Symbolic Execution (ASE) plugin — following the work by Ducousso et al. — to automatically evaluate the resistance of a PIN verification program against several fault models.

Example program: Verify PIN​

We consider a VerifyPIN program that checks if a number provided by the user is equal to a given secret. The C implementation evaluated is presented below.

verify_pin.c
#define SIZE 4

char secret[SIZE] = { 0xde, 0xad, 0xca, 0xfe };
char buffer[SIZE] = { 0 };

extern void get_pin(); // Load the PIN into the 'buffer'
extern int access_database(); // Do private things

// Verify if PIN is correct
char check() {
  char res = 1;
  for (char i = 0; i < SIZE; ++i)
    res &= buffer[i] == secret[i];
  return res;
}

// A basic function to check PIN
int main(void) {
  get_pin();
  if (check()){
    return access_database();
  }
  fail(1);
}

The main function reads four bytes into buffer, then calls check to verify that they match the secret.
We will use the symbolic engine to simulate user inputs.

How to validate ?

In order to validate the results generated by our faults, we will check if we can access to the function access_database without a valid PIN.

Baseline​

Let us first check, with a plain symbolic execution (without any fault), that reaching access_database is not possible.

We stub the function get_pin with :

  • fill the user PIN buffer with symbolic content
  • assume the given PIN is not equal to the secret PIN
starting from <main>
with concrete stack pointer
load sections .text, .data, .rodata, .plt, .got from file


replace <get_pin>() by
  @[<buffer>, ->, 4] := nondet as user_pin
  assume @[<buffer>,4] <> @[<secret>,4]
  return
end


reach <access_database> then print model
halt at <main> return
Output

BINSEC terminate the execution because its path worklist is empty. He didn't reach the access_database function, whatever the four bytes entered by the user could be.

The behaviour is secure: an attacker cannot make the program accept a wrong pin.

Disassembly of the check function​

We will target the check function, perturbing its behavior to bypass the PIN verification with an invalid PIN.

Let's have a look at its x86_64 disassembly.

Disassembly of check()
0000000000001187 <check>:
    1187:	f3 0f 1e fa          	endbr64
    118b:	55                   	push   %rbp
    118c:	48 89 e5             	mov    %rsp,%rbp
    118f:	c6 45 fe 01          	movb   $0x1,-0x2(%rbp)          # res = 1
    1193:	c6 45 ff 00          	movb   $0x0,-0x1(%rbp)          # loop_counter i = 0
    1197:	eb 34                	jmp    11cd <check+0x46>
    1199:	0f be 45 ff          	movsbl -0x1(%rbp),%eax
    119d:	48 98                	cltq
    119f:	48 8d 15 7e 2e 00 00 	lea    0x2e7e(%rip),%rdx        # 4024 <buffer>
    11a6:	0f b6 14 10          	movzbl (%rax,%rdx,1),%edx
    11aa:	0f be 45 ff          	movsbl -0x1(%rbp),%eax
    11ae:	48 98                	cltq
    11b0:	48 8d 0d 5a 2e 00 00 	lea    0x2e5a(%rip),%rcx        # 4011 <secret>
    11b7:	0f b6 04 08          	movzbl (%rax,%rcx,1),%eax
    11bb:	38 c2                	cmp    %al,%dl
    11bd:	0f 94 c0             	sete   %al
    11c0:	20 45 fe             	and    %al,-0x2(%rbp)           # res &= buffer[i] == secret[i]
    11c3:	0f b6 45 ff          	movzbl -0x1(%rbp),%eax
    11c7:	83 c0 01             	add    $0x1,%eax
    11ca:	88 45 ff             	mov    %al,-0x1(%rbp)           # i+=1
    11cd:	80 7d ff 03          	cmpb   $0x3,-0x1(%rbp)          # loop test
    11d1:	7e c6                	jle    1199 <check+0x12>        # conditional jump to loop body
    11d3:	0f b6 45 fe          	movzbl -0x2(%rbp),%eax
    11d7:	5d                   	pop    %rbp
    11d8:	c3                   	ret

Test Inversion fault model​

What if we could invert the conditional branch? The Test Inversion fault model flips the branch's condition to alter execution flow.

To run the ASE plugin, the following parameters must be configured:

To apply the ASE plugin, you need to specify parameters :

  • target-addresses defines the instruction window that can be faulted (here we will set the target addresses using the values identified during the disassembly step);
  • fault-model specifies the attack strategy (here, the Test Inversion fault model).
  target-addresses = 0x1187, 0x11d8
  fault-model = TestInversionIte


  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
  @[<buffer>, -> ,4] := nondet as user_pin
  assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

BINSEC returns a model.
--- Model ---
# Variables
user_pin!2 : 0x33e4c37d
__b_test_0x0011d1_!4 : 0b1

The first entry gives a successfully validated PIN (33 e4 c3 7d), while the second entry specifies the target branch address that has been faulted by the attack.

Fault model

A fault model provides a formal specification of an adversary's capabilities regarding state and computation perturbation. By bounding the attacker's power, it enables both vulnerability analysis and countermeasure evaluation.

Such models span multiple parameters in computer science, including spatial location, timing, power levels, and control flow alteration. Adapting these abstractions ensures comprehensive coverage across diverse attack scenarios.

Within this context, the BINSEC plugin targets binary-level fault injection and offers automated assessment of countermeasure robustness. The ASE plugin comes with a preset of fault models to streamline this evaluation process.

Software Protection​

We can now introduce a basic software-based countermeasure to the previous implementation by verifying the PIN twice. If the two checks yield different results, a fault is detected and the PIN is rejected.

verify_pin_strong.c
int main(void) {
	get_pin();
	char first_check = check();
	char second_check = first_check ^ check();
	if (first_check && !second_check){
		access_database();
	}
	fail(1);
}

Under our previous single-fault Test Inversion model, this double-check mechanism successfully secures the program.

  target-addresses = 0x1187, 0x11d8
  fault-model = TestInversionIte
  max-faults = 1


  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
      @[<buffer>, ->, 4] := nondet as user_pin
      assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

BINSEC cannot reach the access_database routine under the current settings.

However, we can apply a more powerful fault model with a higher budget by using the max-faults parameter to increase the maximum number of faults the attacker can inject into the program.

tip

You can use the option enumerate-models = true to observe the models as there being validated during the SSE exploration.

  target-addresses = 0x1187, 0x11d8
  fault-model = TestInversionIte
  max-faults = 2 # Explore the ideal budget


  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
      @[<buffer>, ->, 4] := nondet as user_pin
      assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

The protected program is vulnerable again: if both executions of check are faulted, the two results agree and the attacker can bypass the protection.

tip

In order to hit the target address, a fault would normally need to be injected at location 0x0011d1 each time. Enabling permanent-faults = true ensures persistent corruption (e.g. modeling an instruction cache alteration), allowing us to bypass the protection with fewer faults (here, only one).

Fault Models Portfolio​

The ASE plugin provides several fault models. Let me demonstrate how they work.

Arbitrary Value Fault Model​

The Arbitrary Value fault model allows an attacker to replace any value during program execution with a value of their choice. It is the most powerful value-based fault model, as it gives the attacker maximum flexibility.

Here, we uncover a vulnerability by altering the initial value of the loop counter.

  target-addresses = 0x1187, 0x11d8
  fault-model = ArbitraryValue
  fault-on-flags = false
  excluded-DBA-vars = rsp, rbp
  where-check-feasibility = EveryConditionalBranch
  max-faults = 1


  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
      @[<buffer>, ->, 4] := nondet as user_pin
      assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

Instruction skip Fault Model​

The Instruction Skip model skips the execution of an instruction.
In this case, BINSEC returns a vulnerability where the attacker skips the initial loop counter assignment.

  target-addresses = 0x1187, 0x11d8


  fault-model = InstructionSkip
  fault-on-flags = false
  excluded-DBA-vars = rsp, rbp
  where-check-feasibility = EveryConditionalBranch
  max-faults = 1
  
  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
      @[<buffer>, ->, 4] := nondet as user_pin
      assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

note

This attack, however, is not fully convincing because it depends on whatever value happens to be at that stack location, which may be difficult for an attacker to control.

Mask Flip Fault Model​

The Mask Flip model allows flipping a specified mask on any value during execution. By default, it flips a single bit, but custom masks can be configured using the mask option.

In this case, we uncover a similar vulnerability by flipping the third least-significant bit of the loop counter's initial value.

  target-addresses = 0x1187, 0x11d8
  fault-model = MaskFlip
  fault-on-flags = false
  excluded-DBA-vars = rsp, rbp
  where-check-feasibility = EveryConditionalBranch
  max-faults = 1


  # same code base as previous script
  starting from <main>
  with concrete stack pointer
  load sections .text, .data, .rodata, .plt, .got from file


  replace <get_pin>() by
      @[<buffer>, ->, 4] := nondet as user_pin
      assume @[<buffer>,4] <> @[<secret>,4]
  return
  end


  reach <access_database> then print model
  halt at <main> return
Output

Plugin options​

The ASE plugin comes with numerous options to adjust models to a specific context.

warning

The plugin is still under active development; options and syntax are subject to change.

Key parameters and fault model configurations include:

  • fault-model: Specifies the attack strategy or type of fault injection;
  • max-faults: Defines the maximum fault budget;
  • enumerate-models: Enumerates several fault witnesses when a target is reached;
  • permanent-faults: Specifies whether faults are transient or persistent.;
  • fault-on-flags: Allows or forbids fault injection on condition flags;
  • excluded-DBA-vars: Defines a set of DBA variables to exclude from fault injection
    (e.g., excluded-DBA-vars = rsp, rbp excludes the stack and frame pointers).