Haard Majmudar

Description: Maybe software isn’t so bad after all… My current password l3ak{...} seems to be working fine, but something tells me someone else has been messing around on my machine 💀. Note: This challenge is the revenge challenge for Software is a scam. It is suggested that you solve that one first.

After solving the electronics homework, we got a seizure by just looking at this circuit.

On solving this set of equations we got 2 solutions, which were l3ak and L3AK.

The description mentioned that the current password worked fine, which is l3ak{...}. We ignored L3AK, for now.

Divider Logic

If we observe every gate connected to a divider , we observe that all of the gates are commutative gates.

Pin	Character
`c1`	`l`
`c2`	`3`
`c3`	`a`
`c4`	`k`
`c5`	`{`
`c34`	`}`

We know that OR is a commutative gate (which means a or b = b or a), so the output will be:

We checked for a couple of them and assumed all were this exact logic because it doesn’t make sense to solve the whole circuit, it had to be a reduction of sorts.

Equation derivation:

from z3 import *

c1 = BitVec('c1', 8)
c3 = BitVec('c3', 8)
c4 = BitVec('c4', 8)

names = [f'c{i}' for i in range(6, 34)]
c = {i: BitVec(f'c{i}', 8) for i in range(6, 34)}

s1 = LShR(c1, 5)   
s3 = LShR(c3, 5)
s4 = LShR(c4, 5)

solver = Solver()
solver.add(c1 == 0x6c)
solver.add(c3 == 0x61)
solver.add(c4 == 0x6b)

eqs = [
    (6,  s1, 0x11, 0x20, 'sub'),
    (7,  s3, 0x41, 0xb2, 'sub'),
    (8,  s4, 0x0d, 0x49, 'sub'),
    (9,  s1, 0x38, 0xdb, 'add'),
    (10, s3, 0x0e, 0x48, 'sub'),
    (11, s4, 0xd1, 0xd2, 'add'),
    (12, s1, 0x3a, 0xe3, 'add'),
    (13, s3, 0x41, 0xf0, 'xor'),
    (14, s4, 0x04, 0x57, 'sub'),
    (15, s1, 0x13, 0x8e, 'add'),
    (16, s3, 0x41, 0xaf, 'sub'),
    (17, s4, 0x31, 0xc6, 'add'),
    (18, s1, 0x05, 0x6e, 'add'),
    (19, s3, 0xc3, 0xb9, 'add'),
    (20, s3, 0x1a, 0x82, 'add'),
    (21, s1, 0x14, 0x37, 'sub'),
    (22, s3, 0x0a, 0x55, 'sub'),
    (23, s4, 0x29, 0xfc, 'sub'),
    (24, s1, 0xd1, 0xbd, 'sub'),
    (25, s3, 0x2a, 0xf4, 'sub'),
    (26, s4, 0x10, 0x14, 'sub'),
    (27, s1, 0x13, 0x98, 'add'),
    (28, s3, 0x0e, 0x58, 'xor'),
    (29, s4, 0x46, 0x03, 'add'),
    (30, s1, 0x33, 0xce, 'sub'),
    (31, s3, 0x0a, 0x66, 'add'),
    (32, s4, 0x52, 0xc1, 'xor'),
    (33, s1, 0x06, 0x2d, 'xor'),
]

for idx, shift_expr, mask, target, op in eqs:
    var = c[idx]
    term = shift_expr * mask   
    if op == 'sub':
        solver.add(var - term == target)
    elif op == 'add':
        solver.add(var + term == target)
    elif op == 'xor':
        solver.add(var ^ term == target)

if solver.check() == sat:
    m = solver.model()
    def val(v):
        return m.eval(v, model_completion=True).as_long()

    print(f"c1 = 0x{val(c1):02x}")
    print(f"c3 = 0x{val(c3):02x}")
    print(f"c4 = 0x{val(c4):02x}")
    print()
    for i in range(6, 34):
        print(f"c{i} = 0x{val(c[i]):02x}")

    known = {1: 0x6c, 2: 0x33, 3: 0x61, 4: 0x6b, 5: 0x7b, 34: 0x7d}

    all_bytes = dict(known)
    all_bytes[1] = val(c1)
    all_bytes[3] = val(c3)
    all_bytes[4] = val(c4)
    for i in range(6, 34):
        all_bytes[i] = val(c[i])

    flag = ''.join(chr(all_bytes[i]) for i in sorted(all_bytes))
    print()
    print(f"{flag}")
