This is (yet another) posthumous writeup from NorthSec, on the MarsAnalytica challenge. It features a heavily (rop)fuscated binary which accepts a 19-character pin; if the pin is correct, it produces a flag, and otherwise prints an access denied message.

Unfortunately, running angr on the challenge doesn’t work in a reasonable amount of time; I instead opt to guide angr to the solution by stopping at the first symbolic branch:

p = angr.Project("./MarsAnalytica")
s = p.factory.entry_state(add_options=angr.options.unicorn)
sm = p.factory.simulation_manager(s)
sm.step(until=lambda lpg: len(lpg.active) > 1)

This code should stop at the first logical “check” of our input, and after 10 minutes or so the step function exits, and drops us into a repl:

$ python -i soln.py
>>>> sm
<SimulationManager with 2 active>
>>>> list(sm.active[1].guards)[-1]
<Bool 0x0#56 .. file_/dev/stdin_24_1_789_8[31;0] >s 0x20>

Here we see there are two active paths, the second of which has a path predicate that constrains a byte of our input to a value > 0x20. This is just an ascii check! Since the second active path is clearly the one we want, we can easily drop the first one and continue:

sm.drop(stash='active', filter_func=lambda s: s != sm.active[1])
sm.step(until=lambda lpg: len(lpg.active) > 1)

As we continue we see similar ascii checks for 0x20 and 0x7f on each byte of stdin. There are going to be 38 of these, and it would be tedious to comb through all of these by hand; we can blow past these by revising our script:

def constrain_stdin(st):
    for _ in xrange(19):
        k = st.posix.files[0].read_from(1)
        st.solver.add(k > 0x20)
        st.solver.add(k < 0x7f)
    st.posix.files[0].seek …

ELF

Verilog

Description

This was a pretty difficult crypto challenge that ended up involving some reverse engineering. It took a while to get any solves, we got it third. Thanks to @nullptr for what turned out to be a really fun challenge (and thanks for not giving in and giving us source :) )

Given is an ELF, which is a Rust binary, and a Verilog file which contains a ‘circuit’.

Example command line input:

Server: ./smcauth verify --netlist smcauth_syn.v --secret $(python -c 'print "A"*(256/8)')
Client: ./smcauth auth --netlist smcauth_syn.v --verifier 127.0.0.1:5331 --secret $(python -c 'print "A"*32')

The verify command runs a server and the auth command runs a client (ostensibly, the challenge server is running as verify). The server (verify) takes --netlist, which is supposed to be the verilog file, and a --secret, which must be 32 printable ascii characters. The client (auth) takes --netlist (the verilog file), --verifier, which is the IP of the server, and --secret (also 32 printable ascii). When the server runs with a secret x, if a client connects with the same secret x the server will return “INFO authentication successful”, but if a client connects with a different secret y the server returns “WARN authentication failed”. We figured that the secret being passed by the server would be the flag, and it was incumbent upon us to input a secret that evaluated successfully.

Solution

From the circuit given and the behavior, it was easy to deduce that this was a Garbled Circuit . If you aren’t familiar with these, I’d highly recommend reading through the protocol before continuing.

In our case, the server is the “generator” or “garbler”, referred to as Alice in the Wikipedia, and the client is the “evaluator”, referred to as Bob …

Challenge description:

It is pitch black.

You are likely to be eaten by a grue.

Hint: “You can find the yellow orb in the maze.”

Introduction

This was a (reasonably) fun challenge from Plaid CTF this year, and one of the only reversing challenges I got to do. Unfortunately we solved this challenge posthumously, and only solved it after we were given a hint on IRC after the CTF had ended.

First things first, the program files comprised a web-based interface for a MUD-type game. The game is surprisingly simple; we need to:

1. Collect 4 colored orbs
2. Collect the silver key
3. Unlock a door
4. Insert the 4 orbs into a statue

Afterwards we can touch each orb; after 48 tries a message pops up:o

The orbs darken for a second. It seems like the code wasn't accepted.

Looks like we need to touch the orbs in a certain order in order to get the flag.

Analysis

Digging through the program files, we notice a Plaid Adventure.gblorb file, which is of a known file format to file:

