Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels

Die Arbeit stellt Model2Kernel vor, ein System zur automatisierten, modellbewussten symbolischen Ausführung, das erstmals die Speichersicherheit von CUDA-Kernen in LLM-Inferenzsystemen verifiziert und dabei 353 bisher unbekannte Fehler aufdeckt.

Das Wesentliche

Stellen Sie sich vor, Sie bauen eine riesige, hochmoderne Bibliothek, in der ein genialer, aber etwas chaotischer Bibliothekar (das KI-Modell) arbeitet. Dieser Bibliothekar ist darauf spezialisiert, Millionen von Büchern (Daten) blitzschnell zu finden und zusammenzufassen. Um diese Arbeit zu erledigen, nutzt er eine Armee von Robotern (die CUDA-Kernel), die auf einem super-schnellen, aber empfindlichen Computer (der GPU) laufen.

Das Problem: Diese Roboter arbeiten mit einer extremen Geschwindigkeit und einem sehr komplexen System. Wenn auch nur ein einziger Roboter einen Fehler macht – zum Beispiel, wenn er versucht, in ein Regal zu greifen, das gar nicht existiert, oder wenn er die Zahlen für die Regalposition falsch berechnet –, kann das ganze System abstürzen. Schlimmer noch: Ein böswilliger Hacker könnte diesen Fehler ausnutzen, um die Bücher im Regal zu manipulieren oder die Bibliothek zu übernehmen.

Bisher gab es keine gute Methode, um diese Roboter sicher zu überprüfen, bevor sie in die echte Bibliothek geschickt werden. Herkömmliche Werkzeuge waren entweder zu langsam, benötigten spezielle Hardware, die niemand hat, oder sie konnten nicht mit den sich ständig ändernden Aufgaben der KI umgehen.

Hier kommt Model2Kernel ins Spiel. Man kann es sich wie einen super-intelligenten Sicherheitsinspektor vorstellen, der zwei besondere Fähigkeiten hat:

1. Der "Architekt-Versteher" (HFProbe)

Stellen Sie sich vor, Sie wollen einen Roboter testen, aber Sie wissen nicht genau, welche Aufgabe er heute hat. Ist er heute für kleine Bücher zuständig oder für riesige Enzyklopädien?
Der erste Teil von Model2Kernel, nennen wir ihn HFProbe, ist wie ein Detektiv, der sich die Baupläne der Bibliothek (das KI-Modell) genau anschaut, ohne den Roboter tatsächlich laufen zu lassen. Er lernt:

• "Ah, dieser Roboter wird immer für Regale mit genau 7168 Fächern gebaut." (Das ist festgelegt durch den Plan).
• "Aber die Anzahl der Bücher, die er heute sortiert, hängt davon ab, wie viele Besucher kommen." (Das ist variabel).

HFProbe erstellt also eine perfekte Checkliste für den Roboter, die genau sagt: "Du musst hier fest bleiben, aber dort darfst du variieren."

2. Der "Traum-Reisender" (cuKLEE)

Der zweite Teil, cuKLEE, ist der eigentliche Testfahrer. Aber er fährt nicht auf der echten Straße (was teuer und langsam wäre). Stattdessen reist er in einer Art Träumerei oder Simulation.
Anstatt den Roboter nur einmal mit echten Zahlen laufen zu lassen, stellt er sich vor: "Was wäre, wenn 100 Besucher kommen? Was wäre, wenn 1 Million? Was wäre, wenn die Regale doppelt so hoch sind?"
Er simuliert alle diese Möglichkeiten gleichzeitig in einem einzigen Durchgang. Er nutzt eine Art "magische Brille", mit der er sieht, ob der Roboter bei irgendeiner dieser hypothetischen Situationen versehentlich gegen eine Wand läuft (Speicherüberlauf) oder eine Zahl berechnet, die zu groß für seinen Taschenrechner ist (Integer-Überlauf).

Warum ist das so wichtig?

In der echten Welt passiert es oft, dass ein KI-Modell so groß wird, dass die Roboter die Zahlen für die Regalpositionen nicht mehr in ihren kleinen Köpfen (den 32-Bit-Zahlen) speichern können. Sie "überlaufen" und zeigen dann auf das falsche Regal. Das führt zu Chaos.

Model2Kernel hat in Tests 353 solcher Fehler gefunden, die bisher niemand bemerkt hatte! Das ist, als würde man vor der Eröffnung einer neuen Brille 353 Risse im Beton finden, die sonst dazu geführt hätten, dass die Brücke einstürzt.

Die Zusammenfassung in einer Metapher

