"Th\u00E8ses et \u00E9crits acad\u00E9miques" . . . "Formalization and guaranty of system security properties, application to the detection of intrusions" . . . . "2007" . . . . . . "Syst\u00E8mes informatiques -- Mesures de s\u00FBret\u00E9" . . "Syst\u00E8mes informatiques" . . "Text" . "Ordinateurs -- Acc\u00E8s -- Contr\u00F4le" . "Formation et garantie de propri\u00E9t\u00E9s de s\u00E9curit\u00E9 syst\u00E8me, application \u00E0 la d\u00E9tection d'intrusions" . "Dans cette th\u00E8se, nous nous int\u00E9ressons \u00E0 la garantie des propri\u00E9t\u00E9s d'int\u00E9grit\u00E9 et de confidentialit\u00E9 d'un syst\u00E8me d'information. Nous proposons tout d'abord un langage de description des activit\u00E9s syst\u00E8me servant de base \u00E0 la d\u00E9finition d'un ensemble de propri\u00E9t\u00E9s de s\u00E9curit\u00E9. Ce langage repose sur une notion de d\u00E9pendance causale entre appels syst\u00E8me et sur des op\u00E9rateurs de corr\u00E9lation. Gr\u00E2ce \u00E0 ce langage, nous pouvons d\u00E9finir toutes les propri\u00E9t\u00E9s de s\u00E9curit\u00E9 syst\u00E8me classiquement rencontr\u00E9es dans la litt\u00E9rature, \u00E9tendre ces propri\u00E9t\u00E9s et en proposer de nouvelles. Afin de garantir le respect de ces propri\u00E9t\u00E9s, une implantation de ce langage est pr\u00E9sent\u00E9e. Nous prouvons que cette implantation capture toutes les d\u00E9pendances perceptibles par un syst\u00E8me. Cette m\u00E9thode permet ainsi d'\u00E9num\u00E9rer l'ensemble des violations possibles des propri\u00E9t\u00E9s mod\u00E9lisables par notre langage. Notre solution exploite la d\u00E9finition d'une politique de contr\u00F4le d'acc\u00E8s afin de calculer diff\u00E9rents graphes. Ces graphes contiennent les terminaux du langage et permettent de garantir le respect des propri\u00E9t\u00E9s exprimables. Nous utilisons alors cette m\u00E9thode pour fournir un syst\u00E8me de d\u00E9tection d'intrusion qui d\u00E9tecte les violations effectives des propri\u00E9t\u00E9s. L'outil peut r\u00E9utiliser les politiques de contr\u00F4le d'acc\u00E8s disponibles pour diff\u00E9rents syst\u00E8mes cibles DAC (Windows, Linux) ou MAC tels que SELinux et grsecurity. Cet outil a \u00E9t\u00E9 exp\u00E9riment\u00E9 sur un pot de miel durant plusieurs mois et permet de d\u00E9tecter les violations des propri\u00E9t\u00E9s souhait\u00E9es." . "Formation et garantie de propri\u00E9t\u00E9s de s\u00E9curit\u00E9 syst\u00E8me, application \u00E0 la d\u00E9tection d'intrusions" .