ArchventureTime

Challenge Description
#

I found this funny multi-arch music software but I can’t remember my license key.

Can you recover it for me?

Solution
#

The binary is a license checker. The correct license will be used as key to decrypt the flag with AES-CBC. We reversed the binary with the help of Ghidra.

The license checker first checks the format of the input to be XXXXX-XXXXX-XXXXX-XXXXX, where X is a digit or an uppercase character. Then, it will create a copy, without the - characters, that will then be used for further checks. The program continues to perform 4 checks by:

creating a temporary file with the contents of an embedded ELF file for a different architecture
call the binary with user-space emulation QEMU and check for an exit code of 0
delete the file

Each binary is embedded in the initial binary without any obfuscation. As such, we can easily export it or even use Ghidra’s Extract and Import functionality after selecting the raw data. In the following, we will describe the functionality of the different binaries. We were able to decompile all of them with Ghidra without problems and did not need to concern ourselves with the architecture details.

1. Binary: RISCV64
#

The program performs merge sort on the input followed by a strcmp with "067889BBCKKMOPPUVWYY". Thus, we now know what characters are part of the license, but not their order.

2. Binary: x86_64
#

The second binary takes each 5 character sequence and computes the following:

The sum of digits
The sum of uppercase characters, where ‘A’ represents 0, ‘G’ represents 6, ‘Z’ 25 and so on)

For each of these sums, there is a table with the expected value and the license check will fail if any don’t match.

3. Binary: PowerPC 64-Bit
#

This program will for every character (but the last) perform the following:

Convert the character to its index in the string "ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"
Then, for each character there is an array of 0x18 integers and it will check to see if the next character in the license is included in this array. If it is not, the check fails

As such, each character has a whitelist of characters that are allowed to follow.

4. Binary: AARCH64
#

The last binary performs two checks:

Check 1: Checking for specific characters
#

First, the program has an array of 20 integers that either are -1 or contain the value of an ASCII character. If the entry is not -1, it will check whether the corresponding character in the input matches the value in the array. With this, we get the following information:

input[15] = 'Y'
input[17] = 'M'
input[18] = '8'

Check 2: Implications
#

The second checking logic essentially implements a form of implication logic. For each byte in the input, there is a list of 10 entries with the following structure.

4 byte padding
4 byte integer match_value
4 byte integer implication_index
4 byte integer implication_value

It will then iterate for every index through the corresponding entries and checks: If input[i] == match_value then input[implication_index] == implication_value.

Combining everything
#

To find an input that satisfies these constraints, we can make use of a constraint solver such as z3. In the following, we will describe how to use z3 and model the constraints:

Defining the flag and flag format
#

To start with z3, we first need to define input variables and create a Solver instance. We know the flag parts are 20 unknown bytes, thus we have to create 20 8-bit bitvector variables.

s = z3.Solver()
flag = [z3.BitVec(f'f{i}', 8) for i in range(20)]

The initial binary also checks that all characters are digits or uppercase characters. We can add these constraints to the solver. To add any constraint, we need to use the Solver.add function. As we need it later as well, we will define helper functions to get a constraint for uppercase characters and digits.

def z3_isdigit(f):
    return z3.And(f >= ord('0'), f <= ord('9'))

def z3_isupper(f):
    return z3.And(f >= ord('A'), f <= ord('Z'))

# General flag format
for f in flag:
    s.add(z3.Or(z3_isdigit(f), z3_isupper(f)))

Modeling the first binary
#

The first binary essentially tells us which characters are part of the string and how often they appear. We can model this by creating helper formulas for the count of each character in the string and adding a constraint for the counts. To create the counts, the z3.If function is very useful:

all_chars = "067889BBCKKMOPPUVWYY"
for c in set(all_chars):
    cnt = all_chars.count(c)
    rcnt = z3.IntVal(0)
    for f in flag:
        rcnt += z3.If(f == ord(c), 1, 0)
    s.add(cnt == rcnt)

