⚠ Spoiler: Đây là write-up cho các challenge của Flare-on 9 tổ chức vào khoảng tháng 11/2022 tại Website.
[07] anode
You’ve made it so far! I can’t believe it! And so many people are ahead of you!
7-zip password: flare
Công cụ sử dụng:
- Visual Studio Code
- HxD
Level 7 là một binary mà nhìn vào logo và Properties chúng ta có thể đoán ra ngay chúng ta sắp phải đối mặt với gì: NodeJS a.k.a Javascript.
Binary này rất nặng, gần 60MB sau khi giải nén, về cơ bản, đây là file chứa toàn bộ Node interpreter (v8 engine from Google) đã compile cho Windows kèm theo đó là source code node.js để có thể chạy code trên môi trường Windows. Khá là giống với cách làm của PyInstaller của Python.
Thử mở file này bằng HxD, hex editor, chúng ta sẽ thấy rõ hơn:
Phần đầu vẫn là một file PE thông thường. Tuy nhiên, kéo đến gần cuối file ta có thể thấy rõ source code Javascript bằng plain-text:
Chú ý đến cụm nexe~~sentinel ở cuối file, chúng ta sẽ dùng đến ở phần sau:
Trước tiên, chạy thử binary này đã:
Tìm kiếm từ khóa nexe trên Google đưa chúng ta đến với repo của packer này: https://github.com/nexe/nexe
Tiếp tục đọc file https://github.com/nexe/nexe/blob/1eeac1b538098352508b6af77faf71bd2409c55f/src/patches/boot-nexe.ts#L9 cho ta cái nhìn cụ thể hơn về cấu trúc của file:
const fs = require('fs'),
fd = fs.openSync(process.execPath, 'r'),
stat = fs.statSync(process.execPath),
tailSize = Math.min(stat.size, 16000),
tailWindow = Buffer.from(Array(tailSize))
fs.readSync(fd, tailWindow, 0, tailSize, stat.size - tailSize)
const footerPosition = tailWindow.indexOf('<nexe~~sentinel>')
if (footerPosition == -1) {
throw 'Invalid Nexe binary'
}
const footer = tailWindow.slice(footerPosition, footerPosition + 32),
contentSize = footer.readDoubleLE(16),
resourceSize = footer.readDoubleLE(24),
contentStart = stat.size - tailSize + footerPosition - resourceSize - contentSize,
resourceStart = contentStart + contentSize
Phần <nexe~~sentinel> chính là đánh dấu footer của file, sau đó là các số double chỉ rõ kích thước của phần content và phần resource để từ đó ta có thể tính ngược được ra vị trí bắt đầu của các phần này
# File structure
<base compiled nodejs interpreter> <content> <resource> <footer>
Đối với file anode.exe thì phần footer như sau:
| 3C 6E 65 78 65 7E 7E 73 65 6E 74 69 6E 65 6C 3E | 00 00 00 00 00 03 CF 40 | 00 00 00 00 DC A4 13 41 |
<nexe~~sentinel> contentSize resourceSize
Chỉnh sửa 1 chút đoạn code trên đọc vào anode.exe rồi thêm dòng debug vào ta tính ra được các vị trí:
// console.log(contentStart, contentSize, resourceStart, resourceSize)
56490496 15878 56506374 321847
Ở index 56490496 là phần code bootstrap:
Từ index 56506374 là phần code của chúng ta (có thể thấy rõ dòng in ra Try again.)
Đến đây ta có thể extract phần code anode.js ra file, mình sẽ lược bỏ bớt các case vì quá dài (Full source: anode.js):
const readline = require('readline').createInterface({
input: process.stdin,
output: process.stdout,
});
readline.question(`Enter flag: `, flag => {
readline.close();
if (flag.length !== 44) {
console.log("Try again.");
process.exit(0);
}
var b = [];
for (var i = 0; i < flag.length; i++) {
b.push(flag.charCodeAt(i));
}
// something strange is happening...
if (1n) {
console.log("uh-oh, math is too correct...");
process.exit(0);
}
var state = 1337;
while (true) {
state ^= Math.floor(Math.random() * (2**30));
switch (state) {
case 306211:
if (Math.random() < 0.5) {
b[30] -= b[34] + b[23] + b[5] + b[37] + b[33] + b[12] + Math.floor(Math.random() * 256);
b[30] &= 0xFF;
} else {
b[26] -= b[24] + b[41] + b[13] + b[43] + b[6] + b[30] + 225;
b[26] &= 0xFF;
}
state = 868071080;
continue;
case 311489:
if (Math.random() < 0.5) {
b[10] -= b[32] + b[1] + b[20] + b[30] + b[23] + b[9] + 115;
b[10] &= 0xFF;
} else {
b[7] ^= (b[18] + b[14] + b[11] + b[25] + b[31] + b[21] + 19) & 0xFF;
}
state = 22167546;
continue;
...
case 185078700:
break;
...
case 1071767211:
if (Math.random() < 0.5) {
b[30] ^= (b[42] + b[9] + b[2] + b[36] + b[12] + b[16] + 241) & 0xFF;
} else {
b[20] ^= (b[41] + b[2] + b[40] + b[21] + b[36] + b[17] + 37) & 0xFF;
}
state = 109621765;
continue;
default:
console.log("uh-oh, math.random() is too random...");
process.exit(0);
}
break;
}
var target = [106, 196, 106, 178, 174, 102, 31, 91, 66, 255, 86, 196, 74, 139, 219, 166, 106, 4, 211, 68, 227, 72, 156, 38, 239, 153, 223, 225, 73, 171, 51, 4, 234, 50, 207, 82, 18, 111, 180, 212, 81, 189, 73, 76];
if (b.every((x,i) => x === target[i])) {
console.log('Congrats!');
} else {
console.log('Try again.');
}
});
Đọc nhanh đoạn đầu ta thấy flag sẽ phải có độ dài là 44 ký tự, sau đó được lưu vào mảng b. Các phần tử của mảng này chạy qua một loạt các tính toán: cộng, trừ, xor và check với mảng target cuối cùng. Và điều kì lạ xảy ra ở:
// something strange is happening...
if (1n) {
console.log("uh-oh, math is too correct...");
process.exit(0);
}
Rõ ràng 1n là BigInt thì khi convert sang boolean phải ra true và binary sẽ thoát nhưng chạy lại với fake flag có độ dài 44 ký tự vẫn ra Try again. Nhưng nếu chạy script đã extract thì lỗi:
Thử sửa dòng console.log('Try again.'); thành console.log('TRY AGAIN.'); ta thấy binary vẫn chạy ra đúng dòng đã đổi:
Code bao gồm 1025 case khác nhau, có duy nhất một case break ra khỏi switch, state lại được tính toán dựa trên Math.random, dẫn ta đến nghi vấn là author đã patch hoặc làm gì đó với phần <base compiled nodejs interpreter>, làm cho tất cả các lần chạy đều giống nhau bằng cách sửa Math.random khởi tạo với một seed cố định.
state ^= Math.floor(Math.random() * (2**30));
Sửa lại file binary ban đầu để in ra giá trị của state nhưng vẫn đảm bảo độ dài không đổi và đúng syntax, xác nhận giả thuyết của chúng ta là đúng khi state đều không đổi sau mỗi lần chạy:
Do state đã không đổi sau mỗi lần chạy thì việc cần làm đầu tiên là recovery lại các giá trị state cũng như các giá trị output của hàm Math.random do:
statetính toán dựa trênMath.random- Giá trị của các phần tử của
b, rơi vào nhánh nào của if-else cũng phụ thuộc vào giá trị này, ví dụ như ở đây:
if (Math.random() < 0.5) {
b[30] -= b[34] + b[23] + b[5] + b[37] + b[33] + b[12] + Math.floor(Math.random() * 256);
b[30] &= 0xFF;
} else {
b[26] -= b[24] + b[41] + b[13] + b[43] + b[6] + b[30] + 225;
b[26] &= 0xFF;
}
Ta sử dụng một script nhỏ để build ra file binary mới dựa trên phần <base compiled nodejs interpreter> (cắt ra từ binary gốc), phần base.js là phần code bootstrap và phần code.js là phần code của chúng ta đã tùy chỉnh, đồng thời tính toán lại kích thước code mới ở phần footer cho đúng:
import struct
import binascii
def double_to_hex(f):
return struct.unpack('<Q', struct.pack('<d', f))[0]
x = 321847.0
# x = 15878.0
"""
56490496 15878 56506374 321847
contentStart, contentSize, resourceStart, resourceSize
"""
tag = b"<nexe~~sentinel>"
base_binary = open("base.exe", "rb").read()
base_code = open("base.js", "rb").read()
code = open("code.js", "rb").read()
base_code = base_code.replace(b"321847", str(len(code)).encode("utf-8"))
with open("test.exe", "wb") as f:
f.write(base_binary)
f.write(base_code)
f.write(code)
f.write(tag)
f.write(bytearray(struct.pack("d", len(base_code))))
f.write(bytearray(struct.pack("d", len(code))))
Với phần code.js mới, ta sẽ proxy hàm Math.random để mỗi lần gọi hàm sẽ output ra giá trị Math.floor(Math.random() * 256), đồng thời log lại giá trị state và case nào mà code sẽ nhảy vào (Full source: code.js):
const handler = {
apply: function (target, thisArg, argumentsList) {
var ret = target()
// console.log(`Math.random: ${ret}`);
console.log(`Value: ${Math.floor(ret * 256)}`);
return ret
}
};
Math.random = new Proxy(Math.random, handler);
var flag = "abcdefabcdefabcdefabcdefabcdef0@flare-on.com";
// var flag = "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv";
var b = [];
var pre_b = [];
for (var i = 0; i < flag.length; i++) {
b.push(flag.charCodeAt(i));
}
// something strange is happening... abcdefabcdefabcdefabcdefabcdef0@flare-on.com
// abcdefabcdefabcdefabcdefabcdef0@flare-on.com
// aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
if (1n) {
console.log("Case: A")
console.log("uh-oh, math is too correct...");
process.exit(0);
}
var state = 1337;
while (true) {
state ^= Math.floor(Math.random() * (2 ** 30));
console.log(`State: ${state}`)
switch (state) {
case 306211:
if (Math.random() < 0.5) {
console.log("Case: A")
b[30] -= b[34] + b[23] + b[5] + b[37] + b[33] + b[12] + Math.floor(Math.random() * 256);
b[30] &= 0xFF;
} else {
console.log("Case: B")
b[26] -= b[24] + b[41] + b[13] + b[43] + b[6] + b[30] + 225;
b[26] &= 0xFF;
}
state = 868071080;
continue;
...
Chạy thử chúng ra ta output như sau (Full source: result):
Value: 240
State: 1010356043
Value: 224
Case: B
Value: 131
State: 497278214
Case: B
...
Case: B
Value: 50
Value: 188
State: 210975861
Case: B
Value: 208
State: 185078700
Các giá trị state vẫn đúng như ban đầu. Bước tiếp theo là parse output này, thay thế value vào các vị trí Math.random để lấy ra toàn bộ flow đúng (Full source: final.js):
var flag = "abcdefabcdefabcdefabcdefabcdef0@flare-on.com";
var b = [];
for (var i = 0; i < flag.length; i++) {
b.push(flag.charCodeAt(i));
}
b[29] -= b[37] + b[23] + b[22] + b[24] + b[26] + b[10] + 7;
b[29] &= 0xFF;
console.log(`B: ${b}`)
b[39] += b[34] + b[2] + b[1] + b[43] + b[20] + b[9] + 79;
b[39] &= 0xFF;
console.log(`B: ${b}`)
b[19] ^= (b[26] + b[0] + b[40] + b[37] + b[23] + b[32] + 255) & 0xFF;
...
b[22] += b[16] + b[18] + b[7] + b[23] + b[1] + b[27] + 50;
b[22] &= 0xFF;
console.log(`B: ${b}`)
b[39] += b[18] + b[16] + b[8] + b[19] + b[5] + b[23] + 36;
b[39] &= 0xFF;
console.log(`B: ${b}`)
Giờ chúng ta đã có flow đúng, đến đây thì có 2 cách để tính ngược ra kết quả ban đầu:
Cách 1
Nhận thấy là mỗi dòng tính toán chỉ thay đổi đúng một giá trị duy nhất trong mảng b, nên ta có thể coi các giá trị là cố định và thực hiện các phép tính ngược lại theo đúng thứ tự từ cuối về đầu, đảo cộng thành trừ, trừ thành cộng:
Tức là nếu theo chiều tính xuôi, phép biến đổi cuối cùng là:
...
b[39] += b[18] + b[16] + b[8] + b[19] + b[5] + b[23] + 36;
b[39] &= 0xFF;
thì tính ngược lại, biến đổi này sẽ đưa lên đầu vào đổi cộng thành trừ:
var b = [106, 196, 106, 178, 174, 102, 31, 91, 66, 255, 86, 196, 74, 139, 219, 166, 106, 4, 211, 68, 227, 72, 156, 38, 239, 153, 223, 225, 73, 171, 51, 4, 234, 50, 207, 82, 18, 111, 180, 212, 81, 189, 73, 76];
b[39] -= b[18] + b[16] + b[8] + b[19] + b[5] + b[23] + 36;
b[39] &= 0xFF;
...
Chạy script cuối cùng này sẽ cho chúng ta flag (Full source: rev.js):
Cách 2: Giải quyết bài toán bằng z3
Khi sử dụng z3 để giải quyết bài toán tìm chuỗi ban đầu theo cách ngược lại từ kết quả thì coi các kí tự trong flag là nghiệm và cần có hệ các phương trình. Trong đó để tìm được nghiệm duy nhất thì số phương trình trong hệ cần ≥ số kí tự trong flag. Các phép toán được thực hiện theo thứ tự
b[29] -= b[37] + b[23] + b[22] + b[24] + b[26] + b[10] + 7;
b[29] &= 0xFF;
b[39] += b[34] + b[2] + b[1] + b[43] + b[20] + b[9] + 79;
b[39] &= 0xFF;
b[19] ^= (b[26] + b[0] + b[40] + b[37] + b[23] + b[32] + 255) & 0xFF;
b[28] ^= (b[1] + b[23] + b[37] + b[31] + b[43] + b[42] + 245) & 0xFF;
b[39] += b[42] + b[10] + b[3] + b[41] + b[14] + b[26] + 177;
...
b[22] += b[16] + b[18] + b[7] + b[23] + b[1] + b[27] + 50;
b[22] &= 0xFF;
b[39] += b[18] + b[16] + b[8] + b[19] + b[5] + b[23] + 36;
b[39] &= 0xFF;
Do tính chất thực hiện tuần tự, các vị trí tham chiếu tới vị trí khác nên cũng phải thực hiện tương tự với z3. Ví dụ
from z3 import *
import sys
print(z3.get_version_string())
s = Solver()
i = 0
flag = [106, 196, 106, 178, 174, 102, 31, 91, 66, 255, 86, 196, 74, 139, 219, 166, 106, 4, 211, 68, 227, 72, 156, 38, 239, 153, 223, 225, 73, 171, 51, 4, 234, 50, 207, 82, 18, 111, 180, 212, 81, 189, 73, 76]
print(len(flag))
b = [BitVec(f'b{i}',8) for i in range(len(flag))]
lines = open("operationslog.txt", 'rb').readlines()
for line in lines:
# line = line.strip()
print(line)
exec(f"""{line.decode()}""")
for i in range(len(flag)):
exec(f"""s.add({flag[i]}==b[{i}])""")
print (s.check())
ff = []
r = s.model()
Tuy nhiên khi thực thi thì không cho ra kết quả trong thời gian phù hợp. Theo suy đoán thì có lẽ số lượng biến dữ liệu khi đi qua các phép toán tuần tự đã khiến cho z3 phải xử lý quá nhiều. Để “hỗ trợ” z3 thì mình thực hiện tiền xử lý các biểu thức sử dụng phương pháp chuyển đổi TAC (three-address code) thường dùng trong phân tích tĩnh (bạn đọc có thể tham khảo cuốn sách Rồng - “Compilers: Principles, Techniques, and Tool“ để biết thêm).
Sau khi chuyển đổi các phép toán sẽ có được
b29_1 == b29_0 - (b37_0+b23_0+b22_0+b24_0+b26_0+b10_0+7)
b39_1 == b39_0 + (b34_0+b2_0+b1_0+b43_0+b20_0+b9_0+79)
b19_1 == b19_0 ^ (b26_0+b0_0+b40_0+b37_0+b23_0+b32_0+255)
b28_1 == b28_0 ^ (b1_0+b23_0+b37_0+b31_0+b43_0+b42_0+245)
b39_2 == b39_1 + (b42_0+b10_0+b3_0+b41_0+b14_0+b26_0+177)
...
b22_26 == b22_25 + (b16_23+b18_34+b7_22+b23_27+b1_28+b27_28+50)
b39_24 == b39_23 + (b18_34+b16_23+b8_25+b19_21+b5_26+b23_27+36)
Script để giải ra chuỗi flag:
- indx là array chứa số lượng biến tạm liên quan tới một kí tự trong flag sau chuyển đổi TAC
- flag là mảng giá trị các kí tự của flag sau khi thực hiện tính toán trong Javascript
from z3 import *
print(z3.get_version_string())
indx = [20, 28, 14, 27, 24, 26, 24, 22, 25, 22, 17, 32, 25, 22, 24, 19, 23, 16, 34, 21, 19, 23, 26, 27, 22, 32, 24, 28, 21, 18, 19, 25, 19, 32, 27, 23, 18, 16, 22, 24, 28, 19, 21, 26]
s = Solver()
i = 0
flag = [106, 196, 106, 178, 174, 102, 31, 91, 66, 255, 86, 196, 74, 139, 219, 166, 106, 4, 211, 68, 227, 72, 156, 38, 239, 153, 223, 225, 73, 171, 51, 4, 234, 50, 207, 82, 18, 111, 180, 212, 81, 189, 73, 76]
for maxv in indx:
for j in range(maxv+1):
exec(f'''b{i}_{j} = BitVec('b{i}_{j}',8)''')
exec(f"""s.add(b{i}_{j}=={flag[i]})""")
i+=1
lines = open("tacoperationslog.txt", 'rb').readlines()
for line in lines:
# line = line.strip()
print(line)
exec(f"""s.add({line.decode()})""")
print (s.check())
ff = []
r = s.model()
for i in range(44):
exec(f"""ff.append(int(r[b{i}_0].as_long()))""")
print("".join(map(chr, ff)))
#n0t_ju5t_A_j4vaSCriP7_....
n0t_ju5t_A_j4vaSCriP7_ch4l1eng3@flare-on.com