← Back to Writeups
CUSTOMMediumReversing
Bookmark

equhs

XESXOR9/10/20265 min read
#reversing#custom#medium#ascii_constraint_recovery#linear_system_over_z256#z3_bitvec_solving

equhs

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Medium | OS: NA | Author: XESXOR | Date: 2026-07-02 | Status: Solved Techniques: ascii_constraint_recovery, linear_system_over_z256, z3_bitvec_solving

Summary

Task: Haskell crackme (equhs.hs) that treats the input as a 20-char vector and checks M·x ≡ S (mod 256) for a hardcoded 20×20 matrix. Solution: model the 20 modular linear equations plus printable-ASCII constraints (32 < x < 127) in z3 with BitVec unknowns; naive Gaussian elimination fails because 256 = 2^8 is not a field. z3 uniquely recovers the flag.

equhs — spbctf

Description

Why not file. Run: apt install ghc; ghc equhs.hs; ./equhs

English summary: A Haskell source file equhs.hs is a crackme. It reads one line of input and prints True or False. The goal is to find the input that makes it print True — that input is the flag.

Analysis

Reading equhs.hs, the core logic is:

  • to_int maps the input string to a list of character codes (fromEnum).
  • The input is filtered to printable ASCII with filter (> 32) (filter (< 127) ...) — keeping only chars c where 32 < c < 127.
  • calc1 acc (y, z) = mod (acc + y*z) 256
  • calculate1 y x = foldl calc1 0 (zip y x) computes (Σⱼ yⱼ · xⱼ) mod 256 — a dot product of the input vector y with a matrix row x, taken mod 256.
  • check y xs sx returns, for each matrix row xᵢ and target value sᵢ, the value calculate1 y xᵢ - sᵢ.
  • main compares the resulting 20-element list against [0,0,...,0] (20 zeros) with compare_lists. It prints True only when calculate1 y rowᵢ ≡ sᵢ (mod 256) for every row. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

So this is a system of 20 linear equations over ℤ/256 in 20 unknowns (the 20 input characters):

M · x ≡ S  (mod 256)

where M is the 20×20 matrix embedded in the source and S is the target vector.

Key gotcha: mod 256 = 2⁸ is not a field (it is the ring ℤ/256). Straightforward Gaussian elimination breaks down whenever a pivot is even, since even elements are not invertible mod 256. Rather than doing Hensel lifting / a proper Smith-normal-form solve, the clean route is z3: model each unknown as a BitVec, add the 20 modular equations, and add the printable-ASCII constraint 32 < xᵢ < 127. Those bounds make the solution unique. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Solution

The 20×20 matrix M and target vector S (verbatim from equhs.hs):

S = [61, 228, 94, 109, 218, 126, 203, 95, 215, 205,
     89, 141, 101, 11, 88, 148, 223, 222, 13, 189]

z3 solver (solve2.py) — the essential part:

 python 
from z3 import *

M = [
 [151, 244, 231, 33, 247, 110, 1, 233, 89, 6, 223, 35, 181, 255, 164, 160, 143, 168, 142, 6],
 [72, 99, 103, 36, 118, 175, 68, 1, 116, 51, 209, 190, 140, 94, 180, 41, 106, 33, 54, 251],
 [198, 241, 187, 220, 144, 245, 255, 234, 66, 107, 245, 160, 236, 78, 36, 239, 120, 51, 208, 17],
 [52, 194, 199, 18, 4, 221, 251, 125, 230, 168, 7, 204, 15, 120, 97, 252, 154, 176, 142, 108],
 [139, 116, 120, 51, 183, 28, 217, 184, 31, 110, 119, 68, 114, 198, 62, 175, 213, 14, 53, 163],
 [224, 78, 211, 23, 253, 176, 119, 9, 143, 232, 143, 247, 31, 28, 127, 121, 101, 239, 185, 35],
 [104, 61, 81, 54, 78, 166, 40, 108, 31, 42, 119, 49, 207, 37, 147, 204, 139, 234, 218, 59],
 [136, 201, 66, 252, 19, 217, 125, 44, 31, 128, 36, 125, 15, 219, 199, 61, 36, 88, 46, 104],
 [3, 211, 232, 14, 74, 47, 131, 128, 106, 23, 2, 183, 108, 156, 40, 186, 154, 145, 106, 233],
 [154, 14, 83, 77, 27, 147, 67, 42, 17, 117, 148, 109, 24, 109, 100, 93, 52, 35, 73, 25],
 [200, 230, 233, 252, 73, 201, 253, 49, 19, 112, 157, 33, 25, 49, 27, 56, 58, 88, 19, 234],
 [233, 253, 67, 219, 60, 159, 183, 118, 105, 209, 157, 210, 188, 101, 213, 153, 222, 154, 163, 56],
 [219, 49, 157, 95, 79, 6, 95, 216, 244, 237, 142, 241, 22, 145, 38, 29, 190, 198, 139, 252],
 [115, 97, 254, 101, 132, 121, 88, 162, 84, 202, 42, 98, 108, 78, 249, 75, 132, 31, 144, 81],
 [197, 178, 78, 169, 41, 13, 218, 51, 225, 246, 234, 230, 4, 6, 102, 181, 53, 159, 33, 65],
 [76, 214, 107, 56, 207, 175, 250, 172, 186, 180, 28, 234, 150, 160, 49, 232, 234, 125, 205, 247],
 [203, 83, 253, 84, 160, 138, 5, 34, 100, 184, 194, 173, 238, 156, 79, 224, 170, 70, 55, 13],
 [153, 210, 57, 220, 4, 191, 185, 52, 85, 112, 112, 224, 108, 251, 124, 138, 211, 228, 47, 88],
 [25, 148, 172, 211, 57, 17, 33, 43, 79, 47, 192, 2, 254, 229, 120, 41, 186, 247, 62, 192],
 [149, 118, 168, 227, 208, 44, 164, 171, 116, 232, 59, 168, 29, 136, 122, 1, 132, 118, 77, 117],
]
S = [61, 228, 94, 109, 218, 126, 203, 95, 215, 205,
     89, 141, 101, 11, 88, 148, 223, 222, 13, 189]
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

n = 20
x = [BitVec(f'x{i}', 16) for i in range(n)]
s = Solver()

# printable-ASCII bounds mirror the Haskell filter (> 32) . filter (< 127)
for i in range(n):
    s.add(x[i] > 32, x[i] < 127)

# one modular linear equation per matrix row: (Σ_j x_j * M[i][j]) % 256 == S[i]
for i in range(n):
    expr = 0
    for j in range(n):
        expr = expr + x[j] * M[i][j]
    s.add((expr % 256) == S[i])

print(s.check())            # sat
m = s.model()
print(''.join(chr(m[x[i]].as_long()) for i in range(n)))

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Running it:

$ python3 solve2.py
sat
spbctf{REDACTED}

Note the wordplay in the flag: "glaf" ≈ "flag" (letters shuffled), a nod to the Haskell theme. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