Lab 4 - Reverse Engineering and Logic Locking

2026-01-12  |  Hackster , Labs , Reverse Engineering , Logic Locking

Introduction

This lab goes through simple logic locking on a combinatorial circuit design, and the implementation of a SAT attack to determine the key used for logic locking. The SAT attack can be performed using a comparison of netlists for the locked and unlocked device. You may also implement the SAT attack using MicroPython, or just use simple brute force (given that the cores are relatively small).

Goals:

  1. Correctly interpret the behaviour of a provided combinational logic circuit using a provided binary with no logic locking
  2. Analyse the provided netlist to carry out a SAT attack and determine the key used for the hardware design using propositional logic solvers
  3. Automatically determine the correct key for the locked circuits using the locked binary and behavioural description (i.e. truth table) of the unlocked binary

Getting Started

  1. Download lab4_bitstreams.zip from Moodle and unzip the contents into hackster-programmer/diy, this includes the required Makefile, run_circuit.py, circuit_prop.txt, binaries, and .json netlists for the locked and unlocked circuits.

The python script, run_circuit.py, currently will set all the inputs to 0, and reflect the output values on the two RP2040 LEDs (APP1, APP2)

The netlists and binaries will be prefixed with your zID (zXXXXXXX_locked.bin, zXXXXXXX_unlocked.bin, zXXXXXXX_locked.json).

To load the unlocked binary onto the hackster, replacing the zID with your zID, use:

ZID=zXXXXXXX make run_fpga

To load the locked binary onto the hackster, use:

ZID=zXXXXXXX make run_fpga_locked

Interpreting hardware behaviour

With the unlocked binary loaded onto the hackster, and starting with run_circuit.py, write a program to check the behaviour of the circuit. At this point, the circuit should be the unlocked version, so the key doesn’t need to be set. Using this, fill out the truth table in circuit.csv.

I/O pin schematic label Direction Value
APP_ICE40_D0 Input input[0]
APP_ICE40_D1 Input input[1]
APP_ICE40_D2 Input input[2]
APP_ICE40_D3 Input input[3]
APP_ICE40_D4 Input key[0]
APP_ICE40_D5 Input key[1]
APP_ICE40_D6 Input key[2]
APP_ICE40_D7 Output output[0]
APP_ICE40_D8 Output output[1]

The provided circuit uses all the available digital I/O pins, these can be read/written to in the micropython script. Typically, the key values would instead be stored or accessed separately, however for this exercise, inputs and key values are all provided via the same RP2040 AppMicro GPIO.

SAT attack and translating the netlist

From the provided .json file, determine the behaviour of the locked circuit using gate definitions, and convert these into propositional logic statement(s), using the syntax for the SAT solver on logictools.org. This could be done as a single statement for both output values, or be separated for each output.

Use the method in High-Level Approaches to Hardware Security (section 4) to determine the key.

For the locked circuit, this module is named “circuit_locked”, for the unlocked circuit, the module is named “circuit”. In the provided files, in the module, bits 3, 4, 5, 6 should correspond to the inputs 0, 1, 2, 3 respectively.

"ports": {
  "ICE_CLK": {
    "direction": "input",
    "bits": [ 2 ]
  },
  "APP_in": {
    "direction": "input",
    "bits": [ 3, 4, 5, 6 ]
  },
  "APP_key": {
    "direction": "input",
    "bits": [ 7, 8, 9 ]
  },
  "APP_out": {
    "direction": "output",
    "bits": [ 10, 11 ]
  }
}

The json netlist generated by Yosys defines the circuit with multiple LUT4s, below is an example LUT4 definition for an and gate (inside the “cells” for the module) - both I1 and I0 are unused, so in the truth table only states with I1 = I0 = “0” will occur.

LUT_INIT defines the output values for each of the input combinations from [15:0]. More documentation about the json netlist generated by yosys can be found here, the full explanation of SB_LUT4 primitive is here (see Page 47-48).

LUT4 example showing the input combinations and corresponding output values defined by the LUT_INIT parameter

LUT4 example

Challenge Task: Programmatically determine the key bits

Write a Python script, get_key.py, which is runnable on the RP2040, to determine the correct key using the expected behaviour of the unlocked circuit and the provided locked circuit (zXXXXXXX_locked.bin). In this case the design is quite small so can be determined by brute force (worth 1 mark) or by using a programmatic SAT attack (2 marks).

Resources

Resources:

Video resources:

Deliverables and Weightings:

This lab is worth 10% of your final grade for this course.

Deliverables:

Grading Rubric

SAT Attack on Logic Locking (10%)