Modeling character sums
#

The second binary had constraints about the sums of digits or uppercase characters. Similarly to before, sums can be easily modeled with the z3.If function. As the flag characters are bitvectors, we use a bitvector type for the sum as well so we don’t have to cast later on:

number_sums      = [  0,  7, 14, 17 ]
capitalized_sums = [ 61, 36, 44, 50 ]

for part in range(4):
    sum_n = z3.BitVecVal(0, 8)
    sum_c = z3.BitVecVal(0, 8)
    for part_idx in range(5):
        flag_idx = part * 5 + part_idx
        c = flag[flag_idx]
        sum_n += z3.If(z3_isdigit(c), c - ord('0'), 0)
        sum_c += z3.If(z3_isupper(c), c - ord('A'), 0)
    s.add(number_sums[part] == sum_n)
    s.add(capitalized_sums[part] == sum_c)

Modeling the neighbour whitelists
#

Luckily z3 has an Implies function that can be used to model implications. We will iterate over all characters and for each neighbour pair, we will add the corresponding implications.

In the following snippet, we exported the binary data of the array and directly extracted the values from it. To iterate over the neighbours, we made use of the more_itertools.windowed function. Furthermore, as a small optimization, we didn’t add constraints for characters that are disallowed from the first binary:

_allowed_chars = "ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"
bin3_allow_array = [ 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x51, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x4e, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x50, 0x00, 0x00, 0x00, 0x59, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x34, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x57, 0x00, 0x00, 0x00, 0x4b, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x4f, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x38, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x48, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x32, 0x00, 0x00, 0x00, 0x4c, 0x00, 0x00, 0x00, 0x30, 0x00, 0x00, 0x00, 0x47, 0x00, 0x00, 0x00, 0x39, 0x00, 0x00, 0x00, 0x58, 0x00, 0x00, 0x00, 0x5a, 0x00, 0x00, 0x00, 0x49, 0x00, 0x00, 0x00, 0x35, 0x00, 0x00, 0x00, 0x54, 0x00, 0x00, 0x00, 0x45, 0x00, 0x00, 0x00, 0x44, 0x00, 0x00, 0x00, 0x33, 0x00, 0x00, 0x00, 0x4a, 0x00, 0x00, 0x00, 0x43, 0x00, 0x00, 0x00, 0x55, 0x00, 0x00, 0x00, 0x53, 0x00, 0x00, 0x00, 0x31, 0x00, 0x00, 0x00, 0x46, 0x00, 0x00, 0x00, 0x41, 0x00, 0x00, 0x00, 0x4d, 0x00, 0x00, 0x00, 0x37, 0x00, 0x00, 0x00, 0x52, 0x00, 0x00, 0x00, 0x56, 0x00, 0x00, 0x00, 0x42, 0x00, 0x00, 0x00, 0x36, 0x00, 0x00, 0x00, 0x50 ]

for c in all_chars:
    idx = _allowed_chars.index(c)
    c_allowed_chars = [bin3_allow_array[0x60*idx + i+3] for i in range(0, 0x60, 0x4)]
    c_allowed_chars = list(filter(lambda x: chr(x) in all_chars, c_allowed_chars))

    for f1,f2 in windowed(flag,2):
        s.add(z3.Implies(f1 == ord(c), z3.Or(*[f2 == ca for ca in c_allowed_chars])))

Modeling the last binary
#

For the first check, we can simply add the equality constraints:

s.add(flag[15] == ord('Y'))
s.add(flag[17] == ord('M'))
s.add(flag[18] == ord('8'))

For the implications, we can make use of the z3.Implies function again. Again, we extracted the binary data with Ghidra and directly parsed it - this time with the struct package:

