Step 3 - La crypto de consistance

Étape 3 - The Authenticator in SHAdow

Description

Remarkable work, agent. You have successfully hacked into the machine of the organisation's lead developer, DEV. Thanks to you, we have secured a foothold inside the target's internal network!

With this newfound access, we discovered that the organisation is running a customized internal chat application, MafiaChat.

Moreover, it seems that a suspicious individual named EMERALD and acting as the organisation's BOSS is trying to establish contact with DEV through MafiaChat. Our social engineering team certainly could make good use of this opportunity if you find a way to respond to him as DEV (@mafiaDEV).

Our team conducted a first analysis of the application. It looks like the development is still in its early phase and the confidentiality of the messages is not assured, therefore we can freely read messages from the server. Conversely, the messages' integrity is strongly enforced, and all the messages require signing through a specialized Hardware Security Module, running on a 3rd party machine. However, the conversation between DEV and another member of the organisation, Mafia-Bro, suggests that the Module contains a backdoor that you could exploit using your cryptography skills!

Thanksfully, the lead developer was in charge of this very project, and since we hacked their computer we got access to the source and binaries involved (albeit stripped from production secrets):

* MafiaChat, a python server;
* Shardy, a python client;
* HSMM, a RISCV-64 C program used for message signing, which runs on a specialized Hardware Security Module.

According to some of DEV's notes, the backdoored hardware for running the HSMM binary can be emulated perfectly with QEMU and the provided backdoor.diff patch, how convenient! All assets, combined with appropriate Dockerfiles and some of the developer notes are available here.

Your goal is to send a first message (whatever it is) to EMERALD (@mafiaBOSS) as DEV (@mafiaDEV).

Résolution

Pour cette étape, il est demandé d’envoyer un message à EMERALD depuis DEV via le protocole de communication offert par MafiaChat. Pour qu’un message soit accepté lors de son émission, une signature valide doit être associée. Cette signature est vérifiée par le module HSM fourni.

On nous donne l’intégralité des sources du serveur et du client (Shardy) Mafia Chat, ainsi que du HSM, une grande partie ici.

Vu la description fournie, on suppose qu’il va falloir forger une signature qui devra être acceptée par le HSM et authentifiera le compte MafiaDev dont on n’est pas supposé connaître les éléments d’authentification associés.

Setup

Afin de faciliter le debug du HSM, il est préférable de modifier légèrement le contenu du script fourni pour ajouter un gdbserver à l’ensemble et pouvoir débogguer pas à pas. Ainsi, la directive docker CMD initiale :

CMD socat TCP-LISTEN:5000,reuseaddr,fork \
    EXEC:"/sstic/qemu-riscv64 \
    -cpu 'rv64,zkr=true,v=true,vext_spec=v1.0,zvbb=true,zvknha=true' \
    -L /sstic/install/riscv/sysroot \
    -E LD_LIBRARY_PATH='/sstic/install/openssl/lib' \
    -E OPENSSL_riscvcap='rv64imafdcvh_zicbom_zicboz_zicntr_zicsr_zifencei_zihintntl_zihintpause_zihpm_zawrs_zfa_zca_zcd_zba_zbb_zbc_zbs_zkr_v_zvbb_zve32f_zve64f_zve64d_zvknha_sstc_svadu' \
    /sstic/hsmm",stderr

peut être remplacée par l’ensemble suivant :

# fichier gdbscript.sh
#!/bin/sh

gdbserver localhost:5544 /sstic/qemu-riscv64 \
    -cpu 'rv64,zkr=true,v=true,vext_spec=v1.0,zvbb=true,zvknha=true' \
    -L /sstic/install/riscv/sysroot \
    -E LD_LIBRARY_PATH='/sstic/install/openssl/lib' \
    -E OPENSSL_riscvcap='rv64imafdcvh_zicbom_zicboz_zicntr_zicsr_zifencei_zihintntl_zihintpause_zihpm_zawrs_zfa_zca_zcd_zba_zbb_zbc_zbs_zkr_v_zvbb_zve32f_zve64f_zve64d_zvknha_sstc_svadu' \
    /sstic/hsmm

et le contenu du Dockerfile associé :

FROM ubuntu:jammy-20240227 AS challenge

