Hardware Wallet Sudoku: Elliptic Relations Ledger Donjon CTF Writeup
This challenge was the only one in the reverse engineering category of Ledger Donjon CTF. Writeup by rbtree.
Elliptic Relations (300pts)
We found this binary, which seems to come from a well known hardware wallet. We were told it contains a secret. Can you retrieve it?
First looking at this, there are too many syscalls (SVC 1
) which are unknown. After searching, we found out that there’s an emulator for Ledger wallets called speculos, and it was able to figure out how those syscalls work.
For example, look at this syscall function:
.text:C0D012C0 cx_rng_ID_IN ; CODE XREF: sub_C0D01020+8A↑p
.text:C0D012C0
.text:C0D012C0 var_18 = -0x18
.text:C0D012C0 var_14 = -0x14
.text:C0D012C0
.text:C0D012C0 PUSH {R3-R7,LR}
.text:C0D012C2 STR R0, [SP,#0x18+var_18]
.text:C0D012C4 STR R1, [SP,#0x18+var_14]
.text:C0D012C6 LDR R0, =0x6000052C
.text:C0D012C8 MOV R1, SP
.text:C0D012CA BL call_svc_1
.text:C0D012CE LDR R0, [SP,#0x18+var_14]
.text:C0D012D0 ADD SP, SP, #0x10
.text:C0D012D2 POP {R7,PC}
It set R0 = 0x600052C
, and R1 = arguments
. If you look at bolos_syscalls_1.6.h
in speculos, you can find out that this function is cx_rng_ID_IN
, and also figure out how the syscall works by searching cx_rng
.
// bolos_syscalls_1.6.h
...
#define SYSCALL_cx_rng_u32_ID_IN 0x600089ecUL
#define SYSCALL_cx_rng_u32_ID_OUT 0x900089d4UL
#define SYSCALL_cx_rng_ID_IN 0x6000052cUL
#define SYSCALL_cx_rng_ID_OUT 0x90000567UL
#define SYSCALL_cx_hash_ID_IN 0x6000073bUL
...
// emu_cx.c
/* not secure, but this is clearly not the goal of this emulator */
unsigned long sys_cx_rng(uint8_t *buffer, unsigned int length)
{
unsigned int i;
if (!initialized) {
srand(get_rng_seed_from_env("RNG_SEED"));
initialized = true;
}
for (i = 0; i < length; i++) {
buffer[i] = rand() & 0xff;
}
return 0;
}
After renaming all the syscall functions, we found a suspicious function:
int __fastcall sub_C0D000D4(int a1)
{
char *v2; // r7
int v3; // r1
int i; // r5
int v5; // r0
int v6; // r6
int v7; // r0
int v9; // [sp+8h] [bp-98h]
cx_ecfp_256_public_key_s pub_key; // [sp+18h] [bp-88h] BYREF
cx_ecfp_256_private_key_s priv_key; // [sp+64h] [bp-3Ch] BYREF
v2 = &byte_C0D02C29[1];
v3 = 0;
while ( v3 != 27 )
{
v9 = v3;
cx_ecfp_init_private_key_ID_IN(CX_CURVE_SECP256K1, a1 + byte_C0D02C29[9 * v3], 1, (int)&priv_key);
cx_ecfp_generate_pair_ID_IN(CX_CURVE_SECP256K1, (int)&pub_key, (int)&priv_key, 1);
if ( !pub_key.W_len )
return 0;
for ( i = 0; i != 8; ++i )
{
v5 = v2[i];
if ( !*(_BYTE *)(a1 + v5) )
return 0;
cx_ecfp_scalar_mult_ID_IN(LOBYTE(pub_key.curve), (int)pub_key.W, pub_key.W_len, a1 + v5, 1);
}
v6 = 0;
if ( pub_key.W_len == 65 )
{
v7 = sub_C0D02A80(pub_key.W, dword_C0D02D1C, 65);
v2 += 9;
v3 = v9 + 1;
if ( !v7 )
continue;
}
return v6;
}
return 1;
}
It calculates (a1 + byte_C0D02C29[9 * i + 0]) * ... * (a1 + byte_C0D02C29[9 * i + 8]) * G
for each i = 0..26
, and then compare with the point dword_C0D02D1C
. a1
is byte_20001800
, which is 81-bytes. It seems like Sudoku, doesn’t it?
Next, let’s see the setter of byte_20001800
.
int __fastcall set_byte_20001800(unsigned int idx, char value)
{
int v2; // r4
int v6; // [sp+4h] [bp-1Ch] BYREF
_BYTE v7[24]; // [sp+8h] [bp-18h] BYREF
v2 = -1;
if ( idx <= 0x50 && !byte_20001800[idx] )
{
LOBYTE(v6) = 64;
v7[0] = value;
if ( cx_math_is_prime_ID_IN((int)v7, 1) )
{
if ( cx_math_cmp_ID_IN(v7, &v6, 1) < 0 )
{
byte_20001800[idx] = value;
v2 = 0;
}
}
}
return v2;
}
Okay, every value should be a prime number less than 64.
From this, we can brute-force to get a
that dword_C0D02D1C = a * G
.
from ecdsa import VerifyingKey, SECP256k1
from ecdsa.ellipticcurve import Point
from ecdsa.util import sigencode_string
from ecdsa.numbertheory import inverse_mod
with open('elliptic_relations.elf', 'rb') as f:
data = f.read()
byte_C0D02C29 = data[0x12C29:0x12C29 + 9 * 27]
dword_C0D02D1C = data[0x12D1C:0x12D1C + 65]
dword_C0D02C14 = data[0x12C14:0x12C14 + 21]
# primes under 64
primes = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61]
assert max(byte_C0D02C29) == 80
arr = dword_C0D02C14 + b'\x01' * 60
x = 1
unknown = []
for v in byte_C0D02C29[18:27]:
if v <= 20:
print(arr[v])
x *= arr[v]
else:
unknown.append(v)
import itertools
for x1, x2, x3, x4, x5 in itertools.product(primes, repeat=5):
print(x1, x2, x3, x4, x5)
y = x * x1 * x2 * x3 * x4 * x5
point = SECP256k1.generator * y
if dword_C0D02D1C == bytes.fromhex("04{:064x}{:064x}".format(point.x(), point.y())):
print("WOW")
break
After running the script, we got dword_C0D02D1C = 5 * 11 * 13 * 19 * 23 * 31 * 37 * 43 * 53 * G
. Nine different primes. So, Sudoku confirmed.
Flag-printing logic is here (run after sub_C0D000D4
):
int sub_C0D00180()
{
int i; // r0
char v2[124]; // [sp+Ch] [bp-7Ch] BYREF
cx_sha256_init_ID_IN(v2);
cx_hash_ID_IN((int)v2, 1, (int)load_sth, 81, (int)byte_20001A6C, 32);
for ( i = 0; i != 26; ++i )
byte_20001A6C[i] ^= *((_BYTE *)dword_C0D02EFC + i);
return sub_C0D001D0(26, 1);
}
Finally, here is the solver that uses z3 to solve the Sudoku puzzle:
from ecdsa import VerifyingKey, SECP256k1
from ecdsa.ellipticcurve import Point
from ecdsa.util import sigencode_string
from ecdsa.numbertheory import inverse_mod
with open('elliptic_relations.elf', 'rb') as f:
data = f.read()
byte_C0D02C29 = data[0x12C29:0x12C29 + 9 * 27]
assert max(byte_C0D02C29) == 80
dword_C0D02D1C = data[0x12D1C:0x12D1C + 65]
dword_C0D02C14 = data[0x12C14:0x12C14 + 21]
dword_C0D02EFC = data[0x12EFC:0x12EFC + 26]
from z3 import *
primes_to_int = {5: 1, 11: 2, 13: 3, 19: 4, 23: 5, 31: 6, 37: 7, 43: 8, 53: 9}
int_to_primes = [0, 5, 11, 13, 19, 23, 31, 37, 43, 53]
arr = [Int('Arr{}'.format(i)) for i in range(81)]
s = Solver()
for i in range(21):
s.add(primes_to_int[dword_C0D02C14[i]] == arr[i])
for i in range(81):
s.add(And(1 <= arr[i], arr[i] <= 9))
for v3 in range(27):
s.add(Distinct([arr[v] for v in byte_C0D02C29[9 * v3:9 * v3 + 9]]))
if s.check() == unsat:
exit(0)
m = s.model()
ans = bytes(int_to_primes[m[v].as_long()] for v in arr)
import hashlib
hasher = hashlib.sha256()
hasher.update(ans)
hsh = bytearray(hasher.digest())
for i in range(26):
hsh[i] ^= dword_C0D02EFC[i]
print(hsh)
The flag is CTF{r4nD0m1Z3d_sUD0ku_FTW}
.