bin4_check_array = b'\x00\x00\x00\x00\x49\x00\x00\x00\x12\x00\x00\x00\x35\x00\x00\x00\x00\x00\x00\x00\x59\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x00\x00\x00\x00\x56\x00\x00\x00\x0e\x00\x00\x00\x55\x00\x00\x00\x00\x00\x00\x00\x4c\x00\x00\x00\x06\x00\x00\x00\x49\x00\x00\x00\x00\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x5a\x00\x00\x00\x00\x00\x00\x00\x37\x00\x00\x00\x03\x00\x00\x00\x57\x00\x00\x00\x00\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x49\x00\x00\x00\x00\x00\x00\x00\x58\x00\x00\x00\x08\x00\x00\x00\x33\x00\x00\x00\x00\x00\x00\x00\x37\x00\x00\x00\x0c\x00\x00\x00\x4d\x00\x00\x00\x00\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x43\x00\x00\x00\x01\x00\x00\x00\x4a\x00\x00\x00\x03\x00\x00\x00\x54\x00\x00\x00\x01\x00\x00\x00\x55\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x4c\x00\x00\x00\x02\x00\x00\x00\x47\x00\x00\x00\x01\x00\x00\x00\x56\x00\x00\x00\x12\x00\x00\x00\x36\x00\x00\x00\x01\x00\x00\x00\x44\x00\x00\x00\x0f\x00\x00\x00\x35\x00\x00\x00\x01\x00\x00\x00\x4d\x00\x00\x00\x05\x00\x00\x00\x4f\x00\x00\x00\x01\x00\x00\x00\x4d\x00\x00\x00\x0d\x00\x00\x00\x54\x00\x00\x00\x01\x00\x00\x00\x38\x00\x00\x00\x07\x00\x00\x00\x55\x00\x00\x00\x01\x00\x00\x00\x58\x00\x00\x00\x11\x00\x00\x00\x50\x00\x00\x00\x02\x00\x00\x00\x58\x00\x00\x00\x05\x00\x00\x00\x44\x00\x00\x00\x02\x00\x00\x00\x59\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x00\x00\x02\x00\x00\x00\x4d\x00\x00\x00\x03\x00\x00\x00\x56\x00\x00\x00\x02\x00\x00\x00\x59\x00\x00\x00\x0d\x00\x00\x00\x5a\x00\x00\x00\x02\x00\x00\x00\x47\x00\x00\x00\x0c\x00\x00\x00\x4f\x00\x00\x00\x02\x00\x00\x00\x45\x00\x00\x00\x13\x00\x00\x00\x57\x00\x00\x00\x02\x00\x00\x00\x31\x00\x00\x00\x07\x00\x00\x00\x58\x00\x00\x00\x02\x00\x00\x00\x46\x00\x00\x00\x08\x00\x00\x00\x46\x00\x00\x00\x02\x00\x00\x00\x45\x00\x00\x00\x01\x00\x00\x00\x55\x00\x00\x00\x02\x00\x00\x00\x52\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x03\x00\x00\x00\x44\x00\x00\x00\x13\x00\x00\x00\x50\x00\x00\x00\x03\x00\x00\x00\x39\x00\x00\x00\x01\x00\x00\x00\x58\x00\x00\x00\x03\x00\x00\x00\x4e\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x03\x00\x00\x00\x4c\x00\x00\x00\x09\x00\x00\x00\x52\x00\x00\x00\x03\x00\x00\x00\x45\x00\x00\x00\x0c\x00\x00\x00\x48\x00\x00\x00\x03\x00\x00\x00\x59\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x03\x00\x00\x00\x4a\x00\x00\x00\x06\x00\x00\x00\x41\x00\x00\x00\x03\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x30\x00\x00\x00\x03\x00\x00\x00\x52\x00\x00\x00\x08\x00\x00\x00\x38\x00\x00\x00\x03\x00\x00\x00\x56\x00\x00\x00\x07\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x39\x00\x00\x00\x00\x00\x00\x00\x42\x00\x00\x00\x04\x00\x00\x00\x4a\x00\x00\x00\x10\x00\x00\x00\x45\x00\x00\x00\x04\x00\x00\x00\x37\x00\x00\x00\x06\x00\x00\x00\x32\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x04\x00\x00\x00\x4a\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x04\x00\x00\x00\x33\x00\x00\x00\x08\x00\x00\x00\x54\x00\x00\x00\x04\x00\x00\x00\x33\x00\x00\x00\x01\x00\x00\x00\x54\x00\x00\x00\x04\x00\x00\x00\x4c\x00\x00\x00\x03\x00\x00\x00\x42\x00\x00\x00\x04\x00\x00\x00\x52\x00\x00\x00\x0d\x00\x00\x00\x48\x00\x00\x00\x04\x00\x00\x00\x32\x00\x00\x00\x0b\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x42\x00\x00\x00\x0b\x00\x00\x00\x56\x00\x00\x00\x05\x00\x00\x00\x4a\x00\x00\x00\x13\x00\x00\x00\x30\x00\x00\x00\x05\x00\x00\x00\x31\x00\x00\x00\x12\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x36\x00\x00\x00\x06\x00\x00\x00\x4d\x00\x00\x00\x05\x00\x00\x00\x54\x00\x00\x00\x00\x00\x00\x00\x44\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x0e\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x42\x00\x00\x00\x0f\x00\x00\x00\x4a\x00\x00\x00\x05\x00\x00\x00\x45\x00\x00\x00\x10\x00\x00\x00\x44\x00\x00\x00\x05\x00\x00\x00\x55\x00\x00\x00\x11\x00\x00\x00\x4c\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x06\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x32\x00\x00\x00\x06\x00\x00\x00\x46\x00\x00\x00\x13\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x4f\x00\x00\x00\x0d\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x53\x00\x00\x00\x0b\x00\x00\x00\x56\x00\x00\x00\x06\x00\x00\x00\x30\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x06\x00\x00\x00\x32\x00\x00\x00\x09\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x33\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x06\x00\x00\x00\x56\x00\x00\x00\x00\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x5a\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x06\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x44\x00\x00\x00\x07\x00\x00\x00\x58\x00\x00\x00\x12\x00\x00\x00\x38\x00\x00\x00\x07\x00\x00\x00\x31\x00\x00\x00\x0f\x00\x00\x00\x57\x00\x00\x00\x07\x00\x00\x00\x33\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x07\x00\x00\x00\x4f\x00\x00\x00\x0a\x00\x00\x00\x41\x00\x00\x00\x07\x00\x00\x00\x34\x00\x00\x00\x08\x00\x00\x00\x4a\x00\x00\x00\x07\x00\x00\x00\x46\x00\x00\x00\x11\x00\x00\x00\x55\x00\x00\x00\x07\x00\x00\x00\x39\x00\x00\x00\x05\x00\x00\x00\x34\x00\x00\x00\x07\x00\x00\x00\x52\x00\x00\x00\x06\x00\x00\x00\x51\x00\x00\x00\x07\x00\x00\x00\x55\x00\x00\x00\x0e\x00\x00\x00\x4e\x00\x00\x00\x07\x00\x00\x00\x4f\x00\x00\x00\x10\x00\x00\x00\x48\x00\x00\x00\x08\x00\x00\x00\x4e\x00\x00\x00\x0f\x00\x00\x00\x4b\x00\x00\x00\x08\x00\x00\x00\x33\x00\x00\x00\x12\x00\x00\x00\x54\x00\x00\x00\x08\x00\x00\x00\x34\x00\x00\x00\x0a\x00\x00\x00\x4f\x00\x00\x00\x08\x00\x00\x00\x38\x00\x00\x00\x11\x00\x00\x00\x39\x00\x00\x00\x08\x00\x00\x00\x56\x00\x00\x00\x0b\x00\x00\x00\x54\x00\x00\x00\x08\x00\x00\x00\x4d\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x08\x00\x00\x00\x43\x00\x00\x00\x10\x00\x00\x00\x58\x00\x00\x00\x08\x00\x00\x00\x34\x00\x00\x00\x0c\x00\x00\x00\x37\x00\x00\x00\x08\x00\x00\x00\x52\x00\x00\x00\x06\x00\x00\x00\x46\x00\x00\x00\x08\x00\x00\x00\x4e\x00\x00\x00\x0d\x00\x00\x00\x50\x00\x00\x00\x09\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x52\x00\x00\x00\x09\x00\x00\x00\x33\x00\x00\x00\x07\x00\x00\x00\x41\x00\x00\x00\x09\x00\x00\x00\x49\x00\x00\x00\x03\x00\x00\x00\x47\x00\x00\x00\x09\x00\x00\x00\x59\x00\x00\x00\x11\x00\x00\x00\x58\x00\x00\x00\x09\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x41\x00\x00\x00\x09\x00\x00\x00\x32\x00\x00\x00\x10\x00\x00\x00\x33\x00\x00\x00\x09\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x52\x00\x00\x00\x09\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x33\x00\x00\x00\x09\x00\x00\x00\x51\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x09\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x0a\x00\x00\x00\x57\x00\x00\x00\x02\x00\x00\x00\x51\x00\x00\x00\x0a\x00\x00\x00\x30\x00\x00\x00\x09\x00\x00\x00\x4e\x00\x00\x00\x0a\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x36\x00\x00\x00\x0a\x00\x00\x00\x33\x00\x00\x00\x0b\x00\x00\x00\x58\x00\x00\x00\x0a\x00\x00\x00\x49\x00\x00\x00\x0c\x00\x00\x00\x38\x00\x00\x00\x0a\x00\x00\x00\x52\x00\x00\x00\x0f\x00\x00\x00\x46\x00\x00\x00\x0a\x00\x00\x00\x57\x00\x00\x00\x0e\x00\x00\x00\x41\x00\x00\x00\x0a\x00\x00\x00\x45\x00\x00\x00\x05\x00\x00\x00\x34\x00\x00\x00\x0a\x00\x00\x00\x55\x00\x00\x00\x11\x00\x00\x00\x4b\x00\x00\x00\x0a\x00\x00\x00\x33\x00\x00\x00\x03\x00\x00\x00\x41\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x0b\x00\x00\x00\x4d\x00\x00\x00\x08\x00\x00\x00\x53\x00\x00\x00\x0b\x00\x00\x00\x4a\x00\x00\x00\x11\x00\x00\x00\x52\x00\x00\x00\x0b\x00\x00\x00\x5a\x00\x00\x00\x05\x00\x00\x00\x47\x00\x00\x00\x0b\x00\x00\x00\x52\x00\x00\x00\x0c\x00\x00\x00\x41\x00\x00\x00\x0b\x00\x00\x00\x39\x00\x00\x00\x0d\x00\x00\x00\x31\x00\x00\x00\x0b\x00\x00\x00\x32\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x0b\x00\x00\x00\x32\x00\x00\x00\x0e\x00\x00\x00\x48\x00\x00\x00\x0b\x00\x00\x00\x34\x00\x00\x00\x10\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0c\x00\x00\x00\x38\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0c\x00\x00\x00\x4f\x00\x00\x00\x01\x00\x00\x00\x43\x00\x00\x00\x0c\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x31\x00\x00\x00\x0c\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x36\x00\x00\x00\x0c\x00\x00\x00\x37\x00\x00\x00\x06\x00\x00\x00\x54\x00\x00\x00\x0c\x00\x00\x00\x35\x00\x00\x00\x07\x00\x00\x00\x45\x00\x00\x00\x0c\x00\x00\x00\x50\x00\x00\x00\x13\x00\x00\x00\x53\x00\x00\x00\x0c\x00\x00\x00\x4d\x00\x00\x00\x0e\x00\x00\x00\x4a\x00\x00\x00\x0c\x00\x00\x00\x50\x00\x00\x00\x09\x00\x00\x00\x49\x00\x00\x00\x0c\x00\x00\x00\x57\x00\x00\x00\x10\x00\x00\x00\x41\x00\x00\x00\x0d\x00\x00\x00\x5a\x00\x00\x00\x02\x00\x00\x00\x37\x00\x00\x00\x0d\x00\x00\x00\x4e\x00\x00\x00\x00\x00\x00\x00\x38\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x08\x00\x00\x00\x37\x00\x00\x00\x0d\x00\x00\x00\x45\x00\x00\x00\x07\x00\x00\x00\x36\x00\x00\x00\x0d\x00\x00\x00\x55\x00\x00\x00\x12\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x0d\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x44\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0d\x00\x00\x00\x37\x00\x00\x00\x0f\x00\x00\x00\x36\x00\x00\x00\x0d\x00\x00\x00\x32\x00\x00\x00\x0a\x00\x00\x00\x51\x00\x00\x00\x0e\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x4e\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x09\x00\x00\x00\x36\x00\x00\x00\x0e\x00\x00\x00\x37\x00\x00\x00\x12\x00\x00\x00\x32\x00\x00\x00\x0e\x00\x00\x00\x4b\x00\x00\x00\x0b\x00\x00\x00\x48\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x01\x00\x00\x00\x36\x00\x00\x00\x0e\x00\x00\x00\x57\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x0e\x00\x00\x00\x41\x00\x00\x00\x02\x00\x00\x00\x46\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x06\x00\x00\x00\x59\x00\x00\x00\x0e\x00\x00\x00\x48\x00\x00\x00\x10\x00\x00\x00\x42\x00\x00\x00\x0e\x00\x00\x00\x4e\x00\x00\x00\x0f\x00\x00\x00\x54\x00\x00\x00\x0f\x00\x00\x00\x42\x00\x00\x00\x09\x00\x00\x00\x35\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x0f\x00\x00\x00\x48\x00\x00\x00\x0d\x00\x00\x00\x30\x00\x00\x00\x0f\x00\x00\x00\x42\x00\x00\x00\x0b\x00\x00\x00\x53\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x11\x00\x00\x00\x54\x00\x00\x00\x0f\x00\x00\x00\x50\x00\x00\x00\x03\x00\x00\x00\x57\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x01\x00\x00\x00\x32\x00\x00\x00\x0f\x00\x00\x00\x48\x00\x00\x00\x08\x00\x00\x00\x4f\x00\x00\x00\x0f\x00\x00\x00\x51\x00\x00\x00\x02\x00\x00\x00\x43\x00\x00\x00\x0f\x00\x00\x00\x4e\x00\x00\x00\x10\x00\x00\x00\x34\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x10\x00\x00\x00\x4f\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x10\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x4b\x00\x00\x00\x10\x00\x00\x00\x32\x00\x00\x00\x05\x00\x00\x00\x38\x00\x00\x00\x10\x00\x00\x00\x49\x00\x00\x00\x13\x00\x00\x00\x49\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x10\x00\x00\x00\x48\x00\x00\x00\x00\x00\x00\x00\x54\x00\x00\x00\x10\x00\x00\x00\x4a\x00\x00\x00\x01\x00\x00\x00\x32\x00\x00\x00\x10\x00\x00\x00\x57\x00\x00\x00\x0f\x00\x00\x00\x43\x00\x00\x00\x10\x00\x00\x00\x51\x00\x00\x00\x04\x00\x00\x00\x45\x00\x00\x00\x11\x00\x00\x00\x4c\x00\x00\x00\x0f\x00\x00\x00\x44\x00\x00\x00\x11\x00\x00\x00\x52\x00\x00\x00\x04\x00\x00\x00\x4f\x00\x00\x00\x11\x00\x00\x00\x48\x00\x00\x00\x06\x00\x00\x00\x43\x00\x00\x00\x11\x00\x00\x00\x38\x00\x00\x00\x08\x00\x00\x00\x32\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x11\x00\x00\x00\x38\x00\x00\x00\x00\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x5a\x00\x00\x00\x0a\x00\x00\x00\x5a\x00\x00\x00\x11\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x33\x00\x00\x00\x12\x00\x00\x00\x33\x00\x00\x00\x11\x00\x00\x00\x4b\x00\x00\x00\x05\x00\x00\x00\x39\x00\x00\x00\x12\x00\x00\x00\x38\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x12\x00\x00\x00\x46\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x12\x00\x00\x00\x4d\x00\x00\x00\x11\x00\x00\x00\x55\x00\x00\x00\x12\x00\x00\x00\x53\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x00\x00\x12\x00\x00\x00\x46\x00\x00\x00\x03\x00\x00\x00\x31\x00\x00\x00\x12\x00\x00\x00\x31\x00\x00\x00\x0d\x00\x00\x00\x47\x00\x00\x00\x12\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x36\x00\x00\x00\x12\x00\x00\x00\x31\x00\x00\x00\x06\x00\x00\x00\x54\x00\x00\x00\x12\x00\x00\x00\x45\x00\x00\x00\x13\x00\x00\x00\x37\x00\x00\x00\x12\x00\x00\x00\x42\x00\x00\x00\x08\x00\x00\x00\x52\x00\x00\x00\x13\x00\x00\x00\x32\x00\x00\x00\x08\x00\x00\x00\x56\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x13\x00\x00\x00\x57\x00\x00\x00\x09\x00\x00\x00\x4d\x00\x00\x00\x13\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x57\x00\x00\x00\x13\x00\x00\x00\x56\x00\x00\x00\x04\x00\x00\x00\x47\x00\x00\x00\x13\x00\x00\x00\x42\x00\x00\x00\x02\x00\x00\x00\x37\x00\x00\x00\x13\x00\x00\x00\x49\x00\x00\x00\x01\x00\x00\x00\x38\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x05\x00\x00\x00\x32\x00\x00\x00\x13\x00\x00\x00\x54\x00\x00\x00\x0c\x00\x00\x00\x44\x00\x00\x00\x13\x00\x00\x00\x45\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00'

