Mindre prat

Published: 2025-04-12

Difficulty

Easy

Description

Under sin jakt efter några uppslag på hur hon ska ta sig hem har Harriet stött på något intressant. Hon har hittat källkoden till vad som verkar vara en minimal autentiseringsmodul till något av de många system Kenneth tagit över.

Hon får en vag känsla av att vara lite lätt objektifierad och meddelandeorienterad när hon läser den.

Efter ytterligare lite rotande hittar hon ett system som kör tjänsten, på [Challenge URL removed].

Nu behöver hon bara lista ut vad som är ett godkänt lösenord!

Om du behöver hjälp med att ansluta finns information om hur du gör för att ansluta till utmaningstjänster på informationssidan.

Har du kört fast? Det här kanske är ett bra tillfälle att lära sig mer om Satisfiability Solvers…

Provided files

server.st

'Enter the password: ' display.
s := ([ stdin nextLine ] on: Error do: ['']) asByteArray.
chars := 'abcdefghijklmnopqrstuvwxyz0123456789'.
ok := (s size) == 16 and: [
    (s allSatisfy: [ :c | chars includes: (c asCharacter)])
        & (((s at: 6)  -       (s at: 4))  <  -4)
        & (((s at: 12) -       (s at: 1))  == -5)
        & (((s at: 5)  bitXor: (s at: 13)) == 2)
        & (((s at: 14) bitXor: (s at: 2))  == 19)
        & (((s at: 11) bitOr:  (s at: 2))  == 126)
        & (((s at: 8)  bitOr:  (s at: 5))  == 108)
        & (((s at: 16) bitXor: (s at: 7))  == 16)
        & (((s at: 9)  bitXor: (s at: 10)) == 9)
        & (((s at: 3)  +       (s at: 12)) == 226)
        & (((s at: 15) -       (s at: 4))  == -5)
        & (((s at: 9)  bitOr:  (s at: 8))  == 125)
        & (((s at: 4)  +       (s at: 12)) <  226)
        & (((s at: 6)  bitXor: (s at: 10)) == 8)
        & (((s at: 12) bitOr:  (s at: 11)) == 111)
        & (((s at: 2)  bitXor: (s at: 4))  == 2)
        & (((s at: 13) bitXor: (s at: 3))  == 25)
        & (((s at: 10) bitXor: (s at: 16)) == 26)
].
'' displayNl.
ans := ok
    ifTrue:  [ ans := (FileStream open: 'flag.txt') nextLine ]
    ifFalse: ['Incorrect!'].
ans displayNl.

Solution

Understanding the Code

When examining this server.st file written in Smalltalk, the first step is to understand that we’re looking at a password validation system with multiple mathematical constraints that must all evaluate to true. The code reads user input, checks it against 16 specific conditions using bitwise operations and arithmetic comparisons, and only provides the flag if all conditions are satisfied.

To solve this challenge, we need to find a 16-character string that satisfies all the constraints defined in the code.

The password must be 16 characters long.
Each character must be from the set: lowercase letters (a-z) or digits (0-9).
There are 16 mathematical constraints between specific character positions.

This is a constraint satisfaction problem (CSP) that can be solved using an SMT solver like Z3.

Using Z3 to Solve the Problem

We need to translate the constraints from the Smalltalk code into Z3’s constraint language. This involves conversion of the bitwise operations, arithmetic comparisons, and position indexing from Smalltalk’s 1-based indexing to Python’s 0-based system. By expressing all 16 constraints mathematically, Z3 can efficiently search for a valid password that satisfies all conditions simultaneously.

from z3 import *

# Create solver
solver = Solver()

# Define variables for each character position (0-15)
chars = [BitVec(f'char_{i}', 8) for i in range(16)]

# Ensure all characters are valid (a-z, 0-9)
valid_chars = "abcdefghijklmnopqrstuvwxyz0123456789"
for c in chars:
    constraints = [c == ord(valid_char) for valid_char in valid_chars]
    solver.add(Or(constraints))

# Add all constraints from the Smalltalk code
# Converting from 1-based (Smalltalk) to 0-based (Python) indexing
solver.add(chars[5] - chars[3] < -4)        # (s at: 6) - (s at: 4) < -4
solver.add(chars[11] - chars[0] == -5)      # (s at: 12) - (s at: 1) == -5
solver.add(chars[4] ^ chars[12] == 2)       # (s at: 5) bitXor: (s at: 13) == 2
solver.add(chars[13] ^ chars[1] == 19)      # (s at: 14) bitXor: (s at: 2) == 19
solver.add(chars[10] | chars[1] == 126)     # (s at: 11) bitOr: (s at: 2) == 126
solver.add(chars[7] | chars[4] == 108)      # (s at: 8) bitOr: (s at: 5) == 108
solver.add(chars[15] ^ chars[6] == 16)      # (s at: 16) bitXor: (s at: 7) == 16
solver.add(chars[8] ^ chars[9] == 9)        # (s at: 9) bitXor: (s at: 10) == 9
solver.add(chars[2] + chars[11] == 226)     # (s at: 3) + (s at: 12) == 226
solver.add(chars[14] - chars[3] == -5)      # (s at: 15) - (s at: 4) == -5
solver.add(chars[8] | chars[7] == 125)      # (s at: 9) bitOr: (s at: 8) == 125
solver.add(chars[3] + chars[11] < 226)      # (s at: 4) + (s at: 12) < 226
solver.add(chars[5] ^ chars[9] == 8)        # (s at: 6) bitXor: (s at: 10) == 8
solver.add(chars[11] | chars[10] == 111)    # (s at: 12) bitOr: (s at: 11) == 111
solver.add(chars[1] ^ chars[3] == 2)        # (s at: 2) bitXor: (s at: 4) == 2
solver.add(chars[12] ^ chars[2] == 25)      # (s at: 13) bitXor: (s at: 3) == 25
solver.add(chars[9] ^ chars[15] == 26)      # (s at: 10) bitXor: (s at: 16) == 26

# Check if solvable
if solver.check() == sat:
    model = solver.model()
    
    # Extract the solution and order the characters correctly
    solution = []
    for i in range(16):
        solution.append(chr(model[chars[i]].as_long()))
    
    password = ''.join(solution)
    print(f"Password found: {password}")
else:
    print("No solution found")

Running this script will give this output:

Password found: ptwvlprlqxnkngqb

Testing the Password

Now that we have a candidate password from our Z3 solver, we need to verify it by connecting to the challenge server. Using OpenSSL, we can establish a connection and submit our password to see if it returns the flag.

openssl s_client -connect [Challenge URL removed]:443 -servername [Challenge URL removed] -quiet
Connecting to [ip address removed]
depth=2 OU=GlobalSign Root CA - R6, O=GlobalSign, CN=GlobalSign
verify return:1
depth=1 C=BE, O=GlobalSign nv-sa, CN=GlobalSign GCC R6 AlphaSSL CA 2023
verify return:1
depth=0 CN=*.[Challenge URL removed]
verify return:1
Enter the password: ptwvlprlqxnkngqb

undut{sat-solvers-are-magic}

The flag is undut{sat-solvers-are-magic}.

Conclusion

This challenge involved solving a password validation system that enforced multiple mathematical constraints using bitwise operations and arithmetic comparisons. The system would only accept a 16-character password that satisfied all 16 mathematical relationships between specific character positions. By translating these constraints into an SMT problem, we were able to use Z3 to efficiently determine the exact password that satisfied all conditions simultaneously.