(Sécurité) Assertions par des grands modèles de langage

La sécurité des systèmes informatiques repose généralement sur une racine de confiance matérielle. Les vulnérabilités dans le matériel peuvent avoir des conséquences graves sur un système, il est donc nécessaire de disposer de techniques pour soutenir les activités de vérification de la sécurité. La vérification basée sur les assertions est une technique de vérification populaire qui consiste à capturer l'intention de conception dans un ensemble d'assertions pouvant être utilisées dans la vérification formelle ou dans la vérification basée sur des tests. Cependant, écrire des assertions centrées sur la sécurité est une tâche difficile. Dans ce travail, nous examinons l'utilisation de modèles de langage de grande taille émergents (LLMs) pour la génération de code dans la génération d'assertions matérielles pour la sécurité, où des prompts principalement en langage naturel, tels que ceux que l'on pourrait voir comme commentaires de code dans des fichiers d'assertions, sont utilisés pour produire des assertions SystemVerilog. Nous concentrons notre attention sur un LLM populaire et caractérisons sa capacité à écrire des assertions prêtes à l'emploi, compte tenu de différents niveaux de détail dans le prompt. Nous concevons un cadre d'évaluation qui génère une variété de prompts, et nous créons une suite de référence comprenant de véritables conceptions matérielles et des assertions de référence correspondantes que nous souhaitons générer avec le LLM.