** 이 포스트에서 사용하는 코드는 https://github.com/perillamint/inc0gnito-2017-fpga 에 있습니다.

2017년도 Inc0gnito CTF 에 색다르고 재미있는(?) 문제를 출제해 보았습니다. 바로 FPGA 리버스 엔지니어링이 그것인데요, README.md 에 주어진 문제는 다음과 같습니다

칩의 key 포트에 어떤 입력을 넣었을 때, data 에 자료가 출력되는지를 알아내십시오.
key 포트에 들어간 문자열과, data 포트에 들어간 문자열을 이어 붙인 것이 문제의 flag 입니다. (예: key = ABCD, data = qwer 일 때 flag 는 ABCDqwer)

이 문제가 요구하는 것은, 주어진 칩의 FPGA 비트스트림을 역공학해, 칩이 숨기고 있는 데이터와, 그 데이터를 출력하게 해주는 키를 구하는 것입니다.

이제 README.md 의 힌트 부분을 읽어봅시다.

  • SiliconBlue
  • Lattice

이 힌트를 검색해 보면, 이 문제에서 사용한 FPGA 기종은 Lattice 사의 iCE 시리즈라는 것을 추정할 수 있습니다.

이제 iCE FPGA reverse engineering 이라는 키워드를 검색해보면, 이 FPGA 는 오픈 소스 툴체인을 가지고 있는 FPGA 인 것을 확인할 수 있습니다.

해당 툴체인의 문서를 확인해 보면, iceunpack 툴이 비트스트림을 비트맵 파일로 변환해줄 수 있고, icebox 툴이 비트맵 파일을 이에 대응하는 베릴로그 모델로 변환해줄 수 있다고 합니다. 컴파일된 비트스트림을 대상으로 iceunpack 과 icebox_vlog을 돌려봅니다.

iceunpack inc0gnito.bin > inc0gnito_rev.asc
icebox_vlog -s -S -p inc0gnito.pcf inc0gnito_rev.asc > inc0gnito_rev.v 

출력물을 조사해보면 수 많은 베릴로그 와이어 선언이 있고, 다음과 같이 몇 가지 논리 테이블이 기술되어 있습니다.

assign n68 = /* LUT    1 21  1 */ \key[23]  ? 1'b0 : \key[20]  ? 1'b0 : \key[15]  ? 1'b0 : \key[11]  ? 1'b0 : 1'b1;
assign n69 = /* LUT    1 21  2 */ n49 ? n43 ? n31 ? n19 ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n70 = /* LUT    1 16  2 */ \key[30]  ? \key[27]  ? \key[26]  ? \key[22]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n71 = /* LUT    1 20  6 */ \key[21]  ? \key[19]  ? \key[18]  ? \key[17]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n72 = /* LUT    1 22  4 */ \key[16]  ? \key[14]  ? \key[13]  ? \key[12]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n73 = /* LUT    1 25  5 */ \key[9]  ? 1'b0 : \key[8]  ? 1'b0 : \key[7]  ? 1'b0 : \key[5]  ? 1'b0 : 1'b1;
assign n74 = /* LUT    1 21  4 */ n28 ? n18 ? n46 ? n36 ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n75 = /* LUT    1 28  3 */ \key[3]  ? 1'b0 : \key[2]  ? 1'b0 : \key[0]  ? 1'b0 : \key[31]  ? 1'b0 : 1'b1;
assign n76 = /* LUT    1 27  7 */ \key[10]  ? \key[6]  ? \key[4]  ? \key[1]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
assign n77 = /* LUT    1 16  5 */ \key[29]  ? 1'b0 : \key[28]  ? 1'b0 : \key[25]  ? 1'b0 : \key[24]  ? 1'b0 : 1'b1;
assign n78 = /* LUT    1 21  6 */ 1'b0 ? 1'b0 : 1'b0 ? 1'b0 : n32 ? n33 ? 1'b1 : 1'b0 : 1'b0;

