The 4th DOJO CHALLENGE was rather tricky: you needed to solve an obfuscated XPath request to derive working serials. The 3 first hunters to solve this challenge are rewarded a prestigious BlackHat Briefings pass.
Maybe you don’t know the DOJO yet?
The YesWeHack DOJO is a visual exploitation environment and training platform geared towards learning bug exploitation the fun and visual way.
Introducing the YesWeHack DOJO
The DOJO is three things in one: a learning tool, training platform and a playground.
The DOJO is the arena where the 4th challenge took place (see the announcement here).
WINNERS!
We are glad to announce the #4 DOJO Challenge winners list.
3 FIRST SOLVES (in order)
Marcosen
Pinta
SakiiR
Subscribe to our Twitter or Linkedin feeds to be notified of the upcoming challenges.
Read on to find the best write-up as well as the challenge author’s recommendations. For this instalment of the DOJO Challenges, we have selected two write-ups as their approaches are distinct and rely on different tools. Read on then!
The challenge
You have to find the seven valid serials returning the Access granted! string from the XPath query. The $serial input is filtered to restrict the input to the use of digits and hyphen (-) and 19 characters. The serials format is given: xxxx-xxxx-xxxx-xxxx where x is a single digit.
Tricky tricky… there was a hint pointing us to Microsoft Z3 Prover, but is that challenge even human-solvable?
See the challenge page >
We also asked you to produce a qualified write-up report explaining the logic allowing such exploitation. This write-up serves two purposes:
- Ensure no copy-paste would occur.
- Determine the contestant ability to properly describe a vulnerability and its vectors inside a professionally redacted report. This capacity gives us invaluable hints on your own, unique, talent as a bug hunter.
Here comes the podium
- The first solve came from MARCOSEN, who managed somehow to solve the challenge without the use of any tool! Incredibly classy.
- The second valid report is a piece of mastery crafted by PINTA, actually using Z3
- The third solve came from SakiiR, also using Z3, and the report is another masterpiece.
We were absolutely thrilled by the quality of this session’s reports.
Thank you!
PINTA’s Write-Up
Description
During the testing, I found that we need to find seven valid serials for the provided XPATH query. The format of a serial is defined as: 0000-0000-0000-0000. There are filters applied on the provided serial:
- The maximum length of a serial is 19;
- A serial can only contain 0-9 numbers and ‘-‘ character. If any other character is provided, then it will be replaced by ‘0’
I solved this challenge by writing a constraint solver using Z3 theorem prover tool.
Exploitation
1- The code is obfuscated and unreadable for me. So I took apart the query in different portions. This way I could easily read the XPATH query and understand it. See below:
2- Now, I tried to solve the equations that do not contain the $serial value, by passing the XPATH query in template parameter to endpoint /backend/xpath as shown in the image below:
3- Thus, I have solved all the possible equations and put it in the image shown in Step 1 above. It now goes like this:
4- So, we have minified the XPATH query. Please note the lines 21 and 23 in the image in Step 3:
- The line 21 with value 1 is the second argument of first substring function which indicates the starting index of string.
- The line 23 indicates the length of that string which is 15.
As we can see, the length of “Access granted!” is same as the length of “Access refused!”, and both equal to 15.
5- Now, note the second substring function which takes the output of translate()*42 as its second argument and 15 as third argument. We can thus understand that, if we want to get the “Access granted!” string, then the output of translate()*42 should not be greater than 15.
For e.g. substring("abcdefghijklmno", 16 ,15) will output nothing as second argument (i.e. starting of the string) as it is greater than the length of the string.
6- Another thing to observe is the arguments of the translate function. We can think of translate as a replace function which does not follow any order.
For e.g. translate('abc', 'cb', 'YX') will output aXY i.e. ‘c’ is replaced by ‘Y’ and ‘b’ is replaced by ‘X’, although they were in different order.
In our minified XPATH query, we could see the second argument of translate function is uareltsf and the third argument is 01001011. And the conditions (see image in step 3) from line 3 to 17 eithers outputs true or false. So, this means true will be replaced by 0000 and false will be replaced by 11110.
7- To fufill the condition in Step 5 above, we need all the values equal to true since after concatenation it will output truetruetrue.... which will be replaced 0000000000.... and Access granted! will be printed out.
However, to realise those conditions, we need to write a constraint solver. I wrote a small script using Z3 to solve it. I have also added comments in the code to make it more self-explanatory.
PoC
- Requirements: Follow the instructions here:
https://github.com/Z3Prover/z3
- install Z3.
- Run the provided solution script using python: python sol.py
Solution script: sol.py
from z3 import *
first = Int('first')
second = Int('second')
third = Int('third')
fourth = Int('fourth')
s = Solver()
s.add(0< first, first < 9999)
s.add(0 < second, second < 9999)
s.add(0 < third, third < 9999)
s.add(0 < fourth, fourth < 9999)
s.add(first % 3 == 0)
s.add(third % 9 == 0)
s.add(second % 5 == 0)
s.add(fourth % 8 == 0)
s.add(first == (second+fourth) )
s.add(second == (third-fourth-42) )
s.add( (second*3+first-third) == fourth )
serials = []
while s.check() == sat:
m = s.model()
a1, a2, a3, a4 = str(m[first]), str(m[second]), str(m[third]), str(m[fourth])
if len(a1) != 4:
a1 = '0'*(4-len(a1)) + a1
if len(a2) != 4:
a2 = '0'*(4-len(a2)) + a2
if len(a3) != 4:
a3 = '0'*(4-len(a3)) + a3
if len(a4) != 4:
a4 = '0'*(4-len(a4)) + a4
serials.append( a1 + "-" + a2 + "-" + a3 + "-" + a4)
s.add(Or(m[first] != first, m[second]!=second, m[third]!=third,m[fourth]!=fourth))
for serial in serials:
print (serial)
I found the following 7 valid serial keys:
9678-2430-9720-7248
1038-0270-1080-0768
2478-0630-2520-1848
8238-2070-8280-6168
5358-1350-5400-4008
6798-1710-6840-5088
3918-0990-3960-2928
BONUS: MARCOSEN manual solve (well, if brain had fingers)
Description
The problem here is, that only some obfuscated code is used to hide the evaluation of the serial.
Exploitation
The first part was to remove all the “static garbage” from the code. This means to evaluate all the terms that do not contain the serial. I did this by just sending the term I wanted to evaluate and checking the servers answer.
The next step was to replace all the substring-methods just to make it obvious which part of the serial should be evaluate in that part of the code. I replaced it in the code-snippet below with partX.
Looking at the substring with “granted”, we can observe that the translate-method must be 0, so that we get the substring of the beginning of “granted”. These leaves us with the information that the concatenation of the inner terms must be as follows:
not(part1 mod 3) -> true,
not(part2 mod 5) -> true,
not(part3 mod 9) -> true,
not(part4 mod 8) -> true,
part1!=(part2+part4) -> false,
part2!=(part3-part4-42) -> false,
(part2*3+part1-part3)=part4 -> true
For the math, I will replace part1-part4 with a-d. Simplifying the terms gives us seven equations:
Time to solve the equations! I started by just making it all depending on c. This gives us:
a = c-42
b = c/4
c = ?
d = 3*c/4 - 42
Ok, so c = ? How do we get the value of c? We know that c must be dividable by 9. It must also be dividable by 4, because b = c/4. Also b must be dividable by 5. So, we need the least common multiple (LCM) of 5, 9 and 4. This gives us that c must be a multiple of 180. So, for the next steps I will express this with c = 180x.
But that’s not the end of it. The next step was the hardest for me. It’s the step to get the equation for d to be true. By using the multiplicative inverse modulo of 8 we can get the correct values for c:
c = 180x
3*c/4 = 135x
d mod 8 = 0
(135x - 42) mod 8 = 0
(135x mod 8 - 42 mod 8)) mod 8 = 0
((135 mod 8) * (x mod 8) - 2 mod 8)) mod 8 = 0
((7 mod 8) * (x mod 8) - 2 mod 8)) mod 8 = 0
((7 mod 8) * (x mod 8)) mod 8 = 2 mod 8
x mod 8 = 14 mod 8
x mod 8 = 6
This gives us the values of x and therefore the seven values for c = 180x. With the equations above the input strings for the admin access are:
c | Serial
--------------------------
1080 | 1038-0270-1080-0768
2520 | 2478-0630-2520-1848
3960 | 3918-0990-3960-2928
5400 | 5358-1350-5400-4008
6840 | 6798-1710-6840-5088
8280 | 8238-2070-8280-6168
9720 | 9678-2430-9720-7248
BitK’s Editor note
BitK is the Technical Ambassador at Yes We Hack. He also created the DOJO and this challenge.
While Z3 was not required to solve this challenge, it is a nice simple exercice to get started with the library. Z3 or other SMT solver can be really useful when dealing with a large number of constraints.
