AIRANGE'24 - Rev - Constraints

Challenge Description

Ashfaq Nadeem made an unbreakable licensing software

Download

Solution

My friend Kumail and I solved this challenge together.

First of all open the compiled code in ghidra. Here, in the main function, we can see that verify function is called by providing key (entered by the user) as argument/parameters:

The key verification process is performed by the verify function, which takes four integers extracted from the key input. The function performs several arithmetic operations and checks if the result matches certain values.

Verify Function:

Given the constraints within the verify function, we can represent the problem as a set of equations:

To efficiently solve these equations, we employ the Z3 theorem prover, a powerful tool for constraint solving. I used python’s Z3 library to find the values of the four integers required for a valid key:

from z3 import *

var1, var2, var3, var4 = Ints('var1 var2 var3 var4')

# Defining constraints
constraints = [
    (var3 + var1 * var2) - var4 == 873457778,
    var2 - var1 == 24297,
    (var3 * -5) + var4 == -378312,
    (var2 + var4) % 100000 == 16595
]

# Creating a solver instance
solver = Solver()

# Add constraints to the solver
solver.add(constraints)

# Checking if the constraints are satisfiable
if solver.check() == sat:
    # Getting the satisfying model
    model = solver.model()

    # Extracting values of variables
    valVar1 = model[var1].as_long()
    valVar2 = model[var2].as_long()
    valVar3 = model[var3].as_long()
    valVar4 = model[var4].as_long()

    # Printing key
    print(str(valVar1) + "-" + str(valVar2) + "-" + str(valVar3) + "-" + str(valVar4))
else:
    print("Constraints are unsatisfiable.")

Execute the Python script, which will compute the values of the four integers based on the provided constraints:

Testing against local binary:

Running against remote server to get the flag:

Flag:

AT24{d1d_y0u_us3_z3_0r_d1d_1t_m4nually??}