• Das Problem: KI-Modelle sind wie riesige Orchester, die auf tausenden Instrumenten (GPU-Threads) spielen. Wenn ein Musiker einen falschen Ton spielt, klingt das ganze Stück schrecklich oder das Orchester explodiert.
• Die alte Lösung: Man hörte nur zu, wenn das Orchester spielte (Dynamische Analyse), aber das war zu langsam, oder man versuchte, die Noten im Voraus zu lesen (Statische Analyse), aber die Noten waren zu unklar.
• Die neue Lösung (Model2Kernel): Ein Dirigent, der erst die Partitur genau studiert (HFProbe), um zu wissen, welche Instrumente wann spielen müssen, und dann in einer Simulation alle möglichen Fehler durchspielt (cuKLEE), bevor auch nur ein einziger Ton im echten Konzertsaal erklingt.

Das Ergebnis: Durch diese Kombination aus "Plan-Verstehen" und "Alles-Imaginieren" können wir sicherstellen, dass die KI-Systeme, die unsere Zukunft antreiben, sicher, stabil und nicht hackbar sind. Es ist ein riesiger Schritt, um die digitale Infrastruktur unserer Welt sicherer zu machen.

Technische Zusammenfassung

1. Problemstellung

Die weitverbreitete Nutzung von Large Language Models (LLMs) hat GPU-beschleunigte Inferenz zu einem kritischen Bestandteil der modernen Recheninfrastruktur gemacht. Diese Systeme basieren auf CUDA-Kernen, die die komplexen linearen Algebra-Operationen von Transformer-Architekturen ausführen. Diese Kerne sind jedoch aufgrund mehrerer Faktoren extrem anfällig für Speicher-Sicherheitsfehler:

• Modellabhängige Tensor-Layouts: Die Speicherstrukturen hängen von der spezifischen Modellarchitektur ab.
• Komplexe Indexierung: Feingranulare Berechnungen über große Tensoren und Tausende von Threads führen leicht zu Zugriffen außerhalb der Grenzen (Out-of-Bounds) und Datenrennen.
• Variable Eingabelängen: Inferenzsequenzen können sehr lang sein, was das Risiko von Integer-Overflows erhöht.
• Folgen: Solche Fehler können Modellgewichte korrumpieren, Inferenzdienste zum Absturz bringen oder sogar für adversarische Angriffe (z. B. willkürliche Codeausführung auf der GPU) missbraucht werden.

Bestehende Techniken zur Fehlererkennung sind unzureichend:

• Dynamische Methoden (z. B. Compute Sanitizer) haben hohe Laufzeitkosten oder benötigen spezielle Hardware.
• Statische Analyse-Tools können oft keine Puffer verarbeiten, deren Größe erst zur Laufzeit bestimmt wird, und scheitern an der Variabilität der Kernel-Konfigurationen.

2. Methodik: Model2Kernel

Model2Kernel ist das erste praktische System zur automatisierten Verifikation der Speichersicherheit von CUDA-Kernen in LLM-Inferenzsystemen. Es kombiniert zwei Hauptkomponenten, um die Lücke zwischen statischer Analyse und dynamischer Ausführung zu schließen:

A. HFProbe (Dynamisches Modell-Profilieren)

HFProbe analysiert, wie ein bestimmtes LLM-Modell CUDA-Kerne aufruft, ohne dass GPU-Hardware benötigt wird.

