Regex Crossword Solver with Z3

1. Problem Statement

Regex Crossword (https://regexcrossword.com/) is a crossword puzzle where you fill in a rectangular board, so that regular expressions on every row and column are satisfied. It looks like this.

During fun geeky solving time, I thought it could be solved with computer. And actually there are great works with Regex Crossword solvers.

Herman Schaaf has solved it in Go-lang (http://herman.asia/solving-regex-crosswords-using-go). His solution analyzes the DFA generated by Go-lang’s regular expression compiler. His solution solves it really fast, that it only takes few miliseconds to solve one, but it cannot deal with backreferences.

Thomas Parslow has solved hexagonal version in Haskell (http://almostobsolete.net/regex-crossword/part1.html). His approach is basically same as solving by hand. He wrote a custom regular expression engine to do that. His solution can solve ones with backreferences, very quickly.

I’ve decided to take another approach, using SMT solver.

Read more

32C3 CTF - gurke

Non-standard gurke: https://32c3ctf.ccc.ac/uploads/gurke Talk to it via HTTP on http://136.243.194.43/.

Gurke is German for ‘cucumber’. Server runs this code:

#!/usr/bin/env python
import sys
import os

import socket
import pickle
import base64
import marshal
import types
import inspect
import encodings.string_escape

class Flag(object):
    def __init__(self):
        s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
        s.connect(("172.17.0.1", 1234))
        self.flag = s.recv(1024).strip()
        s.close()
flag = Flag()

from seccomp import *

f = SyscallFilter(KILL)
f.add_rule_exactly(ALLOW, "read")
f.add_rule_exactly(ALLOW, "write", Arg(0, EQ, sys.stdout.fileno()))
f.add_rule_exactly(ALLOW, "write", Arg(0, EQ, sys.stderr.fileno()))
f.add_rule_exactly(ALLOW, "close")
f.add_rule_exactly(ALLOW, "exit_group")

f.add_rule_exactly(ALLOW, "open", Arg(1, EQ, 0))
f.add_rule_exactly(ALLOW, "stat")
f.add_rule_exactly(ALLOW, "lstat")
f.add_rule_exactly(ALLOW, "lseek")
f.add_rule_exactly(ALLOW, "fstat")
f.add_rule_exactly(ALLOW, "getcwd")
f.add_rule_exactly(ALLOW, "readlink")
f.add_rule_exactly(ALLOW, "mmap", Arg(3, MASKED_EQ, 2, 2))
f.add_rule_exactly(ALLOW, "munmap")
f.load()

data = os.read(0, 4096)
try:
    res = pickle.loads(data)
    print 'res: %r\n' % res
except Exception as e:
    print >>sys.stderr, "exception", repr(e)

os._exit(0)

Everyone knows that unpickling user provided data is dangerous. I’ve used arbitrary code execution pickle from https://www.cs.uic.edu/~s/musings/pickle.html.

We cannot just “print flag.flag”, because the context where our code is executed is inside pickle module of remote server. So we needed some workaround by reading:

vars(sys.modules['__main__'])['flag'].flag

Read more

32C3 CTF - ey_or

We have a large (24MB) x86_64 ELF executable. It’s very difficult to reverse engineer this size. Instead, one of the printable strings looked interesting.

$ strings ey_or
    (...)
] ==secret
] ==f
 secret len ==l
 [ ] ==buffer
 0 ==i
 0 ==j
 "Enter Password line by line\n" sys .out .writeall
  #str .fromArray secret bxor
  txt .consume .u
  =j
[ buffer _ len dearray j ] =buffer
[ secret _ len dearray j eq { } { 1 sys .exit } ? * ] =secret
  i 1 add =i
  i l eq {
  buffer f bxor str .fromArray sys .out .writeall
 0 sys .exit
} { } ? *
} sys .in .eachLine
"ey_or" sys .freeze

Read more

32C3 CTF - blobberry

We made this new Raspberry Pi OS, check it out!

1. Inspect image

The problem contains an image file (blobberry.img) and a link to install instruction. The instruction is about installing an OS on real Raspberry Pi device, which we don’t have. So we decided to run it on qemu. We followed this instruction.

$ file blobberry.img
blobberry.img: x86 boot sector
$ fdisk -l blobberry.img

Disk blobberry.img: 68 MB, 68157440 bytes
87 heads, 4 sectors/track, 382 cylinders, total 133120 sectors
Units = sectors of 1 * 512 = 512 bytes
Sector size (logical/physical): 512 bytes / 512 bytes
I/O size (minimum/optimal): 512 bytes / 512 bytes
Disk identifier: 0x2fa1ab6c

        Device Boot      Start         End      Blocks   Id  System
blobberry.img1   *        8192      139263       65536    c  W95 FAT32 (LBA)
$ sudo mount blobberry.img -o offset=4194304 /mnt
$ ls /mnt
bootcode.bin UART.TXT
$ file /mnt/bootcode.bin
bootcode.bin: data

Everything went well until we saw that the image contains only two files. The image supposed to contain /etc/ld.so.preload file, but it didn’t. UART.TXT is just a funny text file explaining where is UART port. And bootcode.bin seemed to be our task. After some googling, we’ve found that bootcode.bin is “secondary boot loader” that runs on Raspberry Pi’s GPU.

Read more

안드로이드 앱 패킷 캡쳐하기

디버깅이나 리버싱을 하기 위해 앱에서 나가거나 앱으로 들어오는 패킷을 봐야 할 때가 있다. 그럴 때 tcpdump와 socat을 사용하면 앱과 서버 사이에 오가는 HTTP, HTTPS 패킷을 볼 수 있다.

준비물

• 안드로이드 폰 (루팅 필요 없음) or 에뮬레이터
• 우분투 서버 (루트 권한 필요)

Read more