Chris won't stop making Java RE challenges... but he might if you find the correct key to this challenge! Flag is in the form of flag{answer_here}

author : ItzSomebody

file : JavaIsEZ2.class

 


Java decompilers didn't decompile it perfectly.

I decompiled it with CFR but it was difficult to understand.

So, I wrote decompiled code on my own.

public class JavaIsEZ2 {

	public static void main(String[] args) {
		// TODO Auto-generated method stub
		String obj[] = { "redpwn", "ctf2020" };
		String flag = "4f162351e2a0bb6e1fc34325972c1de8";
		long arr[] = { 0x727756a076dbe2b2L, 0xb5db07b30685ff09L, 0xffffffffcafebabeL, 0xffffffffdeadbeefL };
		long res1, res2, tmp, l1;
		int i = 0, chk = 0;
		
		for(int k = 0; k < 2; k++) {
			tmp = Long.parseLong(k == 0 ? flag.substring(0, 16) : flag.substring(16), 16);
			for(int j = 0; j < obj[k].length(); j++)
				i = 31 * i + obj[k].charAt(j);
			l1 = (long) i;
			res1 = (l1 | l1 << 32) ^ arr[k];
			res2 = tmp * arr[k+2];
			if(res1 == res2) {
				chk++;
			}
			i = 0;
		}

		flag = "flag{" + flag + "}";
		for(int j = 0; j < flag.length(); j++)
			i = 31 * i + flag.charAt(j);
		if(i == 0x43f82813)
			chk++;
		
		if(chk == 3)
			System.out.println("Oh nice, you found my key :O");
		else
			System.out.println("That is pepega");
	}
}

 

We can get flag with z3.

from z3 import *
a = [BitVec('a%i' % i, 64) for i in range(0,2)]

s = Solver()

s.add(a[0] * 0xffffffffcafebabe == 0x8d88a95fbe9d07a4)
s.add(a[1] * 0xffffffffdeadbeef == 0xf574e322462a1b98)

check = s.check()
print check
if check == sat:
        m = s.model()
        flag = ""
        for i in range(2):
                flag += "%016x" % m[a[i]].as_long()
        print flag

 

flag : flag{4f162351e2a0bb6e1fc34325972c1de8}