** 이 포스트에서 사용하는 코드는 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시간 이내로 풀 수 있는 난이도라고 생각하고 출제했는데, 한명(혹은 두 명)밖에 풀지 못했더군요. 약간 아쉽습니다.