for i, f in enumerate(flag):
    for j in range(10):
        _idx = (i * 10 + j) * 0x10
        _, match_val, imply_idx, imply_val = struct.unpack("<IIII", bin4_check_array[_idx:_idx+0x10])

        s.add(z3.Implies(f == match_val, flag[imply_idx] == imply_val))

Solving the system and getting the flag
#

To get a solution from z3, we will first need to call s.check() on the solver, which will compute whether the constraint system is satisfiable. With s.model(), we can get a possible solution to the constraints. This model can then be indexed with the variable and the value converted to an int with .as_long(). Finally, we make use of more_itertools.chunked to add the - in the final license:

s.check()
m = s.model()
key = [chr(m[f].as_long()) for f in flag]
print("-".join("".join(kv) for kv in chunked(key, 5)))

The complete script can be found in solve.py.

Other writeups of challenges from GPN CTF 2024.

ArchventureTime

Boombox

Dreamer

FutureOfPwning2

Challenge Description#

Solution#

1. Binary: RISCV64#

2. Binary: x86_64#

3. Binary: PowerPC 64-Bit#

4. Binary: AARCH64#

Check 1: Checking for specific characters#

Check 2: Implications#

Combining everything#

Defining the flag and flag format#

Modeling the first binary#

Modeling character sums#

Modeling the neighbour whitelists#

Modeling the last binary#

Solving the system and getting the flag#