Rating:
Sometime, less ~instruction~ equal more ~instruction~ ...
LessEQualmore is a subleq virtual machine running a challenge program. The provided program asks for a flag and verifies it.
When run the program repeats the input back to you and then verifies it (which hints at the buffer overflow for the SUBformore pwn challenge).
*** Flag Checker ***
hitcon{flag}
You entered:
hitcon{flag}
Sorry, wrong flag!
The problem is that the challenge program contains 44197 tokens, has different alignments in different positions and as subleq programs are is heavily self-modifying. This means that fully understanding the challenge program is a very tedious task as we need to explore traces and the possible paths the program might take depending on input.
These types of challenges are possible to solve way faster assuming they following some common properties / are not hardened:
In practice this means that if the program compares the input in some way and directly decides if it is correct or not from that, we can focus on finding these comparisons and derive the correct input from there.
So how do we find these comparisons?
Given that every subleq instruction can be seen as a branch we first to ignore everything obviously is not a jump (meaning the next address is the same as the branch address). We also only want to focus on branches that depend on the input values, and filter out everything that always takes the same path for printable input characters.
We can do this by rewriting the subleq VM and making the input symbolic variables. Through this we can do taint analysis and figure out what the comparisons are actually doing. We can also use a solver to verify whether for any possible input a branch can be taken or not. The nature of subleq leads itself to reusing specific memory regions a lot, so after a memory cell is zero'd we should also make it concrete / non-symbolic again as this is important for performance and helps with figuring out better candidates.
When you do this you will find a lot of possible candidates and it will take quite a long time to compute. To further restrict the space we can also try the assumption (which may not be true but we can easily test) that the comparison of characters is not just with each other but contains some constant.
See the explore.py script for an implementation of this search.
I recommend trying this with a small amount of input characters first (e.g. 8, which you can see is the block size of comparisons):
PC[ 3314 ]: ( 0 1 3320 ) : 3016 +
18446744073709551609*input[0] +
18446744073709551612*input[3] +
18446744073709551603*input[5] +
18446744073709551614*input[6] +
18446744073709551609*input[7] +
18446744073709551614*input[1] +
3*input[2] +
4*input[4] # Possible Solution: b'y~ ~#1A~'
PC[ 3314 ] is for completely wrong input (e.g. all A's) the only comparison that is found.
Note that negative numbers are here shown as unsigned 64-bit numbers, so this actually means:
PC[ 3314 ]: ( 0 1 3320 ) : 3016 +
-7*input[0] +
-4*input[3] +
-13*input[5] +
-2*input[6] +
-7*input[7] +
-2*input[1] +
3*input[2] +
4*input[4] # Possible Solution: b'y~ ~#1A~'
If we now try this as input and explore again:
PC[ 3314 ]: ( 0 1 3320 ) : 3016 +
18446744073709551609*input[0] +
18446744073709551612*input[3] +
18446744073709551603*input[5] +
18446744073709551614*input[6] +
18446744073709551609*input[7] +
18446744073709551614*input[1] +
3*input[2] +
4*input[4] # Possible Solution: b'T231Cy8|'
PC[ 3320 ]: ( 1 0 3386 ) : 18446744073709548600 +
7*input[0] +
4*input[3] +
13*input[5] +
2*input[6] +
7*input[7] +
2*input[1] +
18446744073709551613*input[2] +
18446744073709551612*input[4] # Possible Solution: b'"*Os%uzz'
PC[ 3314 ]: ( 0 1 3320 ) : 18446744073709550205 +
5*input[3] +
18446744073709551606*input[5] +
11*input[6] +
18446744073709551613*input[7] +
6*input[4] +
3*input[1] +
2*input[2] +
18446744073709551614*input[0] # Possible Solution: b'l0<iN7ph'
PC[ 3320 ]: ( 1 0 3386 ) : 1411 +
18446744073709551611*input[3] +
10*input[5] +
18446744073709551605*input[6] +
3*input[7] +
18446744073709551610*input[4] +
18446744073709551613*input[1] +
18446744073709551614*input[2] +
2*input[0] # Possible Solution: b'#}_eA",)'
Through these explorations and manually matching them (and some further experiments) we can figure out that at address 3311 , 3314 and 3320 the actual comparisons happen. At these addresses additional comparisons happen which for correct input do not lead to equality with zero but to less equal zero.
See the solve.py script that uses this knowledge to extracts the constraints and fake the comparisons to match to not stop execution. Through trying different input lengths we can see that the input is verified in blocks of 8, and the actual flag length is 64 characters.
The actual script takes quite a while to run because of all the constraint checking and solving, but after 10-30 minutes we get the flag (see log.txt) :
hitcon{r3vErs1ng_0n3_1ns7ruction_vm_1s_Ann0ying_c9adf98b67af517}