RUN apt-get update -qq \
 && apt-get install -qq \
    libglib2.0-dev \
    socat gdbserver \
 && rm -rf /var/lib/apt/lists/*

[...]
COPY gdbscript.sh /sstic/

CMD socat TCP-LISTEN:5000,reuseaddr,fork \
    EXEC:"bash /sstic/gdbscript.sh",stderr

Pour la suite, c’est principalement le HSM qui va nous intéresser, donc il suffit de build les 2 images Docker (la première d’origine et la seconde en mode debug) :

cd hsmm
docker build . -t hsmm
docker run -it -p 5000:5000 --privileged hsmm
cd hsmm-debug
docker build . -t hsmm-debug
docker run -it -p 5001:5000 --privileged hsmm-debug

On peut vérifier le bon fonctionnement du HSM en utilisant le compte de test fourni dans les fichiers mafiachat/server.py, hsmm/src/src/auth.c ou shardy/client.py :

nc 127.0.0.1 5000
0
@mafiaTEST
OnlyRequiredToSignAndSendMessages
@mafiawhatever
contentwtf
1337
1337

Retourne

ZnJvbTpAbWFmaWFURVNUXHRvOkBtYWZpYXdoYXRldmVyXGNvbnRlbnQ6Y29udGVudHd0Zg==
bOmIMr0+EOyulwlrZhzBeBFWHzX7+bVoikKGIhu3bo4=

Pour faciliter l’exploitation, un service SSH est fourni et peut être lancé en même temps que l’instance au niveau de la page de l’épreuve

Exploration

Les fonctions sign et verify sont définies dans le fichier hsmm.py qui est utilisé à la fois dans le client Shardy et par le serveur du Chat, et fournissent un point d’entrée pour mieux comprendre les interactions implémentées :

def sign(
    user: str,
    pwd: str,
    recipient: str,
    content: bytes,
    extra_0: int,
    extra_1: int,
) -> tuple[str, str]:
    conn = HSMMConnection()
    try:
        conn.sendline("0")
        conn.sendline(user)
        conn.sendline(pwd)
        conn.sendline(recipient)
        conn.sendline(content)
        conn.sendline(f"{extra_0}")
        conn.sendline(f"{extra_1}")
        recvs = conn.recvlines()
        if len(recvs) != 2:
            if len(recvs) == 1:
                raise HSMMException(recvs[0])
            raise HSMMException()
        data_b64 = recvs[0]
        sig_b64 = recvs[1]
        return (data_b64, sig_b64)
    finally:
        conn.close()


def verify(
    data: bytes,
    sig_b64: str,
) -> bool:
    conn = HSMMConnection()
    try:
        conn.sendline("1")
        conn.sendline(sig_b64)
        conn.sendline(data)
        recvs = conn.recvlines()
        if len(recvs) != 1:
            HSMMException()
        recv = recvs[0]
        if recv == "0":
            return False
        elif recv == "1":
            return True
        raise HSMMException(recv)
    finally:
        conn.close()

Ainsi, on ne peut réaliser que deux opérations :

Lorsqu’on utilise le HSM, on constate que le message signé rassemble toutes les données fournies (hors mot de passe de l’émetteur), ci-dessous le résultat de ce qui est indiqué dans le paragraphe de setup précédent :

#ZnJvbTpAbWFmaWFURVNUXHRvOkBtYWZpYXdoYXRldmVyXGNvbnRlbnQ6Y29udGVudHd0Zg==
#bOmIMr0+EOyulwlrZhzBeBFWHzX7+bVoikKGIhu3bo4=

echo ZnJvbTpAbWFmaWFURVNUXHRvOkBtYWZpYXdoYXRldmVyXGNvbnRlbnQ6Y29udGVudHd0Zg==|base64 -d
from:@mafiaTEST\to:@mafiawhatever\content:contentwtf

echo bOmIMr0+EOyulwlrZhzBeBFWHzX7+bVoikKGIhu3bo4=|base64 -d|hexdump -C
00000000  6c e9 88 32 bd 3e 10 ec  ae 97 09 6b 66 1c c1 78  |l..2.>.....kf..x|
00000010  11 56 1f 35 fb f9 b5 68  8a 42 86 22 1b b7 6e 8e  |.V.5...h.B."..n.|
00000020

Le format du message peut être retrouvé dans le fichier hsmm/src/src/message.c :

snprintf(*message, message_sz + 1, "from:%s\\to:%s\\content:%s", username,
           recipient, content);

Réussir le challenge s’apparente donc à être en mesure de créer un message avec une signature valide dont l’émetteur sera interprété comme MafiaDev, et le destinataire EMERALD. Vu les informations communiquées, il est assez naturel de commencer par chercher une faille cryptographique dans le HSM. Un autre argument en faveur de cette piste est que le code du HSM affiche les mots de passe des utilisateurs non privilégiés mafiaTEST et mafiaTECHNICIAN : on peut donc utiliser ces derniers pour forger des signatures valides dans leur contexte utilisateur.

Analyse du patch

Le code source du HSM s’accompagne également de fichiers .diff qui sont des patchs de code source ciblant la version de QEMU utilisée pour lancer le HSM :

Les nouveaux registres déclarés sont utilisés uniquement à trois endroits :

// initialisation des registres lors de l'utilisation du HSM
int main() {
  csrw_mafia_0(1337);
  csrw_mafia_1(1337);
  csrw_mafia_1_now(0);
  //...
}
// utilisation des paramètres utilisateur dans la fonction main_sign
unsigned long extra_0 = hsm_getline_nb();
csrw_mafia_0(extra_0);

unsigned long extra_1 = hsm_getline_nb();
csrw_mafia_1(extra_1);
// utilisation des registres csrr pour générer une clé dans la fonction sign
void sign(char *out, unsigned char *message, size_t message_sz) {
  unsigned char key[SIG_SZ];
  for (int i = 0; i < SIG_SZ / 4; ++i) {
    unsigned long key32 = csrr[i]();
    key[4 * i + 0] = key32 & 0xFF;
    key[4 * i + 1] = key32 >> 8 & 0xFF;
    key[4 * i + 2] = key32 >> 16 & 0xFF;
    key[4 * i + 3] = key32 >> 24 & 0xFF;
  }
  //...
}

Cette dernière clé est utilisée comme argument de la fonction EVP_MAC_init, et dépend bien des 8 registres CSR_MKEYX.

Quant à l’utilisation au sein de la backdoor en elle-même, il n’existe qu’un seul endroit où les registres mafia_0 et mafia_1 sont utilisés comme variables pour définir le comportement d’une fonction, il s’agit de la fonction vsha2c_mafia32 :

static void vsha2c_mafia32(CPURISCVState *env, uint32_t *M)
{
    target_ulong mafia_0_now = env->mafia_0_now;
    env->mafia_0_now += 2;
    if (env->mafia_0 != mafia_0_now) {
        return;
    }

    target_ulong mafia_1_now = env->mafia_1_now;
    env->mafia_1_now += 1;
    if (env->mafia_1 != mafia_1_now) {
        return;
    }

    target_ulong m0 = helper_csrrw(env, 0x015, 0, 0);
    target_ulong m1 = helper_csrrw(env, 0x015, 0, 0);
    if ((m0 & 0b11 << 30) != 0b10 << 30 || (m1 & 0b11 << 30) != 0b10 << 30) {
        riscv_raise_exception(env, RISCV_EXCP_ILLEGAL_INST, GETPC());
    }
    *M = (m0 & 0xFFFF) | (m1 & 0xFFFF) << 0x10;
}

Cette fonction se comporte de la manière suivante : les compteurs qui sont initialisés à 0 mafia_0_now et mafia_1_now sont incrémentés (le premier de 2 et le second de 1), et soit les deux compteurs valent simultanément les valeurs cibles mafia_0 et mafia_1, auquel cas la fonction attribue une valeur non connue à l’emplacement du pointeur M passé en argument, soit ça n’est pas le cas et il ne se passe rien.

La vraie backdoor est implémentée dans 2 fonctions helpers risc-v que sont vsha2ch32_vv et vsha2ch32_vv, de la même manière : la fonction vsha2c_mafia32 ci-dessus est appelée à chaque tour de boucle avant d’appeler la fonction vsha2c_32 avec un argument en plus : la valeur de M, qui vaut soit 0, soit une valeur inconnue lorsque les compteurs coïncident. Cette valeur est utilisée pour modifier d’une des valeurs

Finalement, le compteur mafia_0_now est réinitialisé à 0 dans la fonction vsetvl.

Question du lecteur attentif : mais que font donc ces fonctions vsha2ch32_vv, vsha2ch32_vv et vsha2c_32 ?

Les fonctions vsha2ch32_vv, vsha2ch32_vv et vsha2c_32 sont définies dans le code source de Qemu au niveau du fichier vcrypto_helper.c.

De prime abord, on n’a pas trop envie d’aller mettre ses mains là-dedans :

Retournons maintenant un instant sur le fonctionnement du HSM dans son ensemble.

Fonctionnement du HSM

L’analyse de la faible surface exposée par le HSM montre rapidement que la signature calculée est un HMAC-SHA256 avec la clé stockée dans le HSM, et qu’elle est calculée sur le message fourni en entrée :

  EVP_MAC *mac = EVP_MAC_fetch(NULL, "HMAC", NULL);
  //[...]
  OSSL_PARAM_construct_utf8_string("digest", "SHA256", 0);
  //[...]
  EVP_MAC_init(mac_ctx, key, SIG_SZ, params)
  //[...]
  EVP_MAC_update(mac_ctx, message, message_sz)
  //[...]
  EVP_MAC_final(mac_ctx, signature, NULL, SIG_SZ)

La vérification consiste simplement en calculer le HMAC-SHA256 du message à vérifier, et comparer le résultat avec la signature fournie. Les constructions de type HMAC prévenant notamment des attaques de type Hash-Length extension, il est assez peu probable de parvenir à des scénarios de collision de signature sans connaître la clé (du moins en l’absence de collision sur SHA-256).

Pour rappel, la fonction HMAC-[alg] est définie de la manière suivante :

Définition de HMAC
HMAC[H](text) = H(K XOR opad, H(K XOR ipad, text))

La fonction réalise ainsi au minimum 4 compressions avec :

Les compressions d'un HMAC (SHA-1)

Un détail dans la vérification qui nous indique dans quelle piste s’engager par la suite est la présence d’un commentaire qui indique l’absence de contrôle des caractères fournis, ce qui contraste avec le strict contrôle de l’ensemble des données lors de la signature par exemple :

// No need to call hsm_getline_check since we only check signature,
// also message should contain caracters like ':' and '\'

Ce commentaire laisse entendre qu’on va pouvoir forger une signature valide en ajoutant des données à notre message, et que ces données seront des chars qui prendront l’ensemble des valeurs possibles entre 0 et 255.

Il est temps de s’attaquer à l’effet des paramètres extra_0 et extra_1, qui n’ont pas été utilisés pour le moment.

Un peu de debug avant de foncer

A ce stade, on a vu que la signature était du HMAC-SHA256, et des helpers Risc-V ont été backdoorés dans Qemu pour des opérations liées à sha256. Mais ces derniers sont-ils utilisés lors du calcul du HMAC avec les fonctions d’OpenSSL (utilisées par le HSM) ? La réponse est oui : en cherchant dans le code source d’OpenSSL l’implémentation sha256 sur Risc-V, on tombe sur le code suivant (attention, bonnes lunettes de soleil conseillées) : sha256-riscv64-zvkb-zvknha_or_zvknhb.pl

Point culture :

# Zvknhb - Vector Crypto SHA-256 and SHA-512 Secure Hash
#
# The following 3 instructions are defined in both Zvknha and Zvknhb:
#  - in Zvknha, they support SHA-256 (SEW=32) only,
#  - in Zvknhb, they support both SHA-256 (SEW=32) and SHA-512 (SEW=64).

$import rv_zvknha::vsha2ms.vv
$import rv_zvknha::vsha2ch.vv
$import rv_zvknha::vsha2cl.vv

En plus de noms à dormir debout, le code fourni pour calculer un sha256 est particulièrement dur à suivre car sensiblement optimisé.

Ici est fournie une simplification des opérations réalisées pour le calcul d’un sha256 :

################################################################################
# void sha256_block_data_order_zvkb_zvknha_or_zvknhb(void *c, const void *p, size_t len)

    [Load constants]
    [Init the first 16x int32 from user]  # Generate W[15:0]
  
    [Perform the following round 12x]
    # Quad-round 0 (+0, Wt from oldest to newest in v1->v2->v3->v4)
    @{[vadd_vv $V5, $V10, $V1]}
    @{[vsha2cl_vv $V7, $V6, $V5]}
    @{[vsha2ch_vv $V6, $V7, $V5]}
    @{[vmerge_vvm $V5, $V3, $V2, $V0]}
    @{[vsha2ms_vv $V1, $V5, $V4]}  # Generate W[19:16] ... then repeat 5 instrs for W[23:20] ... until W[63:60]

    [Perform the following round 4x (same but no W generation)]
    # Quad-round 12 (+0, v1->v2->v3->v4)
    # Note that we stop generating new message schedule words (Wt, v1-13)
    # as we already generated all the words we end up consuming (i.e., W[63:60]).
    @{[vadd_vv $V5, $V22, $V1]}
    @{[vsha2cl_vv $V7, $V6, $V5]}
    @{[vsha2ch_vv $V6, $V7, $V5]}

    [Few optimizations and ret $V6 $V7]

On constate la génération progressive d’un tableau de 64 int32 “W[i]”, ainsi que la présence d’un état constitué par $V6 et $V7, et qui constitue les 32 octets du SHA-256 à la fin du calcul global.

NOTE: L’ensemble des 32 registres de l’extension vectorielle (V) en Risc-V comprennent 128 bits et permettent de manipuler simultanément 16 octets.

Un peu de documentation s’impose donc pour mieux comprendre comment un SHA-256 se calcule et comment l’implémentation d’OpenSSL couplée aux helpers Qemu s’articule.

L’article Wikipedia sur la famille SHA-2 se suffit à lui-même sur la question du calcul global :

Le schéma principal extrait de Wikipedia récapitule les opérations qui sont réalisées lors du calcul d’un tour :

1 round SHA-2

Il est important d’observer que seules les valeurs a et e sont des valeurs qui ne proviennent pas directement d’un shift du vecteur. Ainsi, si on applique deux tours successifs, on constate que seules les valeurs a, b, e et f sont des calculs non triviaux de l’état initial.

C’est ce principe qui est exploité pour l’optimisation qui est effectuée dans le code perl plus haut, puisqu’on peut stocker uniquement 4 valeurs de retour dans le vecteur de destination, et faire “glisser” a, b, e et f initiaux aux emplacements c, d, g et h deux tours plus loin :

2 rounds = optimisation

Bref, ça n’est pas très grave si vous n’avez pas suivi jusqu’ici, le seul élément important à retenir, c’est que 4 tours de SHA-256 sont bien calculés par l’application successive de vsha2cl_vv et vsha2ch_vv, et que V6 et V7 représentent [a,b,e,f] [c,d,g,h] tous les 4 tours. On vérifie d’ailleurs bien le nombre de rounds total : 16 applications de vsha2cl_vv et autant de vsha2ch_vv : 32 appels de ces fonctions, donc 32 appels de la fonction vsha2c_32 qui calcule 2 tours de SHA-256 : 64 tours au total.

Pfiou … La fonction vsha2c_32 (non backdoorée) en question, un peu plus claire maintenant :

static void vsha2c_32(uint32_t *vs2, uint32_t *vd, uint32_t *vs1)
{
    uint32_t a = vs2[H4(3)], b = vs2[H4(2)], e = vs2[H4(1)], f = vs2[H4(0)];
    uint32_t c = vd[H4(3)], d = vd[H4(2)], g = vd[H4(1)], h = vd[H4(0)];
    uint32_t W0 = vs1[H4(0)], W1 = vs1[H4(1)];
    uint32_t T1 = h + sum1_32(e) + ch(e, f, g) + W0;
    uint32_t T2 = sum0_32(a) + maj(a, b, c);

    h = g;
    g = f;
    f = e;
    e = d + T1;
    d = c;
    c = b;
    b = a;
    a = T1 + T2;

    T1 = h + sum1_32(e) + ch(e, f, g) + W1;
    T2 = sum0_32(a) + maj(a, b, c);
    h = g;
    g = f;
    f = e;
    e = d + T1;
    d = c;
    c = b;
    b = a;
    a = T1 + T2;

    vd[H4(0)] = f;
    vd[H4(1)] = e;
    vd[H4(2)] = b;
    vd[H4(3)] = a;
}

NOTE: Pour comprendre ce qui est mentionné plus haut, faire du pas à pas a été bien utile, une fois le breakpoint posé sur la fonction vsha2c_32.

Maintenant, l’effet des variables mafia_0 et mafia_1 : la fonction vsha2c_mafia32 va modifier la variable M uniquement quand les “compteurs mafia” vont valoir exactement mafia_0 et mafia_1 renseignées par l’utilisateur. Or, les compteurs :

Comme la fonction vsha2c_mafia32 est appelée 32 fois par round SHA-256, cela veut dire que mafia_0 doit prendre comme valeur une valeur entre 0 et 62 inclus, multiple de 2, pour que la condition 1 soit réunie. La condition est alors remplie une fois par calcul de compression sha256.

La condition 2 peut être réunie uniquement si mafia_1 prend une valeur entre 0 et le nombre de compressions sha256 qui est réalisé pour calculer le condensat du HMAC.

Pour la suite, on pourra faire l’hypothèse que la valeur M écrite par vsha2c_mafia32 dans le cas où les deux conditions sont réunies est similaire à une valeur aléatoire.

Analysons finalement l’effet de la variable M dans la porte dérobée :

uint32_t c = vd[H4(3)] + M, d = vd[H4(2)], g = vd[H4(1)], h = vd[H4(0)];
Injection de faute SHA-256 - sur C

Conclusion: L’attaque à réaliser pour cette troisième étape est une injection de faute sur un round choisi d’une compression sha256 choisie.

A l’attaque

On tombe rapidement sur le papier Algebraic_Fault_Attack_on_the_SHA-256_Compression_Function qui décrit un algorithme d’attaque par injection de faute sur la fonction de compression de SHA-256, avec un cas d’application pour forger une signature valide sur HMAC-256 (almost universal forgery attack) !

Le seul “soucis” est que des données arbitraires doivent pouvoir être insérées à la suite d’un message signé valide pour que l’attaque fonctionne. Cela n’est pas un problème pour le côté arbitraire comme on l’a vu précédemment avec le commentaire, en revanche on peut s’assurer qu’ajouter des données au message va quand même permettre d’écraser l’émetteur initial du message pour le remplacer par MafiaDev.

Cela se fait rapidement en constatant que le serveur place le contenu lu après le séparateur : dans la variable pointée par ce qui se situe entre le précédent séparateur de contenu \\ et le :, autrement dit on peut écraser les variables précédemment lues y compris l’expéditeur et le destinataire :

# Code source de server.py
msg = {
    "from": None,
    "to": None,
    "content": None,
}
msg_key = None
buf_str = ""
for i in data.decode("utf-8", "ignore"):
    if i == ":":
        msg_key = buf_str
        buf_str = ""
    elif i == "\\":
        if msg_key in msg:
            msg[msg_key] = buf_str
        msg_key = None
        buf_str = ""
    else:
        buf_str += i
if msg_key in msg:
    msg[msg_key] = buf_str

S’en suit alors une lutte pour :

La rigueur est impérative à cette étape. Malheureusement, elle n’a pas été de la partie. En conséquence, des sessions de debug pour vérifier chaque partie des calculs ont été réalisées. L’erreur la plus notable a été la confiance aveugle dans le schéma principal, qui a conduit à ne pas voir que la faute injectée ne se propageait pas comme dans le schéma (qui propage la faute à l’état suivant comme si la faute avait été propagée dans d (impactant donc a3, b3 et e3), alors que l’optimisation réalisée dans vsha2c_32 ne propage la valeur modifiée de c que dans a3 et b3 suivant).

Ainsi, la fonction nextH_double suivante simule exactement le comportement de la fonction helper :

def nextH_double(state, k1, w1, k2, w2, is_fault=None):
    a, b, c, d, e, f, g, h = state
    c = c if is_fault is None else (c + is_fault)

    s1 = rotate_right(e, 6) ^ rotate_right(e, 11) ^ rotate_right(e, 25)
    ch = (e & f) ^ ((~e) & g)
    t1 = (h + s1 + ch + k1 + w1) & 0xffffffff
    s0 = rotate_right(a, 2) ^ rotate_right(a, 13) ^ rotate_right(a, 22)
    maj = ((a & b) ^ (a & c) ^ (b & c)) & 0xffffffff
    t2 = (s0 + maj) & 0xffffffff

    a2, b2, c2, d2, e2, f2, g2, h2 = [(t1 + t2) & 0xffffffff, a, b, c & 0xffffffff, (d + t1) & 0xffffffff, e, f, g]


    s1 = rotate_right(e2, 6) ^ rotate_right(e2, 11) ^ rotate_right(e2, 25)
    ch = (e2 & f2) ^ (~e2 & g2)
    tmp1 = (g + s1 + ch + k2 + w2) & 0xffffffff
    s0 = rotate_right(a2, 2) ^ rotate_right(a2, 13) ^ rotate_right(a2, 22)
    maj = (a2 & a) ^ (a2 & b) ^ (a & b)  # there is the trick
    tmp2 = (tmp1 + s0 + maj) & 0xffffffff
    tmp3 = (d2 + tmp1) & 0xffffffff

    return (tmp2, a2, tmp3, e2)

De même, la fonction compute_one_H suivante calcule l’application du nombre de tours désirés partant d’un état initial connu (constantes) ou inconnu (variables z3 pour la résolution de contraintes).

def compute_one_H(begin, end, fault_location, K, WState, fault, initial_state=None):
    currentHState = InitialHState if not initial_state else initial_state
    all_states = [currentHState]
    for i in range(begin, end):
        w1, w2 = WState[2 * i: 2 * (i + 1)]
        k1, k2 = K[2 * i: 2 * (i + 1)]

        a, b, c, d, e, f, g, h = currentHState
        na, nb, ne, nf = nextH_double(currentHState, k1, w1, k2, w2,
                                      fault if fault_location == i else None)
        currentHState = (na, nb, a, b, ne, nf, e, f)
        all_states.append(currentHState)
    return all_states

Finalement, la fonction solve_corpus constitue le coeur de la logique d’exploitation unitaire. Cette fonction prend toutes les contraintes fixées par l’utilisateur sur les différentes variables, et tente de résoudre le problème à partir de l’état souhaité et des expériences fournies.

Les variables dont on cherche à connaître l’état sont nommées de la manière suivante :

A propos du dernier point, on peut détailler ici l’idée de l’attaque finale par rapport à la façon dont sont appliquées les compressions SHA-256 :

Chaînage des fonctions de compression SHA-256 dans le cadre d’un calcul HMAC

Ainsi, on peut constater que dans le cas minimal sans bloc autre qu’un bloc de message à signer M0 suffisamment petit, il y a 4 fonctions de compression qui sont appliquées pour un HMAC-SHA-256, et on s’attaque à la dernière pour retrouver ce qui est indiqué comme Hin et qui correspond à l’entrée de la dernière fonction de compression ; à ce moment on a donc “contourné” la signature dans le sens où on a connaissance de tout ce qui implique le secret K (à la fois Kout et Hin).

Au départ utilisant z3, je me suis aperçu que ce solveur patinait dans le vide sans trouver la solution pour des problèmes fortement contraints. Changer vers le solveur stp (basé sur cryptoMiniSAT) s’est avéré un choix payant pour la suite. La conversion n’a pas été trop complexe car il est possible d’exporter le problème z3 au format QF_ABV supporté par stp :

# merci stack overflow
from z3 import Ast, Z3_benchmark_to_smtlib_string

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic="QF_ABV"):
    v = (Ast * 0)()
    return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast()) + '\n(get-model)'

Sur la base de nombreuses feuilles de brouillon, d’un mélange d’empirisme, de tests / essais erreurs et de debug en parallèle, ici est donné le squelette de ma solution (avec mafia_0 en premier élément du tuple des steps, le nombre d’expériences à réaliser en second, les variables dont on cherche à déterminer la valeur et qui vont devenir les futures contraintes en élément final ; toujours avec mafia_1 = la dernière compression (donc d’index 3 dans notre cas)) :

steps = [
    (30, 15, [f'addLast{i}' for i in [1, 2, 3, 5, 6, 7]]),
    (28, 14, ['WX59', 'WX60', 'WX61', 'WX62', 'WX63', 'addLast0', 'addLast4']),  # les 3 derniers sont faux mais pg
    (26, 14, ['WX56', 'WX57', 'WX58']),
    (25, 14, ['WX53', 'WX54', 'WX55']),
    (24, 14, ['WX51', 'WX52']),
    (23, 14, ['WX49', 'WX50']),
    (22, 14, ['WX47', 'WX48']),
]

last_steps = [
    (29, 14, ['addLast0', 'addLast4']),
    (0, 14, [f'H{i}' for i in range(8)])
]

# Solve for all `steps` (apply known constraints, and search for asked variables)
# Complete solve for all WX as we have W47 ... W63
# Unset computed values for addLast0 and addLast4
# Solve for all `last_steps`

NOTE: Le début de l’attaque telle que décrite dans le papier indique qu’on peut obtenir tous les addLast avec une injection en round 60. Je n’ai jamais réussi à obtenir des valeurs correctes pour 0 et 4 (trop de solutions possibles) car pas assez de contrainte. J’ai continué sans jusqu’à ce qu’on dispose de suffisamment d’information (tous les W) pour finir.

Pour terminer l’attaque, on peut ajouter un bloc M1 qui va “écraser” les valeurs lues pour l’émetteur du message, et calculer le condensat final de la manière suivante (cela s’apparente très fortement aux opérations à réaliser pour une attaque de type hash-length extension) :

# the current_state = Kout is obtained from the previous attack
# as well as to_hash corresponding to Hin + pad

# confirm the retrieved current_state H[i] will give the initial hash, out[0] is Kout
out = compute_one_H(0, 32, -1, SHA256_K, to_hash, fault=None, initial_state=current_state)
test_case = [(a+b) &0xffffffff for a, b in zip(out[0], out[-1])]
print("[.] Should give the initial legit hash")
print(format_state_to_hash(test_case))

rogue = b'\\from:@mafiaDEV\\to:@mafiaBOSS'  # rogue is padded with 0x80 0x0 0x0 ... 0x0 p16(length in bits)
to_int = bytes_to_state(rogue)
to_hash = [
    *to_int, 8 * (0x80 + len(rogue))  # adding the size of message in bits (includes 2 previous messages keyin and M0 : 0x40 * 2)
]

# compute all W from the initial 16 first ones from rogue
for i in range(16, 64):
    n = nextW(to_hash[-16:])
    to_hash.append(n)
current_start = W[:8]  # the state of next compression (rogue) is also the leak in W of the last compression
out = compute_one_H(0, 32, -1, SHA256_K, to_hash, fault=None, initial_state=current_start)
my_hash = [(a + b) & 0xffffffff for a, b in zip(out[0], out[-1])]
print("[+] We computed the rogue hash:")
print_hex(my_hash)

# construct final hash, last compression function from the values we know Kout
to_hash = [
    *my_hash,
    0x80000000, 0, 0, 0,
    0, 0, 0, 0x00000300
]
for i in range(16, 64):
    n = nextW(to_hash[-16:])
    to_hash.append(n)
current_state = HFirst  # this is Kout

out = compute_one_H(0, 32, -1, SHA256_K, to_hash, fault=None, initial_state=current_state)
final_out = [(a + b) & 0xffffffff for a, b in zip(out[0], out[-1])]
sig = bytes.fromhex(format_state_to_hash(final_out))
initial = b'from:@mafiaTEST\\to:@nothing\\content:QQo='
msg = initial + b'\x80' + b'\x00'*(0x40-3-len(initial)) + struct.pack('>H', 8*(0x40+len(initial)))
msg += rogue
print(f"Will send rogue message of length {len(msg)}: {msg.hex()}")
print(base64.b64encode(msg).decode())
print(base64.b64encode(sig).decode())

La solution complète peut être retrouvée avec le code fourni dans 00-solve_complete.py, il faut auparavant faire un forward de port du port 5000 local au port 5000 du HSM indiqué dans l’énoncé lors du lancement de l’étape, également en option le port 8765 local peut être lié au port 8000 distant du serveur MafiaChat :

ssh mafioso-dev@163.172.99.233 -L 5000:hsmm-bbc3c188:5000 -p 38374 -L 8765:mafiachat-bbc3c188:8000
python 00-solve_complete.py

Exécuter le programme donne une commande curl pour finir, qui consiste comme l’énoncé le demande à poster un message qui va être interprété comme provenant de mafiaDEV vers mafiaBOSS :

curl http://127.0.0.1:8765/msgs -d "sig=ZKR3Lbda4aql79UmwC%2BMeEq4WfDnKBqa4lG3O7P%2Bf3M%3D&data=ZnJvbTpAbWFmaWFURVNUXHRvOkBub3RoaW5nXGNvbnRlbnQ6UVFvPYAAAAAAAAAAAAAAAAAAAAAAAAAAAAADQFxmcm9tOkBtYWZpYURFVlx0bzpAbWFmaWFCT1NT"

NOTE: Cette partie n’a pas été automatisée lors de la rédaction du write-up, car il ne va plus rester de temps pour rédiger les autres parties.

Parmi les informations retournées lors de l’appel à cette route, on retrouve notamment l’URL pour obtenir le flag de l’étape :

curl http://163.172.99.233:8080/1616c662849ee18fa8ad0f370fd6e5ac 2>&1|grep SSTIC\{
...SSTIC{b3e2c71f3e67d5a8d5855adb308...}

Analyse post-mortem

Une grosse erreur réalisée lors de cette étape a été la confiance aveugle dans les schémas réalisés et dessinés. Bien que théoriquement en phase avec le problème, il s’avère que les répercussions de la faute dans le contexte du challenge ne sont pas représentables par la propagation d’une faute sur deux rounds telle que dessinée plus haut.

En effet, vu que l’optimisation effectuée ne propage jamais réellement la valeur de c dans le calcul des autres lettres, seul le calcul des éléments qui dépendent directement de c est impacté, donc la première valeur de a2, puis la valeur de a3 qui dépend de a2, et b3 qui est une propagation de a2.

Cela a forcé le debug pas à pas pour identifier le moment de divergence entre la propagation d’une faute par le calcul et entre la propagation d’une faute par la backdoor Qemu, ce qui s’est avéré particulièrement long.