이를 libsmt 포멧으로 기술해줍니다. (전체 파일: https://github.com/perillamint/inc0gnito-2017-fpga/blob/master/inc0gnito.lsp)

part of inc0gnito.lsp
;; assign n68 = /* LUT    1 21  1 */ \key[23]  ? 1'b0 : \key[20]  ? 1'b0 : \key[15]  ? 1'b0 : \key[11]  ? 1'b0 : 1'b1;
(assert (= n68
           (if k23
               false
             (if k20
                 false
               (if k15
                   false
                 (if k11
                     false
                   true))))))

;; assign n69 = /* LUT    1 21  2 */ n49 ? n43 ? n31 ? n19 ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n69
           (if n49
               (if n43
                   (if n31
                       (if n19
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n70 = /* LUT    1 16  2 */ \key[30]  ? \key[27]  ? \key[26]  ? \key[22]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n70
           (if k30
               (if k27
                   (if k26
                       (if k22
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n71 = /* LUT    1 20  6 */ \key[21]  ? \key[19]  ? \key[18]  ? \key[17]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n71
           (if k21
               (if k19
                   (if k18
                       (if k17
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n72 = /* LUT    1 22  4 */ \key[16]  ? \key[14]  ? \key[13]  ? \key[12]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n72
           (if k16
               (if k14
                   (if k13
                       (if k12
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n73 = /* LUT    1 25  5 */ \key[9]  ? 1'b0 : \key[8]  ? 1'b0 : \key[7]  ? 1'b0 : \key[5]  ? 1'b0 : 1'b1;
(assert (= n73
           (if k9
               false
             (if k8
                 false
               (if k7
                   false
                 (if k5
                     false
                   true))))))

;; assign n74 = /* LUT    1 21  4 */ n28 ? n18 ? n46 ? n36 ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n74
           (if n28
               (if n18
                   (if n46
                       (if n36
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n75 = /* LUT    1 28  3 */ \key[3]  ? 1'b0 : \key[2]  ? 1'b0 : \key[0]  ? 1'b0 : \key[31]  ? 1'b0 : 1'b1;
(assert (= n75
           (if k3
               false
             (if k2
                 false
               (if k0
                   false
                 (if k31
                     false
                   true))))))

;; assign n76 = /* LUT    1 27  7 */ \key[10]  ? \key[6]  ? \key[4]  ? \key[1]  ? 1'b1 : 1'b0 : 1'b0 : 1'b0 : 1'b0;
(assert (= n76
           (if k10
               (if k6
                   (if k4
                       (if k1
                           true
                         false)
                     false)
                 false)
             false)))

;; assign n77 = /* LUT    1 16  5 */ \key[29]  ? 1'b0 : \key[28]  ? 1'b0 : \key[25]  ? 1'b0 : \key[24]  ? 1'b0 : 1'b1;
(assert (= n77
           (if k29
               false
             (if k28
                 false
               (if k25
                   false
                 (if k24
                     false
                   true))))))

;; assign n78 = /* LUT    1 21  6 */ 1'b0 ? 1'b0 : 1'b0 ? 1'b0 : n32 ? n33 ? 1'b1 : 1'b0 : 1'b0;
(assert (= n78
           (if n32
               (if n33
                   true
                 false)
             false)))

이를 z3 을 이용해 data 포트가 0x00000000 이 아닐 때의 해를 찾고, 이를 hex 문자열로 변환하면

#!/bin/bash
z3 inc0gnito.lsp | perl -p -e 's/Bool\n//g' | perl -p -e 's/[ ]+/ /g' > result.lsp
cat result.lsp | grep define-fun | awk '{ print $2 " " $4 }' | sed -r 's/\)//' > result.txt
cat result.txt | grep 'd[0-9]*' | sort --version-sort > data.txt
cat result.txt | grep 'k[0-9]*' | sort --version-sort > key.txt

node decode.js

다음과 같은 결과를 얻습니다.

key = 4c6f7452
data = 464c45

이를 문제의 Errata 를 참조해(죄송합니다. 문제 낼 당시 밤을 새서 많이 피곤한 상태였습니다), 해석하면 키는

INC0{LotRELF}

가 됩니다.

ps.

전 이 문제를 사람이 1-2시간 이내로 풀 수 있는 난이도라고 생각하고 출제했는데, 한명(혹은 두 명)밖에 풀지 못했더군요. 약간 아쉽습니다.