Static Detection of Post-Quantum Cryptographic Algorithms in Stripped Binaries for Digital Forensic Examination and Migration Assurance

Technische Samenvatting: Statische Detectie van Post-Quantum Cryptografische Algoritmen in Stripped Binaries

Probleemstelling
De overgang naar post-quantum cryptografie (PQC) staat voor een kritiek verificatiegat: hoewel er instrumenten bestaan om kwantumkwetsbare algoritmen (RSA, ECC) in broncode of binaries te identificeren, is er geen gevestigde methode om de aanwezigheid van gestandaardiseerde post-quantum algoritmen (specifiek ML-KEM en ML-DSA) in gecompileerde, gestripte en statisch gelinkte binaries te verifiëren. Bestaande tools voor cryptografische ontdekking vertrouwen op symbolen, bibliotheekafhankelijkheden, runtime-gedrag of netwerkverkeer. Deze signalen worden vernietigd door standaard build-transformaties zoals het strippen van symbolen, statische linking en compiler-optimalisatie. Gevolgelijk kunnen auditors en forensische onderzoekers niet bevestigen of een binary daadwerkelijk PQC implementeert of het slechts claimt, een onderscheid dat urgent is geworden door de opkomst van PQC-ondersteunde malware (bijv. de "Kyber" ransomware-familie) en regelgevende mandaten (bijv. Executive Order 14412) die de verificatie van ingezette cryptografische primitieven vereisen.

Methodologie: De Kestrel-aanpak
Het paper introduceert Kestrel, een statische analyse-tool die ML-KEM en ML-DSA identificeert door de Number-Theoretic Transform (NTT) constante tabellen te detecteren die zijn ingebed in de read-only datasecties van binaries.

1. Het Signaal: ML-KEM en ML-DSA vertrouwen op polynoomvermenigvuldiging via de NTT, wat precomputed tabellen vereist van machten van een vaste eenheidswortel ($\zeta$) modulo een priemgetal ($q$). In tegenstelling tot code zijn deze constante tabellen data; ze kunnen niet worden verwijderd of gewijzigd door optimalisatie zonder de correctheid van het algoritme te breken. Ze blijven behouden na stripping en statische linking.
2. Fingerprint-afleiding: In plaats van handmatig een lijst met signatures samen te stellen, gebruikt Kestrel een deterministisch proces om de volledige set fingerprints te genereren vanuit publieke schema-parameters ($q$, $\zeta$, transformatie-lengte, bit-reversal breedte). De generator produceert drie families van constanten: forward twiddles, inverse twiddles en base-case/mod-root constanten. Het houdt rekening met diverse opslagrepresentaties, inclusief Montgomery-vorm, signed/unsigned integers en gevectoriseerde lay-outs.
3. Detectie-pipeline:
   • Normalisatie: De detector scant de read-only datasectie en normaliseert kandidaat-waarden naar canonieke residuen modulo $q$. Dit handelt signed versus unsigned representaties af en converteert de Montgomery-vorm terug naar plain residuen.
   • Multiset Scoring: In plaats van exacte byte-matching, scoort de detector een venster op basis van het aantal verwachte canonieke residuen dat het bevat, waarbij ze als een multiset worden behandeld. Deze onafhankelijkheid van volgorde vangt variaties in vectorisatie en lay-out op.
   • Corroboratie: De aanwezigheid van Keccak round constants (gebruikt door de onderliggende SHAKE-functie) wordt gecontroleerd als een secundaire voorwaarde om de betrouwbaarheid te versterken, hoewel dit geen harde eis is om false negatives te voorkomen.
   • Attributie: Het totale aantal bytes van de twiddle-tabellen dient als een provenance-marker. Verschillende implementatie-lineages (bijv. referentie C, Go standaardbibliotheek, Chrome/BoringSSL) slaan een verschillend aantal tabellen op (1, 2 of 3), waardoor de tool de binary kan attribueren aan een specifieke bron-lineage.

Belangrijkste Bijdragen

