DOJO CHALLENGE #4 Winners!
February 12, 2020
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.
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).
We are glad to announce the #4 DOJO Challenge winners list.
3 FIRST SOLVES (in order)
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!
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?
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.
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.
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.
- Requirements: Follow the instructions here:
- install Z3.
- Run the provided solution script using python: python sol.py
Solution script: sol.py
from z3 import * # Creating integers first = Int('first') second = Int('second') third = Int('third') fourth = Int('fourth') # solver s = Solver() # adding constraints # as the number in each part is a 4-digit number, so it must be less than 9999 s.add(0< first, first < 9999) s.add(0 < second, second < 9999) s.add(0 < third, third < 9999) s.add(0 < fourth, fourth < 9999) # Added the conditions that I solved. As shown in image y3.png 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 ) # valid serials list serials =  # find all the valid serials while s.check() == sat: m = s.model() # append a valid serial in the serials list a1, a2, a3, a4 = str(m[first]), str(m[second]), str(m[third]), str(m[fourth]) # If we find a number '23' which satisfies the above mentioned constraints then we prepend '00' to '23' to fulfill the required format of a serial 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) # as we want 7 unique serial, so we ask the solver to do not provide us the serial which we had already found 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)
The problem here is, that only some obfuscated code is used to hide the evaluation of the serial.
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 // multiple inverse element modulo 8 of 7 = 7 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.