original writeup can be found [here](https://zdiv.net/illogical/)

## Illogical - 400 points

> Since the fall in grace of their major competitor, Currency Gmbh tries to take
> over the market with a new encrypted communications device. Unfortunately,
> because of the chip shortage they had to rely on very few components and roll
> their own crypto. But hey, at least they are not backdoored, right ?
> That's what we think, so we typed the flag for you using their device, can you
> get it ?
> FLAG FORMAT : ins-...
> You'll find the following items in the challenge file :
> - hardware.bin - The FPGA bitstream
> - schematic.pdf - Hardware schematic
> - flag.mkv - Us typing the flag.
>
> You can have a look at the device around the admins. Good luck !

The core of the challenge is to retrieve the flag being typed on a PS/2
keyboard, the keyboard is connected to a box which has 8 LEDs for a display.

All we have is a video recording of the LEDs while the flag is being typed.
The video doesn't show the keys typed but we can see the LED pattern after
each key being stroke. The goal is to understand what happen in the box and
how to retrieve the key typed from the LED pattern.

The challenge also provides a very terse schematic and more importantly the
actual bitstream used in the FPGA.

For those who don't know a FGPA is a special circuit that can be reconfigured,
the bitstream is the actual configuration that will be loaded when the FPGA
starts. I am not an FPGA expert but in a FPGA we can find LUTs (look up table),
MUXs and registers. The bitstream will set the actual bits in LUTs, select how
to route signals with Muxs.

Even though I am not familiar with reversing a FPGA bitstream, the only toolchain
I know to work with FPGA is Yosys, Yosys is a free and open-source toolchain that
can convert (aka synthesis) Verilog, an Hardware Description Language (HDL), to some
FPGAs bitstream.

My sole experience with using Yosys was to synthesis a RISC-V softcore on ECP5, which
is possible thanks to the trellis project, the project of reversing the bitstream format
for targeting ECP5 FPGAs. The equivalent project for iCE40 FPGAs is called IceStorm.

## Hardware

First we can take a look at the `schematic.pdf` file, in this file we can found two
informations, first the name of the FPGA boards being used: `TinyFPGA BX`.
We can find more information online:
> TinyFPGA BX - ICE40 FPGA Development Board with USB
> ICE40LP8K

Secondly we can see how the PS/2 interface and LEDs are connected to the FPGA boards,
this will be handy latter.

Yosys accept constraint file `.pcf` that are board depends. I am not very familiar with
there format but they can be used to give names to the FPGA io such which IO is connect
to an user LED (blinky) or even which IO is connected to an external clock with a given
frequency.
The `TinyFPGA BX` pcf file can be found on [github][1]:
```
set_io --warn-no-port PIN_1 A2
set_io --warn-no-port PIN_2 A1
set_io --warn-no-port PIN_3 B1
set_io --warn-no-port PIN_4 C2
set_io --warn-no-port PIN_5 C1
set_io --warn-no-port PIN_6 D2
set_io --warn-no-port PIN_7 D1
set_io --warn-no-port PIN_8 E2
...
set_io --warn-no-port PIN_23 B6
set_io --warn-no-port PIN_24 A6
...
```

Although this is optional, we can go further and modify the .pcf file with the information
from the provided schematic, this should gives:
```
set_io --warn-no-port LED0 A2
set_io --warn-no-port LED1 A1
set_io --warn-no-port LED2 B1
set_io --warn-no-port LED3 C2
set_io --warn-no-port LED4 C1
set_io --warn-no-port LED5 D2
set_io --warn-no-port LED6 D1
set_io --warn-no-port LED7 E2
set_io --warn-no-port CLK B6
set_io --warn-no-port DAT A6
```

## FPGA bitstream to Verilog

For this step, I've cloned the [IceStorm Project][2], and compiled its tools.

```
$ iceunpack hardware.bin > hardware.asc
$ icebox_vlog.py -s -d cm81 -p pins.pcf hardware.asc > hardware.v
```

We now have a very very verbose Verilog source file.

## Cleaning the Verilog

The generated Verilog is very hard to follow, and I didn't have a quick
and easy solution to make it understandable. The only solution I have is
to untangle the wires.

```
...
always @(negedge n1) if (1'b1) LED7 <= 1'b0 ? 1'b0 : n71;
always @(negedge n1) if (1'b1) LED4 <= 1'b0 ? 1'b0 : n72;
always @(negedge n1) if (1'b1) n12 <= 1'b0 ? 1'b0 : n127;
always @(negedge n1) if (1'b1) n15 <= 1'b0 ? 1'b0 : n128;
always @(negedge n1) if (1'b1) n20 <= 1'b0 ? 1'b0 : n76;
always @(negedge n1) if (1'b1) n11 <= 1'b0 ? 1'b0 : n80;
always @(negedge n1) if (1'b1) n10 <= 1'b0 ? 1'b0 : n82;
always @(negedge n1) if (1'b1) n14 <= 1'b0 ? 1'b0 : n83;
always @(negedge n1) if (1'b1) LED5 <= 1'b0 ? 1'b0 : n115;
always @(negedge n1) if (1'b1) n18 <= 1'b0 ? 1'b0 : n116;
always @(negedge n1) if (1'b1) LED3 <= 1'b0 ? 1'b0 : n118;
always @(negedge n1) if (1'b1) LED0 <= 1'b0 ? 1'b0 : n119;
always @(negedge n1) if (1'b1) n13 <= 1'b0 ? 1'b0 : n109;
always @(negedge n1) if (1'b1) LED1 <= 1'b0 ? 1'b0 : n93;
always @(negedge n1) if (1'b1) LED6 <= 1'b0 ? 1'b0 : n97;
always @(negedge n1) if (1'b1) LED2 <= 1'b0 ? 1'b0 : n98;
...
```

In the Verilog source there is a lot of duplicated information, we can start
by merging the all the synchrone statement in a single block.

```
always @(negedge n1) begin
if (1'b1) LED7 <= 1'b0 ? 1'b0 : n71;
if (1'b1) LED4 <= 1'b0 ? 1'b0 : n72;
if (1'b1) n12 <= 1'b0 ? 1'b0 : n127;
if (1'b1) n15 <= 1'b0 ? 1'b0 : n128;
if (1'b1) n20 <= 1'b0 ? 1'b0 : n76;
if (1'b1) n11 <= 1'b0 ? 1'b0 : n80;
if (1'b1) n10 <= 1'b0 ? 1'b0 : n82;
if (1'b1) n14 <= 1'b0 ? 1'b0 : n83;
if (1'b1) LED5 <= 1'b0 ? 1'b0 : n115;
if (1'b1) n18 <= 1'b0 ? 1'b0 : n116;
if (1'b1) LED3 <= 1'b0 ? 1'b0 : n118;
if (1'b1) LED0 <= 1'b0 ? 1'b0 : n119;
if (1'b1) n13 <= 1'b0 ? 1'b0 : n109;
if (1'b1) LED1 <= 1'b0 ? 1'b0 : n93;
if (1'b1) LED6 <= 1'b0 ? 1'b0 : n97;
if (1'b1) LED2 <= 1'b0 ? 1'b0 : n98;
end
```

From there we can see another pattern, we can see a `if (1'b1)` in front of
every line, this is always true and can be removed. Also each register being
set in this block is done with a value from a ternary with a constant condition.
This is most likely due to the way the logic is actually wired inside the FPGA,
but this is no use for our understanding.

```
assign n83 = (n11 ? (n12 ? (n15 ? n13 : !n13) : (n15 ? !n13 : n13)) : (n12 ? (n15 ? !n13 : n13) : (n15 ? n13 : !n13)));
assign n127 = n11;
assign n128 = n18;
assign n76 = n14;
assign n80 = n15;
assign n82 = n12;
assign n116 = n20;
assign n109 = n10;
assign n119 = (n46 ? !n15 : n15);
assign n93 = (n20 ? !n45 : n45);
assign n98 = (n11 ? !n41 : n41);
assign n118 = (n42 ? !n18 : n18);
assign n72 = (n44 ? !n10 : n10);
assign n115 = (n13 ? !n6 : n6);
assign n97 = (n7 ? !n14 : n14);
assign n71 = (n12 ? !n25 : n25);
always @(negedge n1) begin
n12 <= n127;
n15 <= n128;
n20 <= n76;
n11 <= n80;
n10 <= n82;
n14 <= n83;
n18 <= n116;
n13 <= n109;
LED0 <= n119;
LED1 <= n93;
LED2 <= n98;
LED3 <= n118;
LED4 <= n72;
LED5 <= n115;
LED6 <= n97;
LED7 <= n71;
end
```

The next step is to bring back the actual values being affected to the registers.
In our Verilog we only see wire on the right side, even when the wire is directly
assigned to a register. All the right side values can be replaced with the actual
logic.

We can also notice the ternary of the form `(a ? !b : b)` which is the same as
`(a ^ b)`.
```
always @(negedge n1) begin
s_7 <= s_6;
s_6 <= s_5;
s_5 <= s_4;
s_4 <= s_3;
s_3 <= s_2;
s_2 <= s_1;
s_1 <= s_0;
s_0 <= !(s_3 ^ s_4 ^ s_5 ^ s_7);
LED0 <= s_3 ^ n46;
LED1 <= s_1 ^ n45;
LED2 <= s_4 ^ n41;
LED3 <= s_2 ^ n42;
LED4 <= s_6 ^ n44;
LED5 <= s_7 ^ n6;
LED6 <= s_0 ^ n7;
LED7 <= s_5 ^ n25;
end
```

At this point we can see a 8-bits LFSR `s_[0-7]` which is XOR with the PS/2 input.

## Permutation

If you paid attention, each LEDs isn't XORed with the corresponding bit from the LFSR.
There is a permutation going on.
During the CTF I've mixed some lines, or mixed the bit order of the PS/2 input and the
output from the reversed Verilog didn't matched what the actual HW was displaying.

As we were allowed to reset the board we can put the LFSR to a known state, which is zero
after reset.
From this point it is possible to retrieve the actual permutation by typing a known input
over and over and taking note of the LEDs outputs.

## Getting the initial state

At this point, the only missing part is the initial state of the LFSR.
For this we can brute force the 256 possible initial state and test if the simulated LED pattern
matches the first three letters being typed.

The three first key typed are `ins` and there keycode are `0b01000011` `0b00110001` `0b00011011`.
In the video the three first LEDs pattern are `0b10110001` `0b01001011` `0b00110000`, which are
the result **after** the key being pressed.

```
uint16_t s, i;
for (i = 0; i < 256; i++) {
s = i; /* try i as initial state */
if ((lut(s) ^ 0b01000011) != led[0]) /* i */
continue;
s = lfsr(s);
if ((lut(s) ^ 0b00110001) != led[1]) /* n */
continue;
s = lfsr(s);
if ((lut(s) ^ 0b00011011) != led[2]) /* s */
continue;
s = lfsr(s);
break;
}
printf("found initial state %2x\n", i);
```

## Getting the scan codes

```
s = i; /* initial state 0xe3 */
for (i = 0; i < len; i++) {
printf("%x ", led[i] ^ lut(s));
s = lfsr(s);
}
printf("\n");
```

Which gives the following output:
```
43 31 1b 4a 3c 1b 32 66 66 66 4d 1b 1e 29 43 1b 29 1c 1d 26 1b 44 3a 24 49 5a
```
which translate to:
```
ins-usb<del><del><del>ps2 is aw3some.
```
and the flag is:
```
ins-ps2 is aw3some.
```

[1]: https://github.com/tinyfpga/TinyFPGA-BX/tree/master/icestorm_template/pins.pcf
[2]: https://github.com/YosysHQ/icestorm
[3]: https://yosyshq.net/yosys/

Original writeup (https://zdiv.net/illogical/).