1. Afleidingsprocedure: Een algemene methode om fingerprint-sets te genereren voor elk transformatie-gebaseerd lattice-schema op basis van enkel publieke parameters, wat dekking garandeert voor toekomstige of ononderzochte implementaties.
2. Robuuste Detector: Een scoringmechanisme dat data normaliseert en multiset-matching gebruikt om een hoge recall te bereiken over verschillende compilers, optimalisatieniveaus en obfuscatietechnieken, met een analytisch afgeleide false-positive grens.
3. Lineage Attributie: Een aangetoond vermogen om tussen de belangrijkste implementatie-lineages (C-referentie versus from-specification) te onderscheiden op basis van enkel de configuratie en het aantal constante tabellen, zonder toegang tot de broncode.
4. Operationele Validatie: De methode wordt gevalideerd in twee specifieke contexten: forensisch onderzoek (analyseren van in beslag genomen disk-images waar executie onmogelijk is) en migratie-assurance (verifiëren van leveranciersclaims tegen geleverde binaries).

Experimentele Resultaten

• Recall en Precisie: In experimenten over vier onafhankelijke implementatie-lineages (C, Go, Rust, BoringSSL) en alle build-transformaties (inclusief stripping, statische linking en LLVM instructie-substitutie), behaalde Kestrel een 128/128 recall voor ML-KEM en 255/256 voor ML-DSA (de enkele misser is een bekende quirk in de referentie-implementatie, geen detectiefout). De precisie was 100% met nul false positives.
• Systeem-sweep: Een scan van 6.224 binaries van een productie Linux-systeem onthulde nul false positives. Het identificeerde 12 verschillende ongecatalogiseerde programma's die ML-KEM bevatten, waaronder de OpenSSH key-exchange binary en de container-management stack (containerd, docker, runc). Opvallend genoeg bevatten de container-tools PQC-code die afkomstig is van de Go taal-runtime zonder expliciet bewustzijn van de projectbeheerders.
• Forensisch Herstel: In een proef met een verwijderde binary op een disk-image faalde conventionele file carving bij het terughalen van het bestand. Kestrel detecteerde echter de ML-KEM tabel door de ruwe unallocated space te scannen, wat aantoont dat het signaal de file-level destructie overleeft.
• Adversarial Evasion: De tool bood weerstand tegen triviale evasies (herordening, padding, splitsen van tabellen). Alleen een "byte-rewrite" evasie (het XOR'en van de tabel met een runtime key) versloeg de detectie, wat een substantiële modificatie van de cryptografische code vereist.

Betekenis en Claims
Het paper stelt dat Kestrel de eerste praktische methode biedt voor het verifiëren van de aanwezigheid van post-quantum lattice-schema's in stripped binaries, waarmee een blinde vlek in huidige migratie- en forensische tooling wordt geadresseerd.

• Compliance: Het maakt de verificatie van wettelijke migratiedeadlines mogelijk door te bevestigen dat een binary daadwerkelijk de geclaimde PQC-primitieven bevat, in plaats van te vertrouwen op leveranciersverklaringen of scans op bronniveau.
• Forensics: Het stelt onderzoekers in staat om genuante PQC-implementaties te onderscheiden van frauduleuze claims (bijv. malware die PQC claimt maar RSA gebruikt) en om PQC te detecteren in verwijderde of beschadigde bestanden.
• Scope Beperking: De auteur stelt expliciet de grenzen van de methode vast: deze is alleen van toepassing op lattice-schema's met opgeslagen transformatie-tabellen (ML-KEM, ML-DSA) en gaat uit van standaard build-praktijken. Het dekt geen hash-gebaseerde schema's (SLH-DSA), schema's die constanten tijdens runtime berekenen, of managed runtimes waar constanten als instructies in plaats van datatabellen kunnen worden uitgegeven.

Het paper concludeert dat hoewel de techniek van constant matching gevestigd is, de toepassing ervan op post-quantum primitieven in stripped binaries nieuw en noodzakelijk is, aangezien deze primitieven een vingerafdruk achterlaten die een gewone compilatie niet kan verwijderen.