"Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities"

The ANSSI’s WooKey project is a secure encrypted USB storage device requiring user authentication in order to access its content. After attacks were found on it by ITSEFs, WooKey was hardened with countermeasures, some against fault injection. However, the effectiveness of these had yet to be tested in the project’s current version (0.9). We chose to analyze WooKey’s bootloader in order to check that the attacks had indeed been fixed as part of our paper.

Our goal when analyzing WooKey's bootloader was to find attack paths resulting in an outdated firmware being booted. This condition is expressed in the check_rollback function, which checks if the pointer to the chosen boot function corresponds to the latest firmware (returns false - attack unsuccessful) or to another, older one (returns true - attack successful). If the final state is "error" or "secbreach", the attack is considered unsuccessful since either nothing happened or the device destroyed itself.

We considered that the device was set up in dual bank mode since otherwise it cannot hold more than one firmware at a time. The "bootable" field in flip_shared_vars and flop_shared_vars should therefore be set to FW_BOOTABLE if firmware metadata is not deliberately left undefined or made symbolic. Make sure to also assign different values to the versions in that case. In some instances, such as analyzing with Frama-C's Eva plugin, it can be useful to specify one version while leaving the other imprecise in order to help with precision.

Content:

• loader_stubbed.c: bootloader source file (without injection points) with stubbed functions.
• main.c: main file calling the bootloader.
• no_dependencies
  • init.strategy: strategy file containing all possible injection points.
  • after_elimination.strategy: injection points from the previous strategy left after elimination of problematic ones.
  • src.c: bootloader code with simulated faults (not interchangeable with frte.c).
  • main_lazart.c: Lazart's analysis main with manual stubs.
• dependencies
  • brute_force_init.strategy: fault strategy file containing injection points obtained with the dependency analysis and the brute force selection.
  • brute_force_after_elimination.strategy: injection points from the previous strategy left after elimination of problematic ones.
  • no_brute_force_init.strategy: fault strategy file containing injection points obtained with the dependency analysis only.
  • no_brute_force_after_elimination.strategy: injection points from the previous strategy left after elimination of problematic ones.
  • frte.c: bootloader code with simulated faults.
  • main_lazart.c: Lazart's analysis main (with manual stubs).

License

The sources are published under a dual license form: LGPL2.1+ or BSD3 clause on the user's choice.