Kategori
Programmering
Beskrivning
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å undutmaning-mindreprat.chals.io:443.
Nu behöver hon bara lista ut vad som är ett godkänt lösenord!
Lösning
Till utmaningen bifogas en fil, server.st, som innehåller källkoden till servern. Koden är skriven i Smalltalk, ett objektorienterat programspråk som är känt för att vara mycket enkelt att läsa och skriva.
'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.
Här ser vi alla krav som lösenordet måste uppfylla. Det liknar en klassisk SAT-problem, där vi har en mängd villkor som alla måste vara sanna för att lösenordet ska vara korrekt.
För att lösa uppgiften kan vi använda oss av z3, ett SAT-lösningsverktyg som kan hjälpa oss att hitta en lösning på problemet.
#!/usr/bin/env python3
from z3 import *
def printModel(model):
found = []
for idx in range(0, length):
strVal = str(model[pw_vars[idx]])
found.append(chr(int(strVal)))
print(''.join(found))
length = 16
s = Solver()
pw_vars = [BitVec('pw_var_%d' % i, 8) for i in range(length)]
for i in range(length):
s.add(pw_vars[i] >= ord('a'), pw_vars[i] <= ord('z'))
s.add(pw_vars[5] - pw_vars[3] < -4)
s.add(pw_vars[11] - pw_vars[0] == -5)
s.add(pw_vars[4] ^ pw_vars[12] == 2)
s.add(pw_vars[13] ^ pw_vars[1] == 19)
s.add(pw_vars[10] | pw_vars[1] == 126)
s.add(pw_vars[7] | pw_vars[4] == 108)
s.add(pw_vars[15] ^ pw_vars[6] == 16)
s.add(pw_vars[8] ^ pw_vars[9] == 9)
s.add(pw_vars[2] + pw_vars[11] == 226)
s.add(pw_vars[14] - pw_vars[3] == -5)
s.add(pw_vars[8] | pw_vars[7] == 125)
s.add(pw_vars[3] + pw_vars[11] < 226)
s.add(pw_vars[5] ^ pw_vars[9] == 8)
s.add(pw_vars[11] | pw_vars[10] == 111)
s.add(pw_vars[1] ^ pw_vars[3] == 2)
s.add(pw_vars[12] ^ pw_vars[2] == 25)
s.add(pw_vars[9] ^ pw_vars[15] == 26)
if s.check() == unsat:
print("No solution found")
exit(1)
printModel(s.model())
När vi kör skriptet får vi ut lösenordet ptwvlprlqxnkngqb. Ansluter vi till servern och skriver in lösenordet får vi ut flaggan.
sc undutmaning-mindreprat.chals.io 443
(connected to undutmaning-mindreprat.chals.io:443 and reading from stdin)
Enter the password: ptwvlprlqxnkngqb
undut{sat-solvers-are-magic}