• Funktionsweise: Es führt das Modell in einer simulierten Umgebung (mit „gefälschten" CUDA-Kernen) aus. Dabei werden die Aufrufmuster protokolliert.
• Konfigurationsmutation: HFProbe nutzt einen LLM-Agenten, um die Modellkonfigurationen (z. B. config.json) systematisch zu variieren, um mehr verschiedene CUDA-Kerne zu aktivieren, die sonst nicht ausgelöst würden.
• Ergebnis: Es klassifiziert Kernel-Argumente in zwei Kategorien:
  1. Modell-fixiert: Werte, die durch die Architektur bestimmt sind (z. B. versteckte Größe) und während der Analyse konstant bleiben sollten.
  2. Benutzerkontrolliert: Werte, die von der Eingabe abhängen (z. B. Batch-Größe, Sequenzlänge) und als symbolische Variablen behandelt werden müssen.

B. cuKLEE (CUDA-spezifische Symbolische Ausführung)

cuKLEE ist eine auf CUDA spezialisierte symbolische Ausführungs-Engine, die auf KLEE aufbaut. Sie nutzt die Informationen von HFProbe, um effizient und präzise zu arbeiten.

• Speichermodell für Tensoren: Anstatt einen zusammenhängenden Speicher zu verwenden, modelliert cuKLEE jeden Tensor als einen diskreten, weit voneinander entfernten Speicherbereich. Dies vereinfacht die Zuordnung von Zeigern zu Tensoren und die Grenzwertprüfung erheblich.
• Symbolische Tensor-Eigenschaften: Es führt symbolische Variablen für Basisadressen, Elementanzahl, Dimensionen und Datentypen ein. Tensor-Methoden (z. B. sum, view) werden durch Constraints zusammengefasst, die die Beziehungen zwischen den Tensoren abbilden.
• Thread-Skalierung: Anstatt jeden Thread einzeln zu simulieren, behandelt cuKLEE Thread- und Block-Identifikatoren (threadIdx.x, blockIdx.x) als symbolische Variablen. Dies ermöglicht eine einheitliche Analyse von Tausenden parallelen Threads in einem einzigen Durchlauf.
• Fehlererkennung: Das System prüft auf vier Fehlerarten: Buffer Overflows, Integer Overflows, Datenrennen (Data Races) und NULL-Pointer-Dereferenzierungen.

3. Schlüsselbeiträge

1. cuKLEE: Entwicklung einer spezialisierten symbolischen Ausführungs-Engine für CUDA, die dynamische Tensor-Formen unterstützt und auf Tausende von Threads skaliert.
2. HFProbe: Entwicklung eines dynamischen Profilierungswerkzeugs, das modellabhängige Kernel-Argumente automatisch ableitet und durch Konfigurationsmutation die Abdeckung erhöht.
3. Integriertes Framework (Model2Kernel): Die Kombination beider Komponenten ermöglicht eine vollautomatische Analyse von CUDA-Kernen in realen LLM-Inferenzsystemen (unterstützt Hugging Face-Formate).
4. Praktische Validierung: Umfassende Experimente mit realen Modellen und Kernen, die die Wirksamkeit des Ansatzes belegen.

4. Ergebnisse

Die Evaluierung umfasste 120 Modelle und 173 CUDA-Kerne aus drei Quellen:

• vLLM (Text-Generierungs-Modelle)
• Hugging Face (Modelle mit benutzerdefinierten Kernen)
• Aktuelle Forschungsarbeiten (Top-Tier-Publikationen)

Ergebnisse:

• Fehlererkennung: Model2Kernel entdeckte 353 bisher unbekannte Speicherfehler.
  • Davon waren 328 Integer-Overflows.
  • 25 Zugriffe außerhalb der Grenzen (Out-of-Bounds).
  • Keine Datenrennen oder NULL-Pointer-Dereferenzierungen wurden in diesem Datensatz gefunden.
• Genauigkeit: Die False-Positive-Rate lag bei nur 2,49 % (9 False Positives).
• Vergleich mit Baselines: Im Vergleich zu bestehenden Tools (Honeycomb, GKLEE, ESBMC-GPU) konnte cuKLEE 15 von 20 bekannten vLLM-Fehlern finden, während die Baselines nur 0 bis 5 fanden.
• Kosten: Die Analyse erforderte insgesamt ca. 986 Stunden Rechenzeit und moderate Kosten für LLM-Agenten, was bei über 100.000 Zeilen Code als moderat eingestuft wird.

5. Bedeutung

Model2Kernel adressiert eine kritische Sicherheitslücke in der KI-Infrastruktur. Da LLM-Inferenzsysteme zunehmend in Produktion eingesetzt werden, stellen Speicherfehler in CUDA-Kernen ein erhebliches Risiko für die Stabilität und Sicherheit dar (z. B. Manipulation von Modellgewichten).

• Paradigmenwechsel: Das Paper zeigt, dass durch die Kombination von dynamischem Profilieren (um den Kontext zu verstehen) und spezialisierter symbolischer Ausführung (um den Code zu analysieren) komplexe Speicherfehler in GPU-Code automatisch und skalierbar gefunden werden können.
• Praktischer Nutzen: Entwickler können Model2Kernel nutzen, um neue Kernel-Optimierungen zu validieren oder sicherzustellen, dass neue Modellarchitekturen sicher mit bestehenden Kernen interagieren.
• Zukunftsausblick: Die vorgestellten Konzepte (Modellierung dynamischer Arrays als diskrete Bereiche, Symbolisierung von Thread-IDs) bieten eine Grundlage für die Erweiterung auf andere Hardware-Architekturen (z. B. NPUs) und andere Fehlertypen.

Zusammenfassend demonstriert Model2Kernel, dass eine „modellbewusste" Analyse entscheidend ist, um die Komplexität moderner LLM-Inferenzsysteme zu bewältigen und deren Speichersicherheit zu gewährleisten.