[rev] SekaiCTF 2026 - nevm Writeup
Overview
SekaiCTF 2026 rev/nevm is a reversing challenge built around EVM bytecode in the 70 MB range. The description makes it look like an ordinary EVM contract, but the actual target is a separate VM implemented inside EVM.
The core idea is not to read the entire EVM bytecode directly. Instead, I built traces of the internal VM, recovered the semantics of its instruction handlers, validated those semantics against real contract outputs, and finally generated SMT constraints to recover four 16-byte plaintexts.
Challenge structure
The challenge description was short.
just your average 70 mb evm contract
The distributed files are roughly structured like this.
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 only mentions that the challenge was inspired by Loki and should be run through ./run.sh. Most of the actual challenge logic is in build/runner/src/main.rs.
The files are named challenge_1.bin through challenge_4.bin, so I will refer to the four contracts as challenge 1 through challenge 4. They are different EVM bytecodes, but the runner calls all of them in the same way and compares each return value against a fixed target.
run.sh prepares a Docker image and forwards the arguments to the runner. So the reversing target is not only the bytecode itself, but also the runner logic that defines how each bytecode is called and checked.
1. Runner analysis
The goal becomes clear once we look at build/runner/src/main.rs.
The runner's solve mode takes four plaintexts. It then reads challenge_1.bin through challenge_4.bin and runs each challenge with the corresponding plaintext.
for (i, pt) in plaintexts.iter().enumerate() {
let n = i + 1;
let code = fs::read(format!("{dir}/challenge_{n}.bin")).expect("read challenge");
...
}
The solve command only runs when exactly four plaintexts are provided.
[cmd, pts @ ..\] if cmd == "solve" && pts.len() == 4 => solve(pts),
Each contract receives calldata in this form.
calldata = 20 bytes zero || 16 bytes plaintext
The runner compares the first 16 bytes of return data with TARGETS[i].
if run_contract(code, calldata)[..16] == TARGETS[i] {
eprintln!("contract {n}: ok");
}
The reason there are four targets is visible in the runner. TARGETS contains four 16-byte arrays, and the runner uses the target at the same index as the currently loaded challenge_{n}.bin.
target_1 = ba9383cedce86c2fed648b9d172ea216
target_2 = e78b91ff6200517467b1e55a85a44742
target_3 = cc07fb3d2216fc7b0aeca4d3cced2095
target_4 = fe1815270a539cc1155e320b92aef397
After all four plaintexts are found, the runner concatenates the 64 bytes and decrypts the flag blob with a keccak-based keystream.
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]
So the challenge can be viewed as four independent equations.
F_i(plaintext_i)\[0:16\] == target_i
Each plaintext is 16 bytes.
2. Not EVM
This is not an EVM problem. It is a VM problem.
At first, the challenge looks like a direct EVM reversing task. But once the execution flow is followed, the real logic is handled by an internal VM implemented on top of EVM.
I initially tried to follow the EVM-level control flow directly, but the bytecode size and dispatcher structure made that approach unhelpful very quickly. Each contract is around 70 MB, and this is not the kind of EVM target where reading a decompiler output is enough.
The execution has two main layers.
EVM bytecode
└─ first layer decrypt / setup
└─ internal VM dispatcher
└─ VM instruction stream
└─ register / scratch / bank / table / calldata operations
The important shift is to recover the format and semantics of the internal VM instructions, not the meaning of every EVM instruction.
Each internal VM instruction roughly contains:
opcode index
destination register
source register 0..3
immediate / selector fields
I configured traces to print each VM instruction in the following form.
DEC <pos> idx<opcode> dst <dst> f=<8 fields>
s0=<decoded source0>
s1=<decoded source1>
s2=<decoded source2>
s3=<decoded source3>
out=<decoded output>
This is an excerpt from the final return path of challenge 4.
DEC 88029 idx201 dst 239 f=201,239,240,239,1,1,0,2996
s0=0x0000...65099407f34340fdb4e7cb9b7b667a6d
s1=0x0000...0000000000000080
out=0x65099407f34340fdb4e7cb9b7b667a6d0000...
Here, idx201 is the VM instruction number, dst 239 is the destination register, and f[2]..f[5] are used as source registers.
3. Trace alignment
Each challenge needed a different decode constant and instruction-number offset.
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 is the challenge-specific constant used to decode trace values. offset is subtracted from instruction numbers so that the same VM operation can be compared under a common index across challenges.
Traces are generated in this form. I kept the output files in the same working directory as the analysis script.
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 is especially important. From challenge 2 onward, the same handler meaning appears under shifted instruction numbers. Without normalizing this offset, the same operation looks like different handlers.
I did spend time comparing traces before taking the offset seriously enough. Once the instruction numbers were normalized, the shared structure between challenges became much clearer.
4. V-space normalization
The decoded trace sources and outputs are still masked if read directly. However, for each trace, one value H makes most operations much cleaner.
H = first_decoded_output ^ 0xc0de
V(x) = x ^ H
After this, I work with sources, scratch slots, and outputs in V-space.
H is recomputed per trace. Values from different inputs are not compared directly; each trace is first unmasked with its own H, and only then are handler inputs and outputs compared. With this normalization, basic operations such as XOR, ADD, and SHIFT start to look like their original forms.
For one trace row with sources s0, s1, s2, s3 and output out, the model input is:
o0 = V(s0)
o1 = V(s1)
o2 = V(s2)
o3 = V(s3)
result = V(out)
Scratch slots are kept in the same space.
scratch[0x19] = V(saved value)
scratch[0x1a] = V(saved value)
scratch[0x1b] = V(saved value)
scratch[0x1c] = V(saved value)
The final tuple used for handler semantic recovery is:
o = (
V(s0), V(s1), V(s2), V(s3),
scratch_0x19, scratch_0x1a, scratch_0x1b, scratch_0x1c,
f6, f7, H
)
The concrete checker builds the same tuple. It derives H from the first trace output and then gathers register and scratch values into the handler input o.
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,
)
After normalization, the basic instructions become straightforward.
idx5 : xor
idx3 : add
idx8 : scratch save
idx9 : dynamic bank write
idx10 : dynamic bank read
Table lookup, calldata read, and return store have challenge-specific instruction numbers, but their meaning is shared.
5. Handler Semantics Recovery
Handler recovery is the most important part of the solve. The goal is not just to find formulas that fit a few samples. The recovered semantics must be checked continuously against actual trace values.
Each handler is keyed by (idx, f7).
key = (idx, f7)
sample = (o, V(out))
Collecting all trace rows with the same key gives pairs of input tuples and expected outputs. Candidate formulas are generated from these pairs and kept only if they satisfy all samples.
Recovered handlers are evaluated through one dispatch function. Special instructions such as table read, calldata read, and bank read are handled first. Everything else is evaluated through the recovered meaning for (idx, f7). If the function returns None, the handler is still unrecovered and will be counted as UNFIT during validation.
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 Sample collection
For each decoded trace, I collect:
handler key = (idx, f7)
handler input = (V(s0), V(s1), V(s2), V(s3), scratch slots, f6, f7, H)
handler expected = V(out)
Once this structure is available, handler recovery becomes the problem of finding a function f(o) that satisfies every sample for a given key.
If a candidate function fails even one sample, it is discarded. Some candidates fit early samples but broke on additional validation vectors later, so I kept recovery and validation as separate phases.
5.2 Basic templates
I started with simple operations. This list is not a fixed semantic table; it is a set of candidate templates tested against handler samples.
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
This resolves many arithmetic, logical, and shift operations. Handlers that do not fit here move on to bitfield assembly or byte-mixing families.
5.3 Bitfield assembly
Many handlers fit this shape:
acc | (((src >> shift_a) & mask) << shift_b)
I searched over candidates for src, shift_a, shift_b, mask, and acc. The shift amount can be a constant, an operand, or a value from a scratch slot.
This family appears often when the VM rearranges fragments of 256-bit values. These assembly operations show up frequently around the point where the upper 128 bits of the output register are formed.
5.4 Linear models and small shift formulas
Some byte-mixing handlers fit bit-level linear models. I treated input bits as variables and used Gaussian elimination over GF(2) to recover output bits.
Some other handlers compute shift amounts with simple first-degree expressions over the inputs. In other words, they multiply an input by a small coefficient and add a constant to produce the shift value.
shift = a * o[i] + b
shift = a * o[i] + b * o[j] + c
These candidates are also rechecked against every sample after the coefficients are found.
5.5 Reusing existing semantics
Challenge 3 and challenge 4 have almost the same overall structure, but their instruction-number layout differs. I used the recovered semantics from challenge 1 and challenge 2 as a candidate pool, then checked whether each new (idx, f7) sample matched an existing meaning.
new_key -> existing_semantic(old_idx, old_f7)
This resolves most handlers quickly. Still, reuse is only a candidate; if it disagrees with real trace output, it is discarded.
kind is the interface that keeps the different recovery results behind one evaluator. This lets concrete validation and SMT generation reuse the same semantic table.
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. Keeping only the output slice
The full trace is very long. For SMT, only instructions that affect the final output are needed.
I first locate the root register immediately before return, then build a backward dependency slice for that register.
The root registers are:
challenge 2:
root = reg251 >> 128
before pos 91743
challenge 3:
root = reg250 >> 128
before pos 92478
challenge 4:
root = reg239 >> 128
before pos 88031
The slice starts from the root register and walks the trace backward. If an instruction writes a needed register, scratch slot, or bank entry, that instruction is kept, and its sources are added to the needed set.
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)
The end of challenge 4 looks like this:
pos 88029: idx201 dst 239 out = <128-bit output || 16 zero bytes>
pos 88031: idx300 dst 1 return store
So the symbolic output is the upper 128 bits of reg239.
output = Extract(255, 128, reg239)
This slice keeps the SMT model focused on the path that actually affects the target.
7. WRONG / UNFIT validation
Once handler semantics are mostly recovered, I run a checker that applies the recovered formulas back to the actual traces.
The checker compares the model output for each trace row against the real trace output. It is not enough to count unknown handlers. Unknown and wrong are different failure modes.
So the validation log separates two states.
WRONG:
a handler formula exists, but its value disagrees with the trace
UNFIT:
no formula has been assigned to the handler yet
The interpretation is:
WRONG > 0:
the semantic model is wrong
WRONG = 0, UNFIT > 0:
the model has not been proven wrong, but unrecovered regions remain
WRONG = 0, UNFIT = 0:
for those traces, the recovered semantics match completely
WRONG means the current hypothesis conflicts with the trace. UNFIT means a missing handler remains. Keeping them separate makes it much easier to decide what to distrust.
The checker performs the comparison directly. Missing formulas become UNFIT; formulas that compute a different value become WRONG.
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 and raw return
The normalization, handler recovery, and WRONG/UNFIT validation described above apply to all four challenges. Challenge 1 and challenge 2 had slightly different solve paths.
For challenge 1, which was the first model I built, solving the whole program in one SMT query was not the most practical path. I cut the program near the output path several times and worked backward from the suffix.
Here, a cut means stopping execution at a trace position, solving for the live state required by the suffix, and then turning that state back into constraints on plaintext bits.
The target-required intermediate state was:
at 84001:
reg244 = 0x8950000000000000
reg252 = 0xa83c284cfcf8ec0e
bank579 = 0xb4c3558c1cd6255c
at 87375:
reg240 = 0x957f70853cbc6ce3
bank837 = 0xe392370516736877
These are not arbitrary intermediate values. They are the states required when target_1 is propagated backward through the output suffix. The earlier prefix was then emitted as a CNF problem with named plaintext bits and solved with a SAT solver.
python3 exploit.py export-cut 1 84001 challenge1_cut_84001.cnf
python3 exploit.py export-cut 1 87375 challenge1_cut_87375.cnf
This gives the challenge 1 plaintext:
pt1 = 0968e0b6a42a7253f9b3bdca8f98bda7
Challenge 2 reused much of the challenge 1 handler semantics, but the last output interpretation was easy to get wrong. Its special instructions and root register are:
table word lookup : idx293
calldata read : idx294
return store : idx292
root : reg251 >> 128
before pos : 91743
The important detail is that the model initially returned V_out, not the raw return value compared by the runner. The raw output mixes H back in at the end.
reg251_final_raw = (V_out << 128) ^ H
raw_top128 = V_out ^ H_top128
After accounting for this, the final challenge 2 segment reduces to a 64-bit ARX tail.
y1 = x0 ^ rol64(y0, 5)
x1 = y1 + ror64(x0, 6)
x2 = x1 ^ 0xbdea9acd5460b5ec
y2 = x2 ^ rol64(y1, 5)
x3 = y2 + ror64(x2, 6)
x4 = x3 ^ 0x73a8e47aa178d197
y3 = x4 ^ rol64(y2, 5)
V_out = (x4 << 64) | y3
raw = V_out ^ H_top128
This expression was checked against several samples for both V_out and raw return.
zero : V/raw both match
one-bit : V/raw both match
ff : V/raw both match
random-1 : V/raw both match
random-2 : V/raw both match
random-3 : V/raw both match
The challenge 2 plaintext is:
pt2 = 3b5a0b3f4e5183fb39642d8c60828660
I also checked it against the actual contract output.
input = 3b5a0b3f4e5183fb39642d8c60828660
output = e78b91ff6200517467b1e55a85a44742
9. challenge 3: gfmix_red
Challenge 3 and challenge 4 share the same generation path, so I first summarized their execution parameters.
challenge 3:
table word lookup = idx287
calldata read = idx288
return store = idx286
root register = reg250
root position = 92476
challenge 4:
table word lookup = idx301
calldata read = idx302
return store = idx300
root register = reg239
root position = 88029
These values determine table lookup, calldata read, return store, and the root register. They are not arbitrary trace positions; they are the parameters used by the validator and the SMT generator.
Most handlers were resolved by reusing existing semantics. The remaining unrecovered keys on the output slice all belonged to the same byte-reduction family.
Instead of forcing a different formula for each key, I grouped the repeated pattern as gfmix_red. Once a key is marked as gfmix_red, both concrete execution and SMT generation use the same semantic function.
def eval_semantics(kind, operands):
if kind[0] == "gfmix_red":
return gfmix_red(operands)
The core formula is:
def gfmix_red(o):
return (
o[0] ^ o[1] ^ o[2] ^ o[3]
^ ((o[3] << o[4]) & o[5])
^ (o[7] if o[6] else 0)
) & 0xff
This XORs four input bytes, conditionally mixes a shifted value, and reduces the result to one byte. Some early samples could be explained by a generic linear candidate, but the repeated pattern on the output path made this reduction function the better model.
Challenge 3 needed this function for six keys.
(143, 0x655a)
(34, 0x6664)
(150, 0x6cec)
(273, 0x6d98)
(267, 0x65b4)
(248, 0x6c96)
The validation vectors were:
zero -> 216f2955f50ed883013ac022f7f65288
one-bit -> 8d4f5e4d24016e0483780f7d6b28c2db
ff -> 5f72fa8e25a8a05cb468ada964fb07e6
random-1 -> df788aa6b9c8e6f050c2d329421d6a19
random-2 -> 62b3cb05e89d00e6d3019cd28677d2f6
random-3 -> 26a2f8c7d3c9aac7c77824af6c2bf64e
All traces reached:
WRONG = 0
UNFIT = 0
Then I generated the target SMT and solved for a preimage.
python3 exploit.py export-smt 3 \
cc07fb3d2216fc7b0aeca4d3cced2095 \
challenge3_target.smt2
bitwuzla -m --print-model --bv-output-format 16 challenge3_target.smt2
The result was:
pt3 = 6e5c4f1a88d3ec6fb429377d551ab38a
I checked it against the actual contract output.
input = 6e5c4f1a88d3ec6fb429377d551ab38a
output = cc07fb3d2216fc7b0aeca4d3cced2095
10. challenge 4: catching a false fit
Challenge 4 uses the execution parameters listed above. The problem appeared after the model seemed complete.
The first six traces looked correct.
zero, one-bit, ff, random-1, random-2, random-3
Symbolic checks for zero and ff also matched. But when I added the target SMT constraint, the result was unsat.
There were two possible explanations:
1. The actual target was unreachable.
2. One handler had been accidentally fit to too few samples.
Because the target comes directly from the runner, I treated the first option as unlikely and added more validation vectors.
additional-1 -> 8bf40ffb23dfb018ae74c82201dbd285
additional-2 -> b3148454ed107cb44c4ffa92418c4a89
additional-3 -> 5471c5baab1369aa2cc9dab6c1266342
additional-4 -> 115d715f15ef25938962cfb8146eb61a
The new validation immediately exposed the issue.
WRONG key = (75, 0x0c5a)
This key looked linear under the first six samples, but failed on the additional samples. It was another gfmix_red-style handler.
The final gfmix_red keys for challenge 4 were:
(196, 0x13cc)
(269, 0x0c01)
(14, 0x1376)
(285, 0x1320)
(73, 0x0ba6)
(75, 0x0c5a)
After the fix, all ten traces validated cleanly.
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
Then I regenerated the SMT.
python3 exploit.py export-smt 4 \
fe1815270a539cc1155e320b92aef397 \
challenge4_target.smt2
bitwuzla -m --print-model --bv-output-format 16 challenge4_target.smt2
The result was:
pt4 = f1c82a1d2113ce6601a4694542d3c1e8
I checked it against the actual contract output.
input = f1c82a1d2113ce6601a4694542d3c1e8
output = fe1815270a539cc1155e320b92aef397
11. Solver structure and SMT model
I eventually cleaned the solving script up as exploit.py. It is not just an SMT emitter; it uses one shared semantic table for trace validation and model generation.
The structure is:
trace parser:
read DEC rows, normalize idx, compute H, convert into V-space
concrete executor:
replay the trace using recovered handler semantics
maintain regs, scratch, bank, and table as 256-bit values
validator:
compare trace outputs with executor outputs
report WRONG / UNFIT counts
SMT generator:
represent the 16 plaintext bytes as symbolic bytes
translate the same handler semantics into SMT-LIB bit-vector expressions
The command modes differ slightly by challenge. Challenge 1 emits cut-state CNF, while challenge 2 uses SMT with raw return handling.
Challenge 3 and challenge 4 share the same generation path. They first run the same validation routine over the full traces, then emit target constraints from the same semantic model.
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
The command names differ, but internally the flow is the same:
1. replay the trace with recovered semantics and check WRONG/UNFIT
2. translate the same semantic table into bit-vector expressions and emit the target constraint
The SMT generation for challenge 3/4 is not a separate model. It is the same execution flow converted into Z3/SMT expressions. It executes only the instructions in the output slice and returns the upper 128 bits of the root register.
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
After concrete semantics are validated, the same formulas are moved into bit-vector expressions.
The plaintext is 16 symbolic 8-bit bytes.
pt0, pt1, ..., pt15 = BitVec(8)
VM registers, scratch slots, and dynamic bank entries are kept as 256-bit expressions.
regs[0..255] : 256-bit expressions
scratch : 256-bit expressions
bank : 256-bit expressions
Table lookup is modeled as a byte array.
table_byte : Array[16-bit address] -> 8-bit value
table_word(addr) = concat(table_byte(addr + 0), ..., table_byte(addr + 31))
The target constraint is simple.
output == target
When writing the SMT file, this constraint is asserted and the 16 plaintext bytes are requested from the model.
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")
The generated SMT files were not small.
challenge 3 SMT: about 193 MB
challenge 4 SMT: about 300 MB
But after reducing the model to the output slice, bitwuzla could solve them.
12. Final result
The final plaintexts are:
pt1 = 0968e0b6a42a7253f9b3bdca8f98bda7
pt2 = 3b5a0b3f4e5183fb39642d8c60828660
pt3 = 6e5c4f1a88d3ec6fb429377d551ab38a
pt4 = f1c82a1d2113ce6601a4694542d3c1e8
Runner validation:
docker run --rm \
-e NEVM_DIR=rev_nevm \
-v /path/to/rev_nevm:/nevm:ro \
-w /nevm \
nevm solve \
0968e0b6a42a7253f9b3bdca8f98bda7 \
3b5a0b3f4e5183fb39642d8c60828660 \
6e5c4f1a88d3ec6fb429377d551ab38a \
f1c82a1d2113ce6601a4694542d3c1e8
Output:
contract 1: ok
contract 2: ok
contract 3: ok
contract 4: ok
SEKAI{32a1544c3991ef4ad7124990ebbda67c0f19c9bb63e0e9587f03a0b02}
## 13. Closing
This challenge was not about reading a huge EVM bytecode directly. It was about finding the internal VM inside it and turning that VM into a trustworthy intermediate representation. Once the runner conditions were clear, the rest of the solve became a loop of tracing, semantic recovery, validation, and SMT generation over only the necessary output slice.
The biggest takeaway for me is that in hard reversing tasks, quickly producing a hypothesis is less important than quickly finding out when the hypothesis is wrong. Challenge 4 was the best example: the early samples made one handler look correct, but additional validation exposed the false fit before I wasted more time on a misleading SMT result.
Another thing I was reminded of is that large problems become manageable only after they are broken into units that can be trusted. A trace I can replay, a handler meaning I can validate, and an output slice I can solve are much more useful than a vague understanding of a 70 MB blob.
The important part was not a single trick. It was keeping unknowns unknown, marking wrong assumptions as wrong, and only letting verified pieces move forward.