présentation
Kani est un vérificateur de modèles open-source pour Rust qui étend la vérification bornée pour fournir des garanties de correction pour les propriétés telles que la sécurité des opérations non sécurisées, la correction fonctionnelle et l'absence de paniques à l'exécution.
fonctionnement
Kani compile des harnais de preuve à partir de la représentation intermédiaire de niveau moyen (MIR) de Rust dans le moteur de vérification bit-precise de CBMC, vérifiant automatiquement un ensemble complet de propriétés de sécurité sans annotation utilisateur.
analyse scientifique
Les études de cas sur des projets Rust industriels ont montré la faisabilité de Kani, avec des contrats qui ont amélioré la vérification de la liberté de panique à la correction fonctionnelle, révélant six bogues inconnus auparavant.
implications et limites
Kani fonctionne à grande échelle dans la production CI, avec plus de 16 000 harnais vérifiés par modification de code dans la campagne de vérification de la bibliothèque standard Rust. Cependant, la vérification bornée a des limites, et Kani fournit un langage de spécification pour étendre la vérification à des propriétés non bornées.
