ityonemo/clrVérificateur pour les durées de vie et autres types de raffinement
Checkeur de
Lifetimes et autres
Raffinements de types
pour Zig
Vidéo : https://www.youtube.com/watch?v=mf0WzTOe-40 Sponsoring : https://buymeacoffee.com/dnautics
discussion sur hn : https://news.ycombinator.com/item?id=42923829
discussion sur lobste.rs : https://lobste.rs/s/9sitsj/clr_checker_for_lifetimes_other
vidéo de démo en direct : https://www.youtube.com/watch?v=ZY_Z-aGbYm8
Ce projet crée un transpileur Zig pour le compilateur Zig, qui transforme AIR (Abstract Intermediate Representation) en code source Zig effectuant une analyse statique à la compilation. L'analyseur généré détecte les problèmes de sécurité mémoire comme l'utilisation avant affectation, l'utilisation après libération, les échappées de pointeur de pile, ainsi que les comportements indéfinis spécifiques à Zig (assertions de non-nullité, violations d'union étiquetée, mauvais usage de fieldParentPtr).
L'objectif est d'apporter les garanties de sécurité mémoire de Rust à Zig via l'analyse statique d'AIR, sans modifier le langage lui-même.
CLR dépend d'une version forkée du compilateur Zig (incluse comme sous-module dans zig/) qui ajoute le support du routage d'AIR vers des plugins externes. Lorsqu'il est invoqué avec -ofmt=air -fair-out=<plugin.so>, le compilateur charge la bibliothèque partagée spécifiée et lui passe l'AIR généré pour traitement.
CLR vise à pousser les programmes vers des modèles de cycle de vie explicites et vérifiables localement, et non simplement à reconnaître tout programme Zig techniquement valide. Lorsque deux représentations sont possibles, CLR préfère celle qui rend l'état des ressources visible dans la structure du type et du flux de contrôle.
Par exemple, évitez de fermer conditionnellement un descripteur de fichier non optionnel :
const file = try std.fs.cwd().openFile(path, .{});
if (should_close) {
file.close(); // Mauvais : le fichier est ambiguëment ouvert après cette branche.
}
Préférez représenter la possession conditionnelle avec un optionnel :
var file: ?std.fs.File = null;
if (should_open) {
file = try std.fs.cwd().openFile(path, .{});
}
if (file) |open_file| {
open_file.close();
}
Fermer conditionnellement un descripteur non optionnel laisse son cycle de vie ambigu après la branche. La politique prévue de CLR est de rejeter ce modèle plutôt que de porter un état permanent « peut-être fermé ».
Le même principe s'applique aux pointeurs alloués. Ne libérez pas via un pointeur dérivé :
const allocation = try allocator.alloc(u8, size);
const payload = allocation[header_size..];
allocator.free(payload); // Mauvais : payload n'est pas la base de l'allocation.
Gardez le pointeur de base de l'allocation disponible pour la désallocation, et utilisez les pointeurs dérivés uniquement pour l'accès :
const allocation = try allocator.alloc(u8, size);
defer allocator.free(allocation);
const payload = allocation[header_size..];
use(payload);
Libérer un pointeur de champ, une sous-tranche ou un pointeur produit par arithmétique est rejeté à moins qu'une règle interne documentée ne rétablisse la provenance de la base d'allocation.
Ces politiques sont strictes par défaut car elles produisent un code avec des cycles de vie de ressources plus simples et plus faciles à réviser. Un futur mécanisme d'annotation unsafe permettra à certains GID ou opérations de se retirer de certaines analyses. Cela supportera du code qui accepte délibérément une vérification plus faible en échange de performances, sans affaiblir le modèle par défaut pour le reste du programme.
Il s'agit d'une réécriture active en Zig de la preuve de concept originale basée sur Elixir. L'implémentation Zig se charge comme un plugin de compilateur et analyse AIR directement.
Actuellement implémenté :
std.mem.Allocator :
create/destroy - allocation d'élément uniquealloc/free - allocation de tranche (y compris alignedAlloc, allocSentinel, etc.)realloc/remap - réallocation de tranche avec suivi de l'ancienne tranche libéréedupe/dupeZ - duplication de trancheinit// - cycle de vie complet de l'arènePrévu (voir LIMITATIONS.md pour les détails) :
sudo apt install batsLe compilateur Zig fourni et le plugin libclr doivent être construits avec des niveaux d'optimisation correspondants. Des niveaux d'optimisation non correspondants provoqueront des segfaults.
# Construire le compilateur Zig personnalisé avec ReleaseFast (première fois uniquement, ou après modifications du sous-module)
cd zig && zig build --zig-lib-dir lib -Doptimize=ReleaseFast && cd ..
# Construire le plugin CLR avec l'optimisation correspondante
zig build -Doptimize=ReleaseFast
Pour le développement/débogage, utilisez ReleaseSafe ou Debug pour les deux :
# ReleaseSafe (avec vérifications de sécurité, légèrement plus lent)
cd zig && zig build --zig-lib-dir lib -Doptimize=ReleaseSafe && cd ..
zig build -Doptimize=ReleaseSafe
# Debug (informations de débogage complètes, plus lent)
cd zig && zig build --zig-lib-dir lib && cd ..
zig build
# Compiler un fichier Zig en utilisant le backend AIR
zig/zig-out/bin/zig build-exe -fair-out=zig-out/lib/libclr.so -ofmt=air -femit-bin=output.air.zig your_file.zig
# Exécuter l'analyseur généré
zig run --dep clr -Mroot=output.air.zig -Mclr=lib/lib.zig
La sortie va sur stderr.
# Tests unitaires (codegen/DLL)
zig build test
# Tests unitaires (bibliothèque runtime)
zig test lib/lib.zig
# Un fichier de test d'intégration ciblé
bats test/integration/fd.bats
# Tests d'intégration (nécessite BATS)
# Par défaut ReleaseFast ; remplacer avec OPTIMIZE=ReleaseSafe ou OPTIMIZE=Debug
./run_integration.sh
# Test manuel d'un seul fichier
./run_one.sh test/cases/undefined/use_before_assign.zig
Remarque : Les tests d'intégration reconstruisent libclr avec le niveau d'optimisation spécifié (par défaut : ReleaseFast). Assurez-vous que votre compilateur Zig fourni a été construit avec un niveau d'optimisation correspondant.
clr/
├── src/ # Code de la DLL/plugin (génère .air.zig)
│ ├── clr.zig # Point d'entrée principal du plugin CLR
│ ├── codegen.zig # Génère le source .air.zig à partir des instructions AIR
│ └── allocator.zig # Wrapper d'allocateur compatible DLL
├── lib/ # Bibliothèque d'analyse runtime
│ ├── lib.zig # Point d'entrée de la bibliothèque
│ ├── tag.zig # Union AnyTag, Type, handlers de tag, distribution splat
│ ├── Inst.zig # Résultats d'instruction et analyse interprocédurale
│ ├── Refinements.zig # Types de raffinement (pointeur, struct, optionnel, etc.)
│ ├── Analyte.zig # Conteneur d'état d'analyse
│ ├── Context.zig # Contexte d'exécution (métadonnées, rapport d'erreurs)
│ └── analysis/ # Modules d'analyse
│ ├── undefined_safety.zig # Suivi d'utilisation avant affectation
│ ├── memory_safety.zig # Suivi d'allocation/libération
│ ├── null_safety.zig # Vérification de déballage d'optionnel
│ ├── variant_safety.zig # Accès aux champs d'union étiquetée
│ └── fd_safety.zig # Suivi des descripteurs de fichier
├── test/
│ ├── integration/ # Tests d'intégration BATS
│ │ ├── test_helper.bash
│ │ └── *.bats
│ └── cases/ # Fichiers d'entrée de test (.zig)
├── zig/ # Sous-module du compilateur Zig (fork instrumenté)
├── build.zig # Configuration de construction
└── build.zig.zon # Dépendances de paquet
Zig est un langage notoirement « unsafe ». La gestion de la mémoire est manuelle, ce qui ouvre la possibilité d'erreurs d'implémentation. Bien que Zig réduise les problèmes de sécurité par rapport à C en éliminant les accès hors limites aux tableaux et les déréférencements de pointeur nul dans le code vérifié, il reste moins sûr que Rust, qui élimine les utilisations après libération, les doubles libérations et les courses de données grâce à l'analyse statique.
Inspiré par le projet MIRI de Rust, CLR effectue une analyse statique sur la représentation intermédiaire AIR de Zig pour atteindre un degré de sécurité plus élevé que celui fourni par Zig par défaut. Contrairement à MIRI, qui interprète le MIR de Rust dans un pseudo-runtime en bac à sable, CLR transpile AIR en code source Zig qui exécute l'analyse de manière statique. Notez que le code zig de sortie d'air de CLR pourrait en principe être exécuté au moment de la compilation, mais en passant par un intermédiaire zig, on produit un flux logique facile à comprendre et à déboguer. Une personne ambitieuse pourrait utiliser cette approche générale pour émettre une cible de sortie différente, comme un langage d'assistant de preuve, ou la refactoriser pour qu'elle s'exécute entièrement dans le compilateur zig !
L'idée clé : si vous avez besoin de MIRI pour les projets Rust soucieux de sécurité de toute façon, pourquoi ne pas choisir un langage plus simple et faire une analyse de style MIRI pour obtenir la vérification d'emprunt et d'autres analyses de type raffinement ? Ce projet montre qu'un tel avenir est une réelle possibilité pour Zig.
Le pipeline de compilation Zig est :
AIR est le niveau idéal pour l'analyse car il est typé, interprétable comme une liste « minimale viable » d'instructions de programmation généralisées, et permet d'étendre les types avec des métadonnées de raffinement.
Pour un aperçu approfondi du fonctionnement d'AIR dans Zig, voir l'article de blog de Mitchell Hashimoto : https://mitchellh.com/zig/sema
Licence MIT - voir LICENSE pour plus de détails.
deinitallocatorstd.process.args,
std.mem.asBytes, std.HashMap et les APIs d'allocateur/fichierstd.HashMap avec identité canonique de métadonnées/clé/valeur
à travers put, get, getPtr et itération de valeursposix.open/close/dup/dup2/socket/accept/epoll_create/pipe