Tokenizer (Rev 100):

By Victor Contreras aka @_Evil_Machine

Descripcion:

Nuestro contacto interno obtuvo esta herramienta que sirve para verificar  
tokens validos, mismos que creemos siguen siendo utilizados como segundo factor
de autenticacion para la Banca en linea. 

Al ya haber conseguido las credenciales del usuario jperez (via Loki challenge) 
analiza la aplicacion, encuentra la forma de generar tokens validos e ingresa a
su cuenta bancaria en:

http://52.14.x.x:8005/login.php

La flag te esperara en la pantalla de bienvenida.

Aqui el codigo fuente del generador de tokens:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
import java.util.Scanner;

/*
 * Fecha: 04 Abril 2006
 * Descripcion: Validador de Tokens para acceso a Banca Movil
 * Version: 1.1 Android OS
 * Autor: Victor Contreras, Architecto Jr, Hack Defender
 * Organizacion: Capture Bank S.A de C.V
 *
*/

public class ValidadorToken {

    public static String token;

    static {
        Scanner sc = new Scanner(System.in);
        System.out.print("Ingresa tu token: ");
        token = sc.nextLine();
        if(token.length() != 16){
            System.out.println("Token INVALIDO");
            System.exit(0x0);
        }
        if(!token.matches("^[a-z]+$")){
            System.out.println("Token INVALIDO");
            System.exit(0x0);
        }

        for(int i = 0; i < token.length(); i++){
            if((int)token.charAt(i) % 0x2 != 0){
                System.out.println("Token INVALIDO");
                System.exit(0x0);
            }
        }

    }

    public static void main(String[] args) {
        int sumatoria = 0;
        for(int i = 0; i < token.length(); i++){
            sumatoria += (token.charAt(i) >> 1) + 22;
        }
        int c = '蜄';
        int b = 1;
        int a = 18279;
        int result =a^c>>b;
        if(sumatoria == result){
            System.out.println("Token valido: "+token);
        }else {
            System.out.println("Token INVALIDO");
            System.exit(0);
        }

    }
}


La logica del generador es muy sencilla, solo tiene las siguientes restricciones:
  1. Linea 20: Size de 16 caracteres
  2. Linea 24: Solo letras minusculas
  3. Linea 30: Divisible entre 2
  4. Linea 41: A cada caracter se le aplica un shift right y se le suma 22
  5. Linea 46: Y el resultado debe ser igual a: a^c>>b
Pusimos en Linea 43 un caracter chino para destantear pero era facilmente descubierto si lo imprimias.
Con esta informacion se creo un script en z3 para resolverlo:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
#!/usr/bin/python3
from z3 import *

for i in range(16):
 globals()['token%i' % i]=BitVec('token%i' %i,32)

s = Solver()

for i in range(16):
    s.add(globals()['token%i' %i] >= ord('a'), globals()['token%i' %i] <= ord('z'))
    s.add(globals()['token%i' %i] % 2 == 0)

# Valores de la operacion final
c = 34564
b = 1
a = 18279
s.add(((token0>> 1) + 22)+((token1>> 1) + 22)+((token2>> 1) + 22)
     +((token3>> 1) + 22)+((token4>> 1) + 22)+((token5>> 1) + 22)
     +((token6>> 1) + 22)+((token7>> 1) + 22)+((token8>> 1) + 22)
     +((token9>> 1) + 22)+((token10 >> 1) + 22)+((token11 >> 1) + 22)
     +((token12 >> 1) + 22)+((token13 >> 1) + 22)+((token14 >> 1) + 22)
     +((token15 >> 1) + 22) == a^c>>b)

if s.check() == sat:
    values =s.model()
    valor = ''
    for i in range(16):
        obj = globals()['token%i' %i]
        char = values[obj].as_long()
        valor += chr(char)
    print(valor)
else:
    print('nooo')

Y obtenemos uno de muchos  tokens posibles:


En la pantalla siguiente se ingresa otro token valido:

Se te presenta la pantalla de home del usuario victima:

Y en el codigo fuente te esperaba la bandera!

Comments

Post a Comment