Keygenning dengan Z3 SMT Solver

Keygen atau key generator merupakan program yang generate kode serial yang valid untuk register software menjadi versi full atau sekedar dapat menggunakan software tersebut. Keygenning adalah proses pembuatan program keygen. Berbeda dengan teknik patching, teknik keygenning merupakan teknik cracking software yang lumayan sulit karena reverser harus mengerti luar dalam dari algoritme pengecekan kode serial. Reverser bisa saja berurusan dengan bermacam-macam algoritme kriptografi yang digunakan untuk pengecekan serial seperti MD5, AES, RSA, dan lain sebagainya. Untuk artikel ini akan saya bahas teknik keygenning pada program sederhana.


SMT

SMT (satisfiability modulo theories) adalah sebuah problem keputusan untuk menunjukan apakah suatu formula matematik memiliki suatu solusi. Misal,

if x % 2 == 0:
    satisfied()
else:
    unsatisfied()

tentunya program akan "satisfied" jika nilai x adalah sebuah bilangan genap. Contoh tadi merupakan kode sederhana dengan 1 batasan (constraint) yaitu jika variable bilangan di mod 2 maka hasilnya haruslah 0 untuk mendapatkan status satisfied. Bayangkan jika terdapat banyak variable dan constraint, apakah kita mau bruteforce? tentu saja bisa namun hasilnya lumayan lama.


z3

z3[1] adalah algoritme yang dikembangkan oleh microsoft untuk menyelesaikan permasalahan satisfiability. z3 mulai diperkenalkan ke khalayak umum tahun 2008 melalui paper Leonardo de Moura[2]. Dalam kasus cracking program tugas kita hanya mendefinisikan constraint-constraintnya saja dan biarkan z3 mencari solusi yang satisfied.


Lab

Jika belum ada z3 di python, install z3 dulu

$ sudo pip install z3-solver

sample1.c

// $ gcc sample1.c -o sample1 
#include<stdio.h>
int main(){
    int x;
    printf("KEY: ");
    scanf("%d", &x);
    // SAT jika nilai x adalah genap dan nilai x dikali 3 lebih besar dari 27
    if(x % 2 == 0 && x * 3 > 28){
        puts("SAT"); // satisfied
    }
    else {
        puts("UNSAT");
    }
    return 0;
}

pertama buat instance solvernya dahulu

from z3 import *

def main():
    s = Solver()
    x = BitVec("x", 32) 

if __name__ == "__main__":
    main()

nilai 32 adalah besar integer dalam vektor biner. Selanjutnya definisikan constraint dan print solusinya.

from z3 import *

def main():
    s = Solver()
    x = BitVec("x", 32) 
    s.add(x % 20 == 0)
    s.add(x * 3 > 28)
    if str(s.check()) == "sat":
        print(s.model())
    
if __name__ == "__main__":
    main()

Jika dijalankan maka akan menghasilkan nilai yang memenuhi constraint yang kita definisikan.

$ python solver.py
[x = 20971520]
$ ./sample1 
KEY: 20971520
SAT

Lalu bagaimana kalau kita mau mendapat solusi yang berbeda dari sebelumnya?, kita dapat membuat constraint baru agar nilai solusi lama tidak dijadikan solusi.

from z3 import *

def main():
    s = Solver()
    for i in range(10):
        x = BitVec("x", 32)
        s.add(x % 20 == 0)
        s.add(x * 3 > 28)
        if str(s.check()) == "sat":
            print("solusi %d: %s" % (i+1, s.model()[x]))
            s.add(x != s.model()[x])

if __name__ == "__main__":
    main()
    

Jika dijalankan kita akan mendapat 10 solusi

$ python solver.py
solusi 1: 20971520
solusi 2: 1789569680
solusi 3: 1789559440
solusi 4: 1779073680
solusi 5: 1745486480
solusi 6: 1795293840
solusi 7: 1744994960
solusi 8: 1778418320
solusi 9: 2030076560
solusi 10: 2046952080

sample2.c

// $ gcc sample2.c -o sample2
#include<stdio.h>
#include<stdlib.h>
#include<string.h>

void invalid(){
  puts("Invalid Serial Number!");
  exit(0);
}