else:
    print("UNSAT")

Unfortunately, this was not the actual flag. After chatting a bit on tickets and reading the description carefully, we understood what was the intended solution.

The description mentioned:

My current password l3ak{...} seems to be working fine, but something tells me someone else has been messing around on my machine 💀.

from z3 import *

c1 = BitVec('c1', 8)
c3 = BitVec('c3', 8)
c4 = BitVec('c4', 8)

names = [f'c{i}' for i in range(6, 34)]
c = {i: BitVec(f'c{i}', 8) for i in range(6, 34)}

s1 = LShR(c1, 5)   
s3 = LShR(c3, 5)
s4 = LShR(c4, 5)

solver = Solver()
solver.add(c1 == 0x4c)
solver.add(c3 == 0x41)
solver.add(c4 == 0x4b)

eqs = [
    (6,  s1, 0x11, 0x20, 'sub'),
    (7,  s3, 0x41, 0xb2, 'sub'),
    (8,  s4, 0x0d, 0x49, 'sub'),
    (9,  s1, 0x38, 0xdb, 'add'),
    (10, s3, 0x0e, 0x48, 'sub'),
    (11, s4, 0xd1, 0xd2, 'add'),
    (12, s1, 0x3a, 0xe3, 'add'),
    (13, s3, 0x41, 0xf0, 'xor'),
    (14, s4, 0x04, 0x57, 'sub'),
    (15, s1, 0x13, 0x8e, 'add'),
    (16, s3, 0x41, 0xaf, 'sub'),
    (17, s4, 0x31, 0xc6, 'add'),
    (18, s1, 0x05, 0x6e, 'add'),
    (19, s3, 0xc3, 0xb9, 'add'),
    (20, s3, 0x1a, 0x82, 'add'),
    (21, s1, 0x14, 0x37, 'sub'),
    (22, s3, 0x0a, 0x55, 'sub'),
    (23, s4, 0x29, 0xfc, 'sub'),
    (24, s1, 0xd1, 0xbd, 'sub'),
    (25, s3, 0x2a, 0xf4, 'sub'),
    (26, s4, 0x10, 0x14, 'sub'),
    (27, s1, 0x13, 0x98, 'add'),
    (28, s3, 0x0e, 0x58, 'xor'),
    (29, s4, 0x46, 0x03, 'add'),
    (30, s1, 0x33, 0xce, 'sub'),
    (31, s3, 0x0a, 0x66, 'add'),
    (32, s4, 0x52, 0xc1, 'xor'),
    (33, s1, 0x06, 0x2d, 'xor'),
]

for idx, shift_expr, mask, target, op in eqs:
    var = c[idx]
    term = shift_expr * mask   
    if op == 'sub':
        solver.add(var - term == target)
    elif op == 'add':
        solver.add(var + term == target)
    elif op == 'xor':
        solver.add(var ^ term == target)

if solver.check() == sat:
    m = solver.model()
    def val(v):
        return m.eval(v, model_completion=True).as_long()

    print(f"c1 = 0x{val(c1):02x}")
    print(f"c3 = 0x{val(c3):02x}")
    print(f"c4 = 0x{val(c4):02x}")
    print()
    for i in range(6, 34):
        print(f"c{i} = 0x{val(c[i]):02x}")

    known = {1: 0x4c, 2: 0x33, 3: 0x41, 4: 0x4b, 5: 0x7b, 34: 0x7d}

    all_bytes = dict(known)
    all_bytes[1] = val(c1)
    all_bytes[3] = val(c3)
    all_bytes[4] = val(c4)
    for i in range(6, 34):
        all_bytes[i] = val(c[i])

    flag = ''.join(chr(all_bytes[i]) for i in sorted(all_bytes))
    print()
    print(f"{flag}")
else:
    print("UNSAT")

Hardware is a Scam

Divider Logic

Equation derivation: