[rev] SekaiCTF 2026 - nevm Writeup## 개요 SekaiCTF 2026 rev/nevm은 70MB대 EVM 바이트코드를 다루는 리버싱 문제입니다. 문제 설명은 평범한 EVM 컨트랙트처럼 보이게 쓰여 있었지만, 실제로는 EVM 안에 구현된 별도의 VM을 분석해야 하는 문제입니다. 풀이의 핵심은 거대한 EVM 바이트코드를 그대로 읽는 것이 아니라, 내부 VM의 trace를 만들고 각 instruction handler의 의미를 복원하는 것입니다. 이후 복원한 의미가 실제 컨트랙트 출력과 맞는지 여러 입력으로 검증하고, 최종적으로 SMT 제약식을 만들어 16바이트 평문 네 개를 구합니다. ## 문제 설명 및 구조 주어진 설명은 매우 짧았습니다. ```text just your average 70 mb evm contract ``` 배포 파일 구조는 대략 다음과 같습니다. ```text rev_nevm/ ├── README.md ├── run.sh ├── challenge_1.bin ├── challenge_2.bin ├── challenge_3.bin ├── challenge_4.bin └── build/ ├── Dockerfile ├── revm-smc.patch └── runner/ ├── Cargo.toml └── src/ └── main.rs ``` `README.md`에는 Loki에서 영감을 받은 문제라는 설명과 `./run.sh`로 실행하라는 내용만 있습니다. 실제 문제 조건은 대부분 `build/runner/src/main.rs`에 들어 있습니다. 배포 파일명이 `challenge_1.bin`부터 `challenge_4.bin`까지로 나뉘어 있으므로, 이 글에서도 네 컨트랙트를 각각 challenge 1부터 challenge 4라고 부르겠습니다. 각 challenge는 서로 다른 EVM 바이트코드이지만, runner는 네 challenge를 같은 방식으로 호출하고 각각의 반환값을 고정 타겟과 비교합니다. `run.sh`는 Docker 이미지를 준비한 뒤 runner에 인자를 넘기는 래퍼입니다. 따라서 문제를 풀 때는 네 개의 바이트코드 자체와, 이들을 어떻게 호출하고 검증하는지 정의한 runner를 함께 봐야 합니다. ## 1. Runner 분석 먼저 `build/runner/src/main.rs`를 보면 목표가 명확해집니다. runner의 `solve` 모드는 평문 네 개를 인자로 받습니다. 그리고 `challenge_1.bin`부터 `challenge_4.bin`까지 순서대로 읽으면서, 각 평문을 해당 challenge에 넣어 실행합니다. ```rust for (i, pt) in plaintexts.iter().enumerate() { let n = i + 1; let code = fs::read(format!("{dir}/challenge_{n}.bin")).expect("read challenge"); ... } ``` `main`에서도 `solve` 모드는 평문 네 개가 들어온 경우에만 실행됩니다. ```rust \[cmd, pts @ ..\] if cmd == "solve" && pts.len() == 4 => solve(pts), ``` 각 컨트랙트에는 다음 형태의 calldata가 들어갑니다. ```text calldata = 20 bytes zero || 16 bytes plaintext ``` 이후 반환 데이터 앞 16바이트를 `TARGETS[i]`와 비교합니다. ```rust if run_contract(code, calldata)[..16] == TARGETS[i] { eprintln!("contract {n}: ok"); } ``` 타겟 네 개가 존재하는 이유도 runner에서 바로 확인할 수 있습니다. `TARGETS`가 4개의 16바이트 배열로 정의되어 있고, runner가 `challenge_{n}.bin`을 읽을 때 같은 인덱스의 타겟을 비교 대상으로 사용합니다. ```text target_1 = ba9383cedce86c2fed648b9d172ea216 target_2 = e78b91ff6200517467b1e55a85a44742 target_3 = cc07fb3d2216fc7b0aeca4d3cced2095 target_4 = fe1815270a539cc1155e320b92aef397 ``` 네 평문을 모두 찾으면 runner는 64바이트를 이어 붙이고, keccak 기반 keystream으로 flag blob을 XOR합니다. ```text packed = pt1 || pt2 || pt3 || pt4 key0 = keccak256(packed) key1 = keccak256(key0) flag[0..32] = key0 ^ FLAG_BLOB[0..32] flag[32..64] = key1 ^ FLAG_BLOB[32..64] ``` 따라서 문제는 다음 네 함수를 각각 푸는 형태로 볼 수 있습니다. ```text F_i(plaintext_i)\[0:16\] == target_i ``` 각 평문은 16바이트입니다. ## 2. Not EVM 이 문제는 EVM 문제가 아닌 VM 문제입니다. 문제를 처음 보면 거대한 EVM 바이트코드를 직접 리버싱해야 할 것처럼 보입니다. 하지만 실행 흐름을 따라가면, 실제 로직은 EVM 위에서 한 번 더 구현된 내부 VM이 처리합니다. 처음에는 직접 EVM 흐름을 따라가려는 시도도 해보았지만, 바이트코드 크기와 dispatcher 구조 때문에 그 방식은 금방 한계가 보였습니다. 각 컨트랙트는 약 70MB대이고, 일반적인 EVM 리버싱처럼 decompile 결과를 읽어서 끝낼 수 있는 구조가 아닙니다. 실행을 따라가면 크게 두 층이 보입니다. ```text EVM 바이트코드 └─ first layer decrypt / setup └─ internal VM dispatcher └─ VM instruction stream └─ register / scratch / bank / table / calldata operations ``` 중요한 점은 EVM instruction 하나하나의 의미를 복원하는 것이 아니라, 내부 VM instruction의 형식과 의미를 복원해야 한다는 것입니다. 내부 VM instruction은 대략 다음 정보를 가집니다. ```text opcode index destination register source register 0..3 immediate / selector fields ``` trace는 각 VM instruction을 다음 형태로 출력하도록 구성합니다. ```text DEC idx dst f= s0= s1= s2= s3= out= ``` 아래는 실제 풀이 중 challenge 4의 return 직전 구간에서 뽑은 trace 일부입니다. ```text DEC 88029 idx201 dst 239 f=201,239,240,239,1,1,0,2996 s0=0x0000...65099407f34340fdb4e7cb9b7b667a6d s1=0x0000...0000000000000080 out=0x65099407f34340fdb4e7cb9b7b667a6d0000... ``` 여기서 `idx201`이 VM instruction 번호이고, `dst 239`가 destination register입니다. `f[2]..f[5]`는 source register로 사용됩니다. ## 3. Trace Alignment 각 challenge는 trace를 디코딩할 때 필요한 상수와 instruction 번호 offset이 달랐습니다. ```text challenge 1: C = 0x0e39ceaa15cd59786f3a37b12d07931a0f78459a54d39db5ffc75d952d308b77 offset = 0 challenge 2: C = 0xd8bf07278fdef01ddba6c0be31e1bf7f27f974817c0b54547d5ded84c5e882b7 offset = 3416 challenge 3: C = 0x8d5d274d2987f6d2bd82b31f9cf5d743d301f1690d640fde49df32c1b22abfdf offset = 3680 challenge 4: C = 0xa21de7f294d2fdc892829c238b4ab7c5ddd78e697d63b63ea126f3c257d878bf offset = 1920 ``` 여기서 `C`는 디코딩된 trace 값을 풀 때 사용하는 challenge마다 다른 상수이고, `offset`은 challenge마다 밀려 있는 instruction 번호를 공통 기준으로 맞추기 위해 빼는 값입니다. 이 두 값을 환경변수로 넘겨야 서로 다른 challenge의 trace를 같은 VM instruction 집합 위에서 비교할 수 있습니다. trace는 다음 형태로 생성합니다. 출력 파일은 분석 스크립트와 같은 작업 디렉터리에 두었습니다. ```bash NEVM_C=$C \ NEVM_IDX_OFFSET=$OFFSET \ NEVM_DECODE=1 \ ./tools/evm_fast ./challenge_$N.bin \ 0000000000000000000000000000000000000000$PLAINTEXT_HEX \ 0 trace > trace_ch${N}_sample.txt 2> trace_ch${N}_sample.err ``` `NEVM_IDX_OFFSET`이 특히 중요합니다. challenge 2 이후는 같은 의미의 handler라도 instruction 번호가 challenge마다 밀려 있습니다. 이 값을 빼고 보정해야 같은 연산이 같은 번호로 정규화됩니다. 처음에는 이 offset을 충분히 의식하지 않고 trace를 비교하면서, 같은 연산을 서로 다른 handler처럼 보는 구간이 있었습니다. 이후 instruction 번호를 정규화하자 challenge 사이에 공유되는 구조가 훨씬 선명하게 보였습니다. ## 4. V-space 정규화 디코딩된 trace의 소스와 출력은 그대로 보면 여전히 마스킹되어 있습니다. 그런데 각 trace마다 하나의 값 `H`를 잡으면 대부분의 연산이 깔끔해집니다. ```text H = first_decoded_output ^ 0xc0de V(x) = x ^ H ``` 이후 소스, 스크래치 슬롯, 출력값을 모두 `V-space`에서 다룹니다. `H`는 trace마다 다시 계산합니다. 즉, 서로 다른 입력에서 나온 값을 그대로 섞어 비교하지 않고, 각 trace 안에서 같은 마스크를 걷어낸 뒤 handler 입력과 출력을 비교합니다. 이 정규화를 거치면 XOR, ADD, SHIFT 같은 기본 연산이 원래 형태에 가깝게 보이기 시작합니다. 한 행의 소스가 `s0, s1, s2, s3`, 출력이 `out`이면 모델 입력은 다음과 같습니다. ```text o0 = V(s0) o1 = V(s1) o2 = V(s2) o3 = V(s3) result = V(out) ``` 스크래치 슬롯도 같은 공간에서 관리합니다. ```text scratch[0x19] = V(saved value) scratch[0x1a] = V(saved value) scratch[0x1b] = V(saved value) scratch[0x1c] = V(saved value) ``` 최종적으로 handler 의미 복원에 사용하는 튜플은 다음과 같습니다. ```text o = ( V(s0), V(s1), V(s2), V(s3), scratch_0x19, scratch_0x1a, scratch_0x1b, scratch_0x1c, f6, f7, H ) ``` 실제 검증기에서도 같은 형태로 `H`와 입력 튜플을 만듭니다. trace 첫 출력에서 `H`를 잡고, register와 scratch 값을 모아 handler 입력 `o`를 구성합니다. ```python H = first_trace_output ^ 0xc0de o = ( V(source0), V(source1), V(source2), V(source3), scratch_0x19, scratch_0x1a, scratch_0x1b, scratch_0x1c, f6, f7, H, ) ``` 정규화 후 기본 명령어들은 상당히 단순해집니다. ```text idx5 : xor idx3 : add idx8 : scratch save idx9 : dynamic bank write idx10 : dynamic bank read ``` 테이블 조회, 호출 데이터 읽기, 반환 저장은 challenge마다 명령어 번호만 다르고 의미는 같습니다. ## 5. Handler Semantics Recovery handler 복원은 이 풀이에서 가장 중요한 부분입니다. 단순히 샘플 몇 개에 맞는 식을 찾는 것이 아니라, 실제 trace 값과 계속 비교하면서 검증 가능한 의미를 붙여야 합니다. 각 handler는 `(idx, f7)`을 키로 잡습니다. ```text key = (idx, f7) sample = (o, V(out)) ``` 같은 키를 가진 trace 행을 모두 모으면, 해당 handler에 대해 입력 튜플과 실제 출력값의 쌍이 생깁니다. 이 쌍을 기준으로 후보식을 만들고, 모든 샘플을 통과하는지 확인합니다. 복원된 handler는 하나의 dispatch 함수에서 처리합니다. 특수 명령어인 table read, calldata read, bank read를 먼저 처리하고, 나머지는 `(idx, f7)`로 찾은 의미를 평가합니다. 이 함수가 `None`을 반환하면 아직 의미를 붙이지 못한 handler로 보고, 뒤의 검증 단계에서 `UNFIT`으로 집계합니다. ```python def eval_handler(challenge, idx, fields, operands, trace_out, bank, mask, plaintext=None): config = challenge_config[challenge] key = (idx, fields[7]) if idx in (2, 6): return trace_out if idx == config.table_read: return table_word(challenge, operands[0]) if idx == config.calldata_read: return calldata_word(operands[0], plaintext) if idx == 10: return bank.get(fields[6], 0) if idx in (config.return_store, 11): return 0 kind = recovered_semantics.get(key) if kind is None: return None return eval_semantics(kind, operands) ``` ### 5.1 샘플 수집 먼저 모든 디코딩 trace를 돌면서 다음 정보를 수집합니다. ```text handler key = (idx, f7) handler input = (V(s0), V(s1), V(s2), V(s3), scratch slots, f6, f7, H) handler expected = V(out) ``` 이 구조가 잡히면 handler 복원은 주어진 key에 대해 모든 샘플을 만족하는 함수 `f(o)`를 찾는 문제가 됩니다. 후보 함수가 하나의 샘플이라도 틀리면 버립니다. 초반 샘플에서는 맞지만 추가 검증 벡터에서 깨지는 경우가 있었기 때문에, 나중에는 복원 단계와 검증 단계를 분리해서 보았습니다. ### 5.2 기본 템플릿 먼저 단순 연산부터 맞춥니다. 아래 목록은 최종 의미를 미리 정해둔 것이 아니라, 각 handler 샘플에 대입해 보는 후보 템플릿입니다. ```text id(o[i]) ~o[i] z64(o[i]) iszero(o[i]) o[i] ^ o[j] o[i] + o[j] o[i] - o[j] o[i] & o[j] o[i] | o[j] o[i] * o[j] shr(o[i], o[j]) shl(o[i], o[j]) byte(o[i], o[j]) lt / gt / eq rotl64 / rotr64 variants ``` 이 단계에서 많은 산술, 논리, 이동 연산이 정리됩니다. 여기서 끝나지 않는 handler는 비트 필드 조립이나 바이트 단위 섞기 계열로 넘어갑니다. ### 5.3 비트 필드 조립 많은 handler는 형태는 다음과 같습니다. ```text acc | (((src >> shift_a) & mask) << shift_b) ``` 여기서 `src`, `shift_a`, `shift_b`, `mask`, `acc` 후보를 바꿔가며 탐색합니다. 이동량은 상수일 수도 있고, 피연산자나 스크래치 슬롯에서 온 값일 수도 있습니다. 이 계열은 VM이 큰 256비트 값을 여러 조각으로 재배치할 때 자주 등장합니다. 출력 레지스터 상위 128비트를 만들기 전후에서 이런 조립 연산이 많이 보입니다. ### 5.4 선형식과 작은 shift 수식 일부 바이트 섞기 handler는 비트 단위 선형식으로 맞습니다. 입력 비트를 변수로 두고 GF(2) 가우스 소거를 돌려 출력 비트를 복원합니다. 또 일부 handler는 shift 값이 입력값의 간단한 일차식으로 표현됩니다. 특정 입력에 작은 계수를 곱하고 상수를 더해 shift 값을 만드는 형태입니다. ```text shift = a * o[i] + b shift = a * o[i] + b * o[j] + c ``` 이 경우도 가능한 계수를 찾은 뒤 모든 샘플에서 다시 검증합니다. ### 5.5 기존 의미 재사용 challenge 3과 4는 전체 구조가 거의 같지만 명령어 번호 배치가 다릅니다. 그래서 이미 복원한 challenge 1, 2의 handler 의미를 후보 풀로 두고, 새 challenge의 `(idx, f7)` 샘플이 어떤 기존 의미와 일치하는지 비교합니다. ```text new_key -> existing_semantic(old_idx, old_f7) ``` 이 방식으로 대부분의 handler를 빠르게 정리할 수 있습니다. 다만 기존 의미 재사용도 어디까지나 후보일 뿐이므로, 실제 trace 출력과 맞지 않으면 폐기합니다. `kind`는 이렇게 여러 복원 결과를 같은 인터페이스로 묶습니다. 이 구조 덕분에 concrete 검증과 SMT 생성에서 같은 의미 테이블을 재사용할 수 있습니다. ```python if kind[0] == "gfmix_red": return gfmix_red(o) if kind[0] == "alias": return eval_known_handler(kind[1], o) if kind[0] == "template": return apply_template(kind[1], o) if kind[0] == "linear": return apply_linear_model(kind[1], kind[2], o) if kind[0] == "bitfield": return apply_bitfield_model(kind[1], kind[2], o) if kind[0] == "shift": return apply_shift_model(kind, o) ``` ## 6. 출력 슬라이스만 남기기 전체 trace는 매우 깁니다. 하지만 최종 출력에 실제로 영향을 주는 명령어만 SMT에 넣으면 됩니다. 마지막 반환 직전의 root register를 찾고, 그 register에 대한 역방향 의존성 슬라이스를 만듭니다. 각 challenge의 root register는 다음과 같습니다. ```text challenge 2: root = reg251 >> 128 before pos 91743 challenge 3: root = reg250 >> 128 before pos 92478 challenge 4: root = reg239 >> 128 before pos 88031 ``` 슬라이스는 root register에서 시작해서 trace를 거꾸로 훑는 방식으로 만듭니다. 어떤 instruction이 필요한 register, scratch, bank 값을 쓰면 그 위치를 남기고, 그 instruction의 source를 다시 필요한 값으로 추가합니다. ```python needed = {("r", root_register)} out = [] for inst in reversed(program[:root_pos]): writes = values_written_by(inst) hit = writes & needed if not hit: continue out.append(inst) needed -= hit needed |= values_read_by(inst) ``` challenge 4의 마지막 부분은 다음처럼 보입니다. ```text pos 88029: idx201 dst 239 out = pos 88031: idx300 dst 1 return store ``` 따라서 심볼릭 출력은 `reg239`의 상위 128비트입니다. ```text output = Extract(255, 128, reg239) ``` 이 슬라이스 덕분에 전체 VM을 전부 심볼릭으로 처리하지 않고, 타겟에 필요한 부분만 SMT로 만들 수 있습니다. ## 7. WRONG / UNFIT 검증 handler 의미를 어느 정도 복원한 뒤에는, 복원한 식을 실제 trace에 다시 적용하는 검증기를 만듭니다. 검증기는 각 trace 행을 보면서 현재 모델이 계산한 값과 실제 출력값을 비교합니다. 이때 단순히 아직 모르는 handler가 남았는지만 보는 것으로는 부족합니다. 모르는 것과 틀린 것은 다르기 때문입니다. 그래서 검증 로그에서는 두 상태를 분리합니다. ```text WRONG: handler 식은 존재하지만 계산값이 실제 trace 출력과 다름 UNFIT: 아직 handler 식을 붙이지 못함 ``` 의미는 다음과 같습니다. ```text WRONG > 0: 의미 모델이 틀림 WRONG = 0, UNFIT > 0: 틀렸다고는 못 하지만 아직 미복원 구간이 있음 WRONG = 0, UNFIT = 0: 해당 trace 묶음 기준으로 의미 모델이 모두 맞음 ``` 여기서 `WRONG`은 세운 가설이 실제 trace와 충돌했다는 뜻입니다. 반면 `UNFIT`은 아직 식을 붙이지 못한 구간이 남았다는 뜻입니다. 이 둘을 분리해두면, 복원 작업 중 어디를 의심해야 하는지 훨씬 명확해집니다. 검증기는 실제로 계산값과 trace 값을 바로 비교합니다. 식이 없으면 `UNFIT`, 식은 있는데 값이 다르면 `WRONG`으로 분리합니다. ```python comp = eval_handler(challenge, idx, fields, operands, trace_out, bank, H, plaintext) expected = trace_row.output ^ H if comp is None: mism.append((pos, idx, fields[7], "UNFIT")) comp = expected elif comp != expected and destination != 1: mism.append((pos, idx, fields[7], "WRONG")) comp = expected ``` ## 8. challenge 1/2: cut-state와 raw return 앞에서 설명한 trace 정규화, handler 복원, WRONG/UNFIT 검증은 네 challenge 모두에 같은 방식으로 적용합니다. 다만 challenge 1과 2는 성격이 조금 달랐습니다. challenge 1은 가장 먼저 잡은 모델이라 전체를 한 번에 SMT로 던지기보다 출력 직전 구간을 여러 번 잘라 보면서 풀었습니다. challenge 2는 V-space 출력과 실제 runner가 비교하는 raw 출력이 달라서, 마지막 제약을 세우기 전에 그 차이를 정리해야 했습니다. challenge 1에서는 마지막 출력으로 이어지는 suffix를 먼저 닫았습니다. 여기서 cut은 특정 trace 위치에서 실행을 끊고, 그 뒤 suffix가 요구하는 live state를 먼저 구한 뒤, 그 state를 다시 평문 비트의 제약으로 되돌리는 방식입니다. 타겟이 요구하는 중간 상태는 다음처럼 정리됩니다. ```text at 84001: reg244 = 0x8950000000000000 reg252 = 0xa83c284cfcf8ec0e bank579 = 0xb4c3558c1cd6255c at 87375: reg240 = 0x957f70853cbc6ce3 bank837 = 0xe392370516736877 ``` 이 값들은 임의로 고른 중간값이 아니라, `target_1`을 출력 suffix에 넣고 역으로 풀었을 때 필요한 state입니다. 이후 앞쪽 구간은 평문 비트에 이름을 붙인 CNF로 내보내 SAT solver에 넘겼습니다. ```bash python3 exploit.py export-cut 1 84001 challenge1_cut_84001.cnf python3 exploit.py export-cut 1 87375 challenge1_cut_87375.cnf ``` 이 방식으로 얻은 challenge 1 평문은 다음과 같습니다. ```text pt1 = 0968e0b6a42a7253f9b3bdca8f98bda7 ``` challenge 2는 challenge 1의 handler 의미를 많이 재사용할 수 있었지만, 마지막 출력 해석에서 한 번 삐끗하기 쉬운 구조였습니다. 특수 명령어와 root register는 다음과 같습니다. ```text table word lookup : idx293 calldata read : idx294 return store : idx292 root : reg251 >> 128 before pos : 91743 ``` 중요한 점은 모델이 처음에 반환하던 값이 runner가 비교하는 raw return이 아니라 `V_out`이었다는 것입니다. 실제 반환값은 마지막에 다시 `H`가 섞입니다. ```text reg251_final_raw = (V_out 5f72fa8e25a8a05cb468ada964fb07e6 random-1 -> df788aa6b9c8e6f050c2d329421d6a19 random-2 -> 62b3cb05e89d00e6d3019cd28677d2f6 random-3 -> 26a2f8c7d3c9aac7c77824af6c2bf64e ``` 모든 trace에서 다음 상태가 됩니다. ```text WRONG = 0 UNFIT = 0 ``` 이후 타겟 SMT를 만들고 solver로 역상을 얻습니다. ```bash python3 exploit.py export-smt 3 \ cc07fb3d2216fc7b0aeca4d3cced2095 \ challenge3_target.smt2 bitwuzla -m --print-model --bv-output-format 16 challenge3_target.smt2 ``` 결과는 다음과 같습니다. ```text pt3 = 6e5c4f1a88d3ec6fb429377d551ab38a ``` 실제 컨트랙트로 다시 검증합니다. ```text input = 6e5c4f1a88d3ec6fb429377d551ab38a output = cc07fb3d2216fc7b0aeca4d3cced2095 ``` ## 10. challenge 4: 잘못된 피팅 잡기 challenge 4는 위에서 정리한 실행 파라미터를 그대로 사용합니다. 문제는 handler 복원이 끝난 것처럼 보인 뒤에 나왔습니다. 초기에는 6개 trace 기준으로 모델이 맞는 것처럼 보였습니다. ```text zero, one-bit, ff, random-1, random-2, random-3 ``` `zero`와 `ff` 심볼릭 검사도 맞았습니다. 그런데 타겟 SMT를 넣자 `unsat`이 나왔습니다. 이 상황에서 가능한 해석은 두 가지였습니다. 1\. 실제 타겟이 도달 불가능한 값입니다. 2\. 샘플이 부족해서 어떤 handler가 우연히 잘못 피팅되었습니다. 실행기의 타겟이 실제 문제 조건이므로 첫 번째 가능성은 낮다고 보았습니다. 그래서 검증 벡터를 더 추가했습니다. ```text additional-1 -> 8bf40ffb23dfb018ae74c82201dbd285 additional-2 -> b3148454ed107cb44c4ffa92418c4a89 additional-3 -> 5471c5baab1369aa2cc9dab6c1266342 additional-4 -> 115d715f15ef25938962cfb8146eb61a ``` 추가 검증에서 바로 문제가 드러났습니다. ```text WRONG key = (75, 0x0c5a) ``` 이 키는 초기 6개 샘플만으로는 선형식처럼 보였지만, 추가 샘플에서는 깨졌습니다. 실제로는 challenge 3에서 본 것과 같은 `gfmix_red` 계열이었습니다. challenge 4에서 `gfmix_red`가 필요한 키는 최종적으로 다음과 같았습니다. ```text (196, 0x13cc) (269, 0x0c01) (14, 0x1376) (285, 0x1320) (73, 0x0ba6) (75, 0x0c5a) ``` 수정 후 10개 trace 전체에서 검증합니다. ```text zero WRONG=0 UNFIT=0 one-bit WRONG=0 UNFIT=0 ff WRONG=0 UNFIT=0 random-1 WRONG=0 UNFIT=0 random-2 WRONG=0 UNFIT=0 random-3 WRONG=0 UNFIT=0 additional-1 WRONG=0 UNFIT=0 additional-2 WRONG=0 UNFIT=0 additional-3 WRONG=0 UNFIT=0 additional-4 WRONG=0 UNFIT=0 ``` 이후 SMT를 다시 만듭니다. ```bash python3 exploit.py export-smt 4 \ fe1815270a539cc1155e320b92aef397 \ challenge4_target.smt2 bitwuzla -m --print-model --bv-output-format 16 challenge4_target.smt2 ``` 결과는 다음과 같습니다. ```text pt4 = f1c82a1d2113ce6601a4694542d3c1e8 ``` 실제 컨트랙트로 다시 검증합니다. ```text input = f1c82a1d2113ce6601a4694542d3c1e8 output = fe1815270a539cc1155e320b92aef397 ``` ## 11. solver 구조와 SMT 모델 풀이용 스크립트는 최종적으로 `exploit.py`라는 이름으로 정리했습니다. 이 스크립트는 단순히 SMT 파일만 찍는 코드가 아니라, trace 검증부터 모델 생성까지 같은 의미 테이블을 공유하도록 구성합니다. 대략적인 구성은 다음과 같습니다. ```text trace 파서: DEC 행을 읽고 idx 보정, H 계산, V-space 변환을 수행 구체 실행기: 복원된 handler 의미로 실제 trace를 다시 실행 regs, scratch, bank, table 상태를 256비트 값으로 유지 검증기: trace 출력과 실행기 출력을 비교 WRONG / UNFIT 개수를 출력 SMT 생성기: 16바이트 평문을 심볼릭 바이트로 두고 같은 handler 의미를 SMT-LIB 비트벡터 식으로 변환 ``` 명령행 모드는 challenge마다 조금 다릅니다. challenge 1은 cut-state를 CNF로 내보내고, challenge 2는 raw return까지 반영한 SMT를 사용합니다. challenge 3과 4는 같은 생성 경로를 공유합니다. 그래서 같은 검증 루틴으로 trace 전체를 먼저 통과시킨 뒤, 같은 코드 경로에서 타겟 제약을 내보냅니다. ```bash python3 exploit.py export-cut 1 84001 challenge1_cut_84001.cnf python3 exploit.py export-cut 1 87375 challenge1_cut_87375.cnf python3 exploit.py export-smt 2 \ e78b91ff6200517467b1e55a85a44742 \ challenge2_target.smt2 python3 exploit.py check-model 3 python3 exploit.py check-model 4 python3 exploit.py export-smt 3 TARGET_HEX challenge3_target.smt2 python3 exploit.py export-smt 4 TARGET_HEX challenge4_target.smt2 ``` 명령어 이름은 다르지만 내부에서는 같은 두 단계로 흘러갑니다. ```text 1. 복원한 의미로 trace 전체를 다시 실행해 WRONG/UNFIT을 확인 2. 같은 의미 테이블을 비트벡터 식으로 바꾸고 타겟 제약식을 출력 ``` challenge 3/4의 SMT 생성도 별도의 모델을 새로 만든 것이 아니라, 검증에 사용한 실행 흐름을 Z3/SMT 식으로 바꾼 형태입니다. 슬라이스에 포함된 instruction만 순서대로 실행하고, 마지막에 root register의 상위 128비트를 반환합니다. ```python plaintext = [BitVec(f"pt{i}", 8) for i in range(16)] for inst in output_slice: operands = read_operands(state, inst) value = symbolic_eval(inst, operands, plaintext) write_destination(state, inst, value) return Extract(255, 128, state[root_register]), plaintext ``` 구체 의미가 검증된 뒤, 같은 식을 비트벡터 식으로 옮깁니다. 평문은 16개의 8비트 심볼릭 바이트입니다. ```python pt0, pt1, ..., pt15 = BitVec(8) ``` VM 레지스터, 스크래치 슬롯, 동적 뱅크는 256비트 식으로 유지합니다. ```text regs[0..255] : 256-bit expressions scratch : 256-bit expressions bank : 256-bit expressions ``` 테이블 조회는 바이트 배열로 모델링합니다. ```text table_byte : Array[16-bit address] -> 8-bit value table_word(addr) = concat(table_byte(addr + 0), ..., table_byte(addr + 31)) ``` 타겟 제약은 단순합니다. ```text output == target ``` SMT 파일을 만들 때는 이 제약을 assert로 넣고, 16개의 평문 바이트 값을 모델에서 출력하도록 합니다. ```python output, plaintext = build_symbolic_model(challenge) constraint = (output == target) fp.write("(assert ") fp.write(constraint.sexpr()) fp.write(")\n") fp.write("(check-sat)\n") fp.write("(get-value (") fp.write(" ".join(p.decl().name() for p in plaintext)) fp.write("))\n") ``` 생성된 SMT 파일은 꽤 컸습니다. ```text challenge 3 SMT: 약 193 MB challenge 4 SMT: 약 300 MB ``` 하지만 출력 슬라이스를 줄여둔 덕분에 bitwuzla로 풀 수 있습니다. ## 12. 전체 결과 네 challenge의 최종 평문은 다음과 같습니다. ```text pt1 = 0968e0b6a42a7253f9b3bdca8f98bda7 pt2 = 3b5a0b3f4e5183fb39642d8c60828660 pt3 = 6e5c4f1a88d3ec6fb429377d551ab38a pt4 = f1c82a1d2113ce6601a4694542d3c1e8 ``` 실행기 검증은 다음과 같습니다. ```bash docker run --rm \ -e NEVM_DIR=rev_nevm \ -v /path/to/rev_nevm:/nevm:ro \ -w /nevm \ nevm solve \ 0968e0b6a42a7253f9b3bdca8f98bda7 \ 3b5a0b3f4e5183fb39642d8c60828660 \ 6e5c4f1a88d3ec6fb429377d551ab38a \ f1c82a1d2113ce6601a4694542d3c1e8 ``` 출력은 다음과 같습니다. ```text contract 1: ok contract 2: ok contract 3: ok contract 4: ok SEKAI{32a1544c3991ef4ad7124990ebbda67c0f19c9bb63e0e9587f03a0b02} ``` ## 13. 마무리 이 문제는 거대한 EVM 바이트코드를 그대로 해석하는 문제가 아니라, 그 안에 구현된 내부 VM을 찾아내고 믿을 수 있는 중간 표현으로 바꾸는 문제였습니다. 실행 조건을 정리하고, trace를 만들고, 명령어 의미를 하나씩 검증한 뒤, 필요한 부분만 SMT로 넘기는 방식으로 문제를 줄일 수 있었습니다. 풀면서 가장 크게 느낀 점은, 어려운 리버싱 문제에서는 빠르게 가설을 세우는 것보다 그 가설이 틀렸음을 빨리 확인할 수 있는 구조가 더 중요하다는 점이었습니다. challenge 4에서 초반 샘플만 믿고 넘어갔다면 계속 엉뚱한 SMT 결과만 보았을 가능성이 높았습니다. 또 하나 느낀 점은, 큰 문제일수록 한 번에 전체를 이해하려고 하면 오히려 길을 잃기 쉽다는 것입니다. 믿을 수 있는 trace, 검증 가능한 handler 의미, 필요한 출력 슬라이스처럼 작은 단위를 쌓아가면, 처음에는 막막해 보이던 문제도 점점 계산 가능한 형태가 됩니다. 결국 이 문제에서 중요한 것은 특별한 한 줄짜리 트릭이 아니었습니다. 모르는 것을 모르는 상태로 남겨두고, 틀린 것을 틀렸다고 표시하고, 맞는 것만 다음 단계로 넘기는 과정이었습니다. 이런 검증 중심의 흐름이 없었다면, 70MB라는 크기보다 잘못된 확신이 더 큰 장애물이 되었을 것 같습니다.