Skip to main content

Secret Erasure

In this chapter, we will exercise the RELational Symbolic Execution engine of BINSEC to check that no secret data remains in memory after returning from a given function, also known as the secret-erasure property.

Indeed, a critical section should not keep the secret data in memory longer than necessary to prevent an attacker from exploiting a memory disclosure vulnerability and accessing the stored secret. Such code can thus use a so-called scrubbing function to fill the secret storage with public data (e.g. all zeros). Unfortunately, the compiler may consider such writes as dead assignments and optimize them out, leaving the executable code unprotected.

secret-erasure

The relational analysis plugin checkct proposes a secret-erasure check inspired by the Daniel et al. paper to ensure that memory does not contain any secret past a given point (a function return in this tutorial).

We will use a binary challenges from the original RELSE benchmark repository.

Test harness​

The benchmark challenges have been compiled with the following test harness.

#define __STDC_WANT_LIB_EXT1__ 1
#include <string.h>
#include <stdlib.h>
#include <stddef.h>
#include <stdlib.h>
#include <assert.h>
#include <stdio.h>
#include "safeclib/include/safe_mem_lib.h"
#include "../__libsym__/sym.h"

/* --------------- SCRUBBING FUNCTIONS ------------------ */
/* Implement your own using the following declaration */

/* [ ... ] */

/* Scrubbing function using memset */
#if MEMSET
void scrub(char *buf, size_t size) {
  memset(buf, 0, size);
}
#endif

/* [ ... ] */

/* --------------- END OF SCRUBBING FUNCTIONS ------------------ */

#define PASSWORD_SIZE 32

/* Volatile so everything is not optimized away */
volatile char good = 0;

void get_secret(char *bufer) {
  // This function is stubbed in SE and puts secret data into bufer
  HIGH_INPUT(PASSWORD_SIZE)(bufer);
}

/* Function that read and check the password */
void __attribute__ ((noinline)) password_checker(char *attempt) {
  char password[PASSWORD_SIZE];

  /* Put secret data in [password] */
  get_secret(password);

  /* Compares attempt to the secret password */
  good = 1;
  for (unsigned int i = 0; i < PASSWORD_SIZE; ++i) {
    good = good & (password[i] == attempt[i]);
  }
  
  // Scrubs secret from memory
  scrub(password, PASSWORD_SIZE);
}


int main () {
  char attempt[PASSWORD_SIZE];
  LOW_INPUT(PASSWORD_SIZE)(attempt);
  
  password_checker(attempt);

  /* Ideally we should declassify good */
  scrub((char *) &good, 1);
  return 0;
}

First (secure) candidate​

We will start with the basic memset variant compiled without optimization (O0) .

To simplify the initialization, we will start from a core dump, as seen in the Core dump chapter.

starting from core
explore all
check secret erasure over <main>

replace <high_input_32> (ptr) by
  @[ptr, 32] := secret as high_input_32
  return
end

replace <low_input_32> (ptr) by
  @[ptr, 32] := public as low_input_32
  return
end
Output

Here, the only thing new is the check secret erasure over <main> command to instruct BINSEC to check the property at the function <main> return.

As expected, the function memset was called and the secret was erased from the memory.

note

We replaced the library function high_input_32 and low_input_32 to produce, respectively a secret or a public value of 32 bytes.

Second (insecure) candidate​

Now, let us put it to the test with an optimizing compiler: we will try memset variant compiled with some optimization (O2) .

starting from core
explore all
check secret erasure over <main>

replace <high_input_32> (ptr) by
  @[ptr, 32] := secret as high_input_32
  return
end

replace <low_input_32> (ptr) by
  @[ptr, 32] := public as low_input_32
  return
end
Output