Today we will be reversing a serial number validator written in EXCEL logic.
First steps
We receive an XLSX file and opening it in EXCEL shows there is a single “Start Page” sheet. It asks us to enter a serial number in XXXXX-XXXX-XXXX-XXXXX format in a cell row. Under it is a 21-cell “serial status” bar which is all red. Finally a label that tells us that if we have problems, send the message below to customer support. Below is a series of seemingly random unicode characters.
We can see that trying a couple of different serials keeps changing the unicode message, and also one of the cells in the status bar turned green. Checking the unicode cell shows this value:
=CONCATENATE(Tabelle4!A4,Tabelle4!B4,Tabelle4!C4,Tabelle4!D4,Tabelle4!E4,Tabelle4!F4,Tabelle4!G4,Tabelle4!H4,Tabelle4!I4,Tabelle4!J4,Tabelle4!K4,Tabelle4!L4,Tabelle4!M4,Tabelle4!N4,Tabelle4!O4,Tabelle4!P4,Tabelle4!Q4,Tabelle4!R4,Tabelle4!S4,Tabelle4!T4,Tabelle4!U4,Tabelle4!V4,Tabelle4!
Huh?! What is Tabelle4 ?!?! It turns out that EXCEL supports hidden sheets, and we just needed to unhide them via the sheet selector. So we uncovered 4 new sheets — Tabelle1/2/3/4. Inside them we see a bunch of tables and when checking some of the cells we see some are fixed and others are dynamically calculated via math functions on cells. We spotted a pattern where Tabelle1’s table has a column with values just copied from the serial number. Other columns are results of operations on the serial (more on that later). Tabelle2 uses a column from Tabelle1, Tabelle3 uses a column from Tabelle2 and Tabelle4 uses a column from Tabelle3.
Finding the win condition
At this point we wasted considerable time reversing different parts of Tabelle1/2/3/4’s operations. At some point we got annoyed that we can’t see the logic which controls the serial status bar (the cell was empty + there were no macros found anywhere in the VBA editor). We extracted the XLSX as a zip and started looking around. Under xl/worksheets there were 5 sheet XMLs. we opened sheet1.xml in an editor and found a series of suspicious lines looking like:
<x14:conditionalFormatting xmlns:xm=”http://schemas.microsoft.com/office/excel/2006/main"><x14:cfRule type=”expression” priority=”23" id=”{47E12DA3-B6E8–5E48–8F2A-14C0E047E813}”><xm:f>Tabelle1!$G$21=0</xm:f><x14:dxf><fill><patternFill><bgColor theme=”9"/></patternFill></fill></x14:dxf></x14:cfRule><xm:sqref>B17</xm:sqref></x14:conditionalFormatting>
This rule states that cell B17 is colored conditionally via the expression “Tabelle1!$G$21=0”, meaning the G21 in Tabelle1 must equal 0. Later we found out this can obviously be displayed graphically via the “Conditional formatting” button. Evidently, all the 21 cells of the status bar depend only on values taken from Tabelle1. So we started understanding Tabelle2/3/4 are a decoy / just functions to generate the unicode message, which will probably be the challenge flag!
Alright, so we dumped the 21 conditions:
Tabelle1!$G$21=0
Tabelle1!$H$7=81 OR Tabelle1!$H$7=87
Tabelle1!$I$11=79
Tabelle1!$J$15=74
Tabelle1!$H$20=82
Tabelle1!$F$24=0
Tabelle1!$M$3=57
Tabelle1!$M$4=38
Tabelle1!$M$5=57
Tabelle1!$M$6=47
Tabelle1!$M$7=169
Tabelle1!$P$7=116
Tabelle1!$Q$3=133
Tabelle1!$Q$4=225
Tabelle1!$Q$5=163
Tabelle1!$Q$6=212
Tabelle1!$K$7=248
Tabelle1!$M$15=176
Tabelle1!$L$11=36
Tabelle1!$L$20=60
Tabelle1!$R$3=62
Tabelle1
This table has 4 columns of 18 constant numbers, then a column which is a copy of the serial number and then a column which is the ASCII mapping of each character from the serial.
6 2 85 17 A 65
5 3 68 34 B 66
4 4 51 51 C 67
3 5 34 68 D 68
2 6 17 85 E 69
1 7 68 17 F 70
0 8 51 34 G 71
8 0 34 51 H 72
7 1 17 68 I 73
6 2 68 17 J 74
5 3 51 34 K 75
4 4 34 51 L 76
3 5 17 68 M 77
2 6 85 17 N 78
1 7 68 34 O 79
0 8 51 51 P 80
8 0 34 68 Q 81
7 1 17 85 R 82
After these, there are a bunch of cells which are calculated using adding and BITOR / BITAND / BITXOR/ BITLSHIFT / BITRSHIFT excel functions on existing cells. This type of operations is very convenient to plug into a constraint solver, so we pretty quickly decided on just coding the whole tabelle1 table in z3 and solving for the conditions on cell values we found in the serial status. Below is the pretty ugly script:
Within no time we get the correct serial: VLLKZ-JKNF-RCGP-GLXNO
import z3
class Excel(object):
def __init__(self):
self.flag = [z3.BitVec("flag_%d" % i,8) for i in range(18)]
self.solver = z3.Solver()
for fl in self.flag:
self._assert_printable(fl)
self.flag_constraints()
def execel_line_to_flag_byte(self, i):
return self.flag[i - 3]
def execel_line_to_index(self, i):
return i - 3
def _assert_printable(self, byte):
self.solver.add(z3.And(byte >= 0x41, byte <= 0x5a))
self.solver.add(z3.And(byte >= 0x11, byte <= 0x7e))
self.solver.add(byte & 0x20 == 0)
def flag_constraints(self):
self.h3 = ((self.execel_line_to_flag_byte(3) ^ 17) >> 2)
self.h4 = ((self.execel_line_to_flag_byte(4) ^ 34) >> 2) + self.h3
self.h5 = ((self.execel_line_to_flag_byte(5) ^ 51) >> 2) + self.h4
self.h6 = ((self.execel_line_to_flag_byte(6) ^ 68) >> 2) + self.h5
self.h7 = ((self.execel_line_to_flag_byte(7) ^ 85) >> 2) + self.h6
self.solver.add(z3.Or(
self.h7 == 81,
self.h7 == 87,
))
self.i8 = ((self.execel_line_to_flag_byte(8) ^ 17) >> 2)
self.i9 = ((self.execel_line_to_flag_byte(9) ^ 34) >> 2) + self.i8
self.i10 = ((self.execel_line_to_flag_byte(10) ^ 51) >> 2) + self.i9
self.i11 = ((self.execel_line_to_flag_byte(11) ^ 68) >> 2) + self.i10
self.solver.add(self.i11 == 79)
self.j12 = ((self.execel_line_to_flag_byte(12) ^ 17) >> 2)
self.j13 = ((self.execel_line_to_flag_byte(13) ^ 34) >> 2) + self.j12
self.j14 = ((self.execel_line_to_flag_byte(14) ^ 51) >> 2) + self.j13
self.j15 = ((self.execel_line_to_flag_byte(15) ^ 68) >> 2) + self.j14
self.solver.add(self.j15 == 74)
self.h16 = ((self.execel_line_to_flag_byte(16) ^ 17) >> 2)
self.h17 = ((self.execel_line_to_flag_byte(17) ^ 34) >> 2) + self.h16
self.h18 = ((self.execel_line_to_flag_byte(18) ^ 51) >> 2) + self.h17
self.h19 = ((self.execel_line_to_flag_byte(19) ^ 68) >> 2) + self.h18
self.h20 = ((self.execel_line_to_flag_byte(20) ^ 85) >> 2) + self.h19
self.solver.add(self.h20 == 82)
self.solver.add(
-14 + sum(z3.BV2Int(self.execel_line_to_flag_byte(i)) for i in range(3, 8))
- sum(z3.BV2Int(self.execel_line_to_flag_byte(i)) for i in range(8, 12))
+ sum(z3.BV2Int(self.execel_line_to_flag_byte(i)) for i in range(12, 16))
- sum(z3.BV2Int(self.execel_line_to_flag_byte(i)) for i in range(16, 21))
== 0
)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [3, 8, 12, 16]) == 57)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [4, 9, 13, 17]) == 38)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [5, 10, 14, 18]) == 57)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [6, 11, 15, 19]) == 47)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [7, 20]) == 169)
self.A = [6, 5, 4, 3, 2, 1, 0, 8, 7, 6, 5, 4, 3, 2, 1, 0, 8, 7]
self.B = [2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]
self.N = [
(self.flag[i] << self.A[i]) | (self.flag[i] >> self.B[i])
for i in range(len(self.flag))
]
self.P = [
self.N[i] ^ self.N[-1 -i]
for i in range(int(len(self.flag) / 2))
]
self.Q = [
self.P[i] ^ self.P[-1 -i]
for i in range(int(len(self.P) / 2))
]
self.solver.add(self.P[self.execel_line_to_index(7)] == 116)
self.solver.add(self.Q[self.execel_line_to_index(3)] == 133)
self.solver.add(self.Q[self.execel_line_to_index(4)] == 225)
self.solver.add(self.Q[self.execel_line_to_index(5)] == 163)
self.solver.add(self.Q[self.execel_line_to_index(6)] == 212)
self.k3 = ((self.execel_line_to_flag_byte(3) ^ 85) << 2)
self.k4 = ((self.execel_line_to_flag_byte(4) ^ 68) << 2) + self.k3
self.k5 = ((self.execel_line_to_flag_byte(5) ^ 51) << 2) + self.k4
self.k6 = ((self.execel_line_to_flag_byte(6) ^ 34) << 2) + self.k5
self.k7 = ((self.execel_line_to_flag_byte(7) ^ 17) << 2) + self.k6
self.solver.add(self.k7 == 248)
self.m12 = ((self.execel_line_to_flag_byte(12) ^ 68) << 2)
self.m13 = ((self.execel_line_to_flag_byte(13) ^ 51) << 2) + self.m12
self.m14 = ((self.execel_line_to_flag_byte(14) ^ 34) << 2) + self.m13
self.m15 = ((self.execel_line_to_flag_byte(15) ^ 17) << 2) + self.m14
self.solver.add(self.m15 == 176)
self.l8 = ((self.execel_line_to_flag_byte(8) ^ 68) << 2)
self.l9 = ((self.execel_line_to_flag_byte(9) ^ 51) << 2) + self.l8
self.l10 = ((self.execel_line_to_flag_byte(10) ^ 34) << 2) + self.l9
self.l11 = ((self.execel_line_to_flag_byte(11) ^ 17) << 2) + self.l10
self.solver.add(self.l11 == 36)
self.l16 = ((self.execel_line_to_flag_byte(16) ^ 85) << 2)
self.l17 = ((self.execel_line_to_flag_byte(17) ^ 68) << 2) + self.l16
self.l18 = ((self.execel_line_to_flag_byte(18) ^ 51) << 2) + self.l17
self.l19 = ((self.execel_line_to_flag_byte(19) ^ 34) << 2) + self.l18
self.l20 = ((self.execel_line_to_flag_byte(20) ^ 17) << 2) + self.l19
self.solver.add(self.l20 == 60)
self.solver.add(sum(self.execel_line_to_flag_byte(i) for i in [4, 5, 18, 19]) == 62)
excel = Excel()
excel.solver.check()
m = excel.solver.model()
print(' '.join(chr(m[flag_letter].as_long()) for flag_letter in excel.flag[0:5]))
print(' '.join(chr(m[flag_letter].as_long()) for flag_letter in excel.flag[5:9]))
print(' '.join(chr(m[flag_letter].as_long()) for flag_letter in excel.flag[9:13]))
print(' '.join(chr(m[flag_letter].as_long()) for flag_letter in excel.flag[13:18]))
And plugging it in, we indeed get the flag in the customer support message section: hxp{excellence_c0mes_fr0m_excel}
Summary
1. Time was wasted reversing the worksheets which we didn’t actually need to understand -> During CTF it is usually more cost effective to implement a greedy algorithm
2. More googling would have found the conditional formatting tab faster and more deterministically than inspecting internal files (which could have been binary).
3. z3 is a CTF beast
Comments