int main(){
  char serial[47];
  int i;
  printf("Serial number: ");
  fgets(serial, 48, stdin);
  // panjang serial sama dengan 47
  if(strlen(serial) != 47){
    invalid();
  }
  // cek karakter strip pada kelipatan 5
  for(i = 5; i < 47; i += 6){
    if(serial[i] != '-'){
      invalid();
    }
  }
  // cek serial hanya huruf besar dan angka
  for(i = 0; i < 47; i++){
    if(!((serial[i] >= 48 && serial[i] <= 57) || (serial[i] >= 65 && serial[i] <= 90)) && i != 5 && i != 11 && i != 17 && i != 23 && i != 29 && i != 35 && i != 41){
      invalid();
    }
  }
  i = 0;
  while(i < 47){
  // penjumlahan serial pada tiap potongan adalah genap
    if((serial[i] + serial[i+1] + serial[i+2] + serial[i+3] + serial[i+4]) % 2 != 0){
      invalid();
    }
    // nilai pada tiap potongan serial tidak boleh sama
    if(serial[i] == serial[i+1] || serial[i+1] == serial[i+2] || serial[i+2] == serial[i+3] || serial[i+3] == serial[i+4] || serial[i+4] == serial[i]){
      invalid();
    }
    i += 6;
  }
  puts("Serial number valid.");
  return 0;
}


  1. Buat instance solver dan variable constraint
from z3 import *

def main():
    s = Solver()
    serials = [BitVec("s_%d" % i, 8) for i in range(47)]
     
if __name__ == "__main__":
    main()

  1. Definisikan constraint
from z3 import *

def main():
    strips = [5, 11, 17, 23, 29, 35, 41]
    s = Solver()
    serials = [BitVec("s_%d" % i, 8) for i in range(47)]
    for i in range(47):
        if i in strips:
            s.add(serials[i] == ord('-'))
        else:
            s.add(Or(And(serials[i] >= 48, serials[i] <= 57), And(serials[i] >= 65, serials[i] <= 90)))
    i = 0
    while i < 47:
        s.add((serials[i] + serials[i+1] + serials[i+2] + serials[i+3] + serials[i+4]) % 2 == 0)
        s.add(And(serials[i] != serials[i+1], serials[i+1] != serials[i+2], serials[i+2] != serials[i+3], serials[i+3] != serials[i+4], serials[i+4] != serials[i]))
        i += 6

    s.check()
    model = s.model()
    print "".join([chr(int(str(model[serials[i]]))) for i in range(47)])


if __name__ == "__main__":
    main()

  1. Buat solusi yang unik (tidak duplikat)
from z3 import *

def rem_dup(s, m, serials):
    constraint = "s.add(Or("
    for i in range(47):
        serial_str = "serials[%d] !=  m[serials[%d]]" % (i, i)
        constraint += serial_str
        if i != 46:
            constraint += ", "
        else:
            constraint += "))"
    eval(constraint)

def main():
    strips = [5, 11, 17, 23, 29, 35, 41]
    s = Solver()
    for i in range(5):
        serials = [BitVec("s_%d" % i, 8) for i in range(47)]
        for i in range(47):
            if i in strips:
                s.add(serials[i] == ord('-'))
            else:
                s.add(Or(And(serials[i] >= 48, serials[i] <= 57), And(serials[i] >= 65, serials[i] <= 90)))
        i = 0
        while i < 47:
            s.add((serials[i] + serials[i+1] + serials[i+2] + serials[i+3] + serials[i+4]) % 2 == 0)
            s.add(And(serials[i] != serials[i+1], serials[i+1] != serials[i+2], serials[i+2] != serials[i+3], serials[i+3] != serials[i+4], serials[i+4] != serials[i]))
            i += 6

        s.check()
        model = s.model()
        print "".join([chr(int(str(model[serials[i]]))) for i in range(47)])
        rem_dup(s, model, serials)



if __name__ == "__main__":
    main()

Jika dijalankan kita akan mendapatkan serial number yang unik

$ python solver2.py
JP08Z-TPXYU-EDLHA-HLDLD-A3SPQ-KJ3AO-C0CK3-OJZLK
NOKOK-NOKOK-NOKOK-NOKOK-NOKOK-NOKOK-NOKOK-NKOKO
8YCKA-1JG3S-ODPLS-DOM91-Y0PXO-RKZLK-RSNLO-LN279
8YCKA-1JG3S-ODPLS-DOM91-Y0PXO-RKZLK-ZSFLO-LN279
8YCKA-1JG3S-OEPLR-DOM91-Y0PXO-RKZLK-ZSFLO-LN279
$ ./sample2
Serial number: JP08Z-TPXYU-EDLHA-HLDLD-A3SPQ-KJ3AO-C0CK3-OJZLK
Serial number valid.

Sekian.


  1. https://github.com/Z3Prover/z3. ↩︎

  2. https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24 ↩︎

Herdian N

Read more posts by this author.