Formalisation de la sémantique des appels système pour un système de type UNIX
Résumé
Nous cherchons à tester kblare, un module de détection d’intrusion pour le noyau Linux. Les tests unitaires développés manuellement, pour lesquels testeur doit spécifier lui-même l’état de départ et l’état final attendu du système, ne donnent aucune garantie forte sur la couverture du code et sur la correction de kblare. Nous développons donc une approche pour la construction formelle de tests. En faisant l’hypothèse de travail que seuls les appels système causent des flux d’information dans un système d’exploitation, nous construisons une sémantique des appels système en termes de flux d’information nous permettant de définir de meilleurs tests. Nous montrons la faisabilité de cette approche en construisant une sémantique utilisant la logique transactionnelle concurrentielle. Nous présentons dans un second temps notre prototype d’interpréteur pour cette sémantique et montrons comment construire et exécuter de simples tests. Nous donnons nos premiers résultats. Ils sont positifs et nous ont convaincu du bien-fondé de l’approche, bien que nous nous heurtions à des problèmes de performance ainsi qu’à l’impossibilité de modéliser certaines situations. Nous concluons avec nos futures directions de recherche sur cette approche.
Loading...