Formalisation de la sémantique des appels système pour un système de type UNIX - DUMAS - Dépôt Universitaire de Mémoires Après Soutenance Accéder directement au contenu
Mémoires Année : 2014

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.
Fichier principal
Vignette du fichier
mri20132014_submission_46.pdf (2.15 Mo) Télécharger le fichier
Loading...

Dates et versions

dumas-01088795 , version 1 (28-11-2014)

Licence

Paternité

Identifiants

  • HAL Id : dumas-01088795 , version 1

Citer

Laurent Georget. Formalisation de la sémantique des appels système pour un système de type UNIX. Informatique [cs]. 2014. ⟨dumas-01088795⟩
164 Consultations
265 Téléchargements

Partager

Gmail Facebook X LinkedIn More