$ file Release/Plaid\ Adventure.gblorb 
Release/Plaid Adventure.gblorb: IFF data, Blorb Interactive Fiction with executable chunk

This is a well-known file format which contains bytecode commonly used for implementing games; the bytecode is for the glulx virtual machine. A decompiler for this file format can be found here.

The important bits we decompiled and subsequently cleaned up are shown below:

[ routine53995 local0 ;
  ...
    if (routine146071(10,local0,269) == 1) {
        TouchSphere(465371-->counter,0);
    }
    if (routine146071(10,local0,269) == 2) {
        TouchSphere(465371-->counter,1);
    }
    if (routine146071(10,local0,269) == 3) {
        TouchSphere(465371-->counter,2);
    }
    if (routine146071(10,local0,269) == 4) {
        TouchSphere(465371-->counter,3);
    }
    465371-->counter = 465371-->counter + 1;
    if (465371-->counter == 48) {
        if (CheckSpheres() == 1) {
            ...
            PrintFlag();
            ...
        } else {
            ...
        }
    }
    ...
    return 0;
];

[ TouchSphere …

Challenge description

Category: rev
Points: 215 (dynamic, calculated from solves)
Solves: 18

This is not compatible with emacs!

Tested with vim 7.4 on amd64 Ubuntu 16.04 (package vim 2:7.4.1689-3ubuntu1.2)

Difficulty: Easy

Preface

There are a lot of words here. If you looked at the challenge during the competition and just missed a few things, you might want to skip ahead to the high-level loop summary section.

Understanding the challenge file

Vim refresher

If you’re a complete Vim beginner, I recommend going through vimtutor. Just run it from a shell.

Here’s a list of every command that this challenge uses (all in normal mode):

• h
• j
• k
• l
• ^
• $
• 0
• G
• f
• F
• t
• Y
• y
• @
• "
• r (only after you get the flag)
• d (only after you get the flag)

If you don’t know what some of them do, look them up in Vim’s help like: :help j or :h j. You might also be interested in the general concepts:

• count (and the rest of notation or the whole intro.txt file)
• registers
• quote_quote
• quote_alpha

and the command :registers for debugging. As an aside, the most common way I know to interact with registers is with q, which puts typed characters into the given register as a way to record macros. qx … @x was a pattern I learned when I was a beginner, but I didn’t make the connection to registers for a long time.

Another thing to know is that @ execution will stop when a command fails to execute. For example, qx0hl@x will put 0hl in register "x and try to run it, but because 0h goes to the first character, h can’t move left and it will stop executing before moving right with l. I found this …

LLVM Obfuscator is an industry-grade obfuscator which we have encountered frequently in the past few years of CTFing. This blog post documents our work in understanding the design of the obfuscator itself, as well as any possible weaknesses in the implementations of the obfuscation passes. We use this work to automate the task of emitting cleaned and working binaries via Binary Ninja.

Introduction

The open source LLVM Obfuscator manifests as 3 relatively disjoint LLVM passes, each implementing some sort of obfuscation that obscures the CFG or arithmetic computation of the original program in some way.

Also note that, due to the fact that these passes operate over LLVM IR, it supports almost every architecture under the sun.

Information for each of the three passes can be found here:

• Instructions Substitution
• Bogus Control Flow
• Control Flow Flattening

These are simply the documentation pages maintained by the authors for each respective pass. However, if the documentation is deficient, the source is also an obvious ground truth.

Unfortunately, the llvm-obfuscator repo maintains multiple branches, one for each version of LLVM that that branch targets, with a clone of the entire LLVM repository, so it’s easy to get lost in the code. The passes for the 4.0 branch can be found here, in the lib/Transforms folder, as is customary for LLVM passes.

This blog post will focus on the control flow flattening pass, as we find it to be one of the most interesting passes in the LLVM Obfuscator ecosystem, as well as the most effective.

Control Flow Flattening

We can visualize the effects of the Control Flow Flattening pass as the following CFG transformation:

1. Collect all of the original basic blocks in a CFG
2. Lay them down flat “at the bottom” of the CFG, and remove all original edges
3. Add …