Cours Politique de sécurité informatique
...
Définition d’une politique de sécurité politique de sécurité : ensemble de lois, de règles et de pratiques qui régissent la fa¸con dont l’information sensible et les autres ressources sont :
gérées
protégées
distribuées à l’intérieur d’un système d’informations
Définition d’une politique de sécurité
objectifs d’une politique de sécurité
protéger le SI contre les menaces identifiées par l’analyse de
risques
plus précisémment définir :
les objectifs de sécurité décrivant les propriétés de :
confidentialité
intégrité
disponibilité
l’état du système o`u ces propriétés sont vérifées
des règles de sécurité décrivant les moyens de modifier
l’état de sécurité du système les politiques de sécurité sont classées en 3 catégories
les politiques de sécurité internes
les politiques de sécurité techniques
les politiques de sécurité système
les politiques de sécurité internes aspects organisationnels
procédures sur la :
répartition des tâches et responsabilités entre utilisateurs
limitation du cumul de pouvoir séparation de pouvoir dans une organisation les politiques de sécurité techniques aspects matériels et logiciels procédures sur :
le vol
les catastrophes naturelles
le feu, · · ·
les politiques de sécurité système spécifient l’ensemble des lois, des règlements et pratiques qui régissent la fa¸con de : gérer protéger diffuser les informations et les autres ressources sensibles au sein du SI les politiques de sécurité système s’appuie sur politique d’identification : identifier de manière unique chaque utilisateur politique d’authentification : permet à l’utilisateur de prouver son identité politique d’autorisation : détermine les opérations légitimes qu’un utilisateur peut réaliser
Une politique de sécurité doit être bien définie cohérente complète
Une politique de sécurité doit être mise en application : sensibilisation
simplicité (définition et implantation)
Une politique de sécurité doit être un document de référence adopté par tous
Différentes méthodes :
MARION (Méthodologie d’Analyse de Risques Informatiques
Orientée par Niveaux)
…
EBIOS (Expression des Besoins et Identification des Objectifs de Sécurité)
Mise en oeuvre d’une politique de sécurité choix des mécanismes les plus simples possibles permettant de protéger les ressources, de manière la plus efficace avec un coût acceptable
système d’authentification (biométrie, serveur d’authentification , · · ·) chiffrement (PKI, mécanismes intégrés à des protocoles de communication (IPsec), · · ·)
pare feux (firewall)
système anti-virus
outil de détection de failles de sécurité
système de détection d’intrusions
système d’exploitation sécurisé
validation d’une politique de sécurité audit de sécurité par un tiers de confiance valide les moyens de protection mis en œuvre par rapport à la politique de sécurité vérifie que chaque règle de sécurité est correctement appliquée l’ensemble des dispositions forme un tout cohérent et sûr test d’une politique de sécurité test d’intrusion : éprouver les moyens de protection d’un SI en essayant de s’introduire dans le système en situation réelle deux méthodes :
black box s’introduire dans le système sans aucune connaissance préalable de celui-ci (situation réelle) white box s’introduire dans le système en ayant connaissance de l’ensemble du système (éprouver au maximum le système)
Validation d’une politique de sécurité
test d’une politique de sécurité
se fait avec l’accord de la hierarchie
le propriétaire du système doit donner une autorisation
dégâts possibles sur le système
permet de sensibiliser le personnel ne permet pas de garantir la sécurité du système gestion des incidents que faire après une attaque ?
obtention de l’adresse du pirate et riposte ?
extinction de l’alimentation de la machine ?
débranchement de la machine du réseau ?
réinstallation du système ?
plan de continuité de l’activité
Gestion de la continuité d’activité définition des responsabilités (à l’avance)
constitution de preuves sur l’attaque ( en cas d’enquête judiciaire) datation de l’intrusion (degré de compromission de la machine) confinement de la compromission (éviter la propagation) sauvegarde (comparaison des données du système avec la sauvegarde) mise en place d’un plan de repli (continuité de service) plan de continuité de l’activité
politique de sauvegarde
définition des parties du SI à sauvegarder
disponibilité des sauvegardes
politique des supports de sauvegarde
organisation des sauvegardes
replication sur un site distant
outil de simulation ()
Formalisation de politiques de sécurité
Règlement de sécurité a pour objectif de définir les actions que les agents ont :
la permission
l′obligation
l′interdiction
de réaliser
2 types de contraintes
contraintes fonctionnelles : s’appliquent aux agents lorsqu’ils effectuent des actions portant sur des objets contraintes organisationnelles : s’appliquent aux agents lorsqu’ils interagissent avec d’autres agents
Contrainte fonctionnelle : règle de la forme :
Un agent a
la permission
l′interdiction
l′obligation
de faire telle action
connaˆıtre telle information
nécessité de modéliser les concepts :
de permission
d’obligation
d’interdiction
Formalisation de politiques de sécurité
Exemple de règles de politique de sécurité :
R1 : Any agent playing the role User is permitted to read any
public file
R2 : Any agent playing the role User is permitted to write his
own public file
R3 : Any agent playing the role User is forbidden to
downgrade a file
Formalisation de politiques de sécurité
Représentation formelle de politiques de sésurité : approches
logiques :
représentation formelle : ensemble de formules raisonnement : vérification de cohérence, inférence logique classique (logique des prédicats LPr) mise en oeuvre du raisonnement : résolution implantation : programmation logique logiques modales mise en oeuvre du raisonnement : tableaux sémantiques implantation : systèmes dédiés (FaCT, · · ·)
Logique des prédicats (rappel)
Le langage de logique des prédicats
Vocabulaire
un ensemble infini dénombrable de symboles de prédicats ou prédicats (prédicats d’arité 0 : propositions) un ensemble infini dénombrable de symboles fonctionnels ou fonctions (fonctions d’arité 0 : constantes 0 ou F ou ⊥ pour
Faux et 1 ou V ou ⊥ pour Vrai)
un ensemble infini dénombrables de variables
les connecteurs : ¬, ,∧, ∨, →, ↔ les quantificateurs ∀, ∃
Logique des prédicats (rappel)
Définitions terme
x une variable , f un symbole fonctionnel est un terme
si t1, · · · ,tn sont des termes alors f (t1, · · · ,tn) est un terme atome
si t1, · · · ,tn sont des termes et P est un prédicat alors
P(t1, · · · ,tn) est un atome formules bien formées de la logique des prédicats :
A → B, A ↔ B sont des formules
Système formel de la logique des prédicats les axiomes
soit A, B, C des formules de LPr, x une variable et t un terme, D une formule n’ayant pas x pour variable libre
A1) (A → (B → A))
A2) ((A → (B → C)) → ((A → B) → (A → C)))
A3) ((¬ A → ¬ B) → (B → A))
A4) (∀x A(x) → A(t))
A5) ((D → B) → (D → ∀x B))
Déduction
Soit B une formule de LPr et H1, · · · , Hn des hypothèses
Une déduction de B à partir des hypothèses H1, · · · , Hn
H1, · · · , Hn ⊢ B
est une suite de formules F1, · · · , Fi
, Fn telle que :
Fn = B
et Fi, 1 ≤ i < n est :
soit une des hypothèses H1, · · · , Hn
soit un axiome
soit obtenue par l’application de règles de déduction à partir de
formules Fj, j < i
sémantique de la logique des prédicats
interprétation : I = (D, Ic , Iv ) o`u
D ensemble non vide, domaine d’interprétation
Ic la fonction :
D
n → D Dm → {0, 1}
f → Ic (f ) P → Ic (P)
Iv la fonction :
Var → D
x → Iv (x)
interprétation d’une formule de la logique des prédicats
A une formule de LPr, association d’une valeur de vérité I(A) à A
si x est une variable libre alors I(x) = Iv (x)
I(f (t1, · · · ,tn)) = (Ic (f ))(I(t1), · · · , I(tn))
I(P(t1, · · · ,tm)) = (Ic (P))(I(t1), · · · , I(tm))
si A et B sont des formules alors ¬A, A ∧ B, A ∨ B, A → B,
A ↔ B s’interprètent comme dans la logique propositionnelle
si A est une formule et x une variable alors I(∀x A) = 1 si Ix/d
(A) = 1 pour tout élément d ∈ D
si A est une formule et x une variable alors I(∃x A) = 1 si
Ix/d (A) = 1 pour au moins un élément d ∈ D
quelques définitions
Soient A ∈ LPr B ∈ LPr et F ⊂ LPr
A est une tautologie , |= A, si pour toute interprétation I,
I(A) = 1
B est une conséquence de A si pour toute interprétation I,
I(A) = 1 alors I(B) = 1, on écrit A |= B
B est une conséquence de F si pour toute interprétation I, tq
∀A ∈ F, I(A) = 1 alors I(B) = 1, on écrit F |= B
quelques définitions (suite)
Soient A ∈ LPr B ∈ LPr et F ⊂ LPr
A est satisfaisable s’il existe une interprétation I tq I(A) = 1
F est satisfaisable s’il existe une interprétation I tq ∀A ∈ F,
I(A) = 1
A est insatisfaisable ou incohérente si pour toute interprétation
I, I(A) = 0
F est insatisfaisable si pour toute interprétation I, ∃A ∈ F tq
I(A) = 0
Formalisation de politiques de sécurité traduction de l’ensemble des règles en F un ensemble de formules de LPr
détermination des prédicats choix des prédicats pour les permissions, obligations, interdictions
représentation des contraintes d’intégrité test de la cohérence traduction de F en un programme logique P test de la cohérence de P avec un moteur d’inférence (par exemple gnu-prolog)
Formalisation de politiques de sécurité
exemple : règle R1
Any agent playing the role User is permitted to read any public file prédicats unaires : File, Public prédicats binaires : Play, Permitted read
constante : User
Formule de LPr
∀f ∀A File(f ) ∧ Public(f ) ∧ Play(A,User) → Permitted read(A, f )
Exemple de contrainte d’intégrité :
∀f ∀A Permitted read(A, f ) ↔ ¬Forbidden read(A, f )
...
Formalisation de politiques de sécurité
Le langage de logique modale propositionnelle
Vocabulaire
un ensemble infini dénombrable de propositions
les constantes : 0 (Faux) et 1 (Vrai)
les connecteurs : ¬, ,∧, ∨, →, ↔
les modalités : , ⋄
Définitions
formules bien formées de la logique modale propositionnelle :
¬ A, A∧B, A∨B, A → B, A ↔ B sont des formules
Système formel de la logique modale propositionnelle (système K)
les axiomes
soit A, B, C des formules de la logique modale propositionnelle
A1) (A → (B → A))
A2) ((A → (B → C)) → ((A → B) → (A → C)))
A3) ((¬ A → ¬ B) → (B → A))
O
...
K-dérivation (déduction)
F : une formule modale, Γ : un ensemble de formules modales
une K-dérivation de F à partir de Γ est une séquence de formules se terminant par F, dont chaque formule est :
soit une axiome
soit un membre de Γ
soit obtenu par l’application des règles de substitution, de modus ponens ou de nécessité
une K-preuve de F est une K-dérivation de F à partir de ∅ : ⊢ F
Système formel K : formé à partir des axiomes, A1, A2, A3, K
Système formel KT : formé à partir des axiomes, A1, A2, A3, K
et de l’axiome de la connaisance T) : A → A
Système formel KT4 ou S4 : formé à partir des axiomes, A1,
A2, A3, K, T et de l’axiome d’introspection positive 4) :
A → A
Système formel KT45 ou S5 : formé à partir des axiomes, A1,
A2, A3, K, T, 4 et de l’axiome d’introspection négative 5) :
⋄ A → ⋄ A
Odi
sémantique de la logique modale propositionnelle
sémantique des “mondes possibles”
une formule modale évaluée dans un “univers” de mondes possibles
une relation d’accessibilité lie les mondes possibles entre eux
A est vraie dans un monde possible ω si A est vraie dans tous les mondes possibles accessibles à partir de ω
⋄A est vraie dans un monde possible ω si A est vraie dans au moins un monde possible accessible à partir de ω
Exemple 1 : on lance une pièce de monnaie
p : ”on obtient PILE” f : ”on obtient FACE”
p est possible f est possible
p ∨ f est nécessairement VRAI
p ∧ f est impossible : nécessairement FAUX
sémantique : définitions
système : paire (W, R) o`u W est l’ensemble des interprétations du langage et R est une relation binaire sur W
ω, ω′ ∈ W, ωRω′ : ω′
est accessible à partir de ω
valuation : application v de W × P dans {0, 1} qui associe une
valeur de vérité v(ω, p) à la variable p dans l’interprétation ω modèle : triplet M = (W, R, v) o`u (W, R) est un système et v une valuation
notation : M,ω |= F : F est vraie dans le monde possible ω pour le modèle M
définitions
Soit M = (W, R, v) un modèle, la relation de conséquence est définie par :
M, ω |= p ssi v(ω, p) = 1
M, ω |= ⊤
M, ω 6|= ⊥
M, ω |= ¬A ssi M, ω 6|= A
M, ω |= A → B ssi M, ω 6|= A ou M, ω |= B
M, ω |= A ∧ B ssi M, ω |= A et M, ω |= B
M, ω |= A ssi M, ω′|= A pour tout ω′ tq ωRω′
M, ω |= ⋄A ssi M, ω′|= A pour au moins un modèle ω′ tq ωRω′
une formule A est valide dans un modèle M = (W, R, v) ssi A est vraie dans tous les mondes possibles du modèle
notation M |= A
une formule A est valide dans un système (W, R) ssi A est vraie dans tout modèle M = (W, R, v)
notation (W, R) |= A
une formule A est valide (ou est une tautologie ), ssi A est vraie dans tout système (W, R)
notation |= A
Exemple 2 : on lance deux pièces de monnaie 1 et 2
M, ω1 |= p1 M, ω2 |= p1 M, ω3 6|= p1
M, ω1 |= (p1 ∨ p2) M, ω2 6|= (p1 ∨ p2)
M, ω2 |= ♦(p1 ∨ p2)
il y a une infinité de logiques modales qui se comportent plus ou moins bien :
K : logique modale la plus faible, formule caractéristique :
(A → B) → (A → B)
T : systèmes réflexifs, R est réflexive, formule caractéristique :
A → A
K4 : systèmes transitifs, R est transitive, formule
caractéristique :
A → A
Odile
S4 : systèmes réflexifs et transitifs, R est réflexive et transitive
KB : systèmes symétriques, R est symétrique, formule
caractéristique :
A → ⋄ A
B : systèmes réflexifs et symétriques, R est réflexive et
symétrique
S5 : systèmes réflexifs, symétriques et transitifs R est une relation d’équivalence, formule caractéristique :
¬A → ¬A
Odi
résultats de correction et de complétude le système formel K
théorème (de correction) : soit A une formule modale, si ⊢ A
alors |= A
(les formules qui sont des théorèmes du système K sont des tautologies pour la classe K)
théorème (de complétude) : soit A une formule modale, si |= A
alors ⊢ A
résultats de correction et de complétude système formel T
théorème : A → A est une tautologie ssi R est réflexive système formel S4
théorème : A → A est une tautologie ssi R est transitive système formel S5
théorème : ¬A → ¬A est une tautologie ssi R est euclidienne
Odile
quelques résultats de décidabilité
définition : une logique modale L possède la propriété de modèle
fini si pour toute formule A qui n’est pas valide dans L , il existe un modèle fini dans lequel A est falsifié proposition : si une logique modale L possède une procédure de preuve et la propriété de modèle fini alors L est décidable théorème : K, T, S4, S5 sont décidables
Logique Déontique Standard (SDL)
G von Wright 1951 : introduction des modalités O, P et F
O : obligation
P : permission
F : interdiction
définitions : soit A une formule propositionnelle
F A =def O ¬A
P A =def ¬F A
P A =def ¬O ¬A
Logique Déontique Standard (SDL)
Logique modale de type KD :
Axiome K : (O(A → B) → (O A → O B))
Axiome D : O A → ¬O ¬A
Logique Déontique Standard est décidable
Logique Déontique Standard (SDL) représentation formelle d’une politique de sécurité raisonnement
vérification de cohérence d’une politique de sécurité inférence interopérabilité de politiques de sécurité
Des systèmes performants basés sur la méthode des tableaux sémantiques
LoTREC
TWB
KSAT
FaCT
Méthode des tableaux sémantiques
formules modales : préfixées par des étiquettes qui “nomment” le monde dans lequel les formules sont supposées satisfaites. formule préfixée : σ F (σ est le préfixe)
σ0.σ1 : préfixe obtenu par concaténation des préfixes σ0 et σ1
σ.n : la suite σ suivie de n ( n entier)
σ.n nomme un monde accessible par l’un des mondes nommé par σ.
construction d’une preuve de F : construction d’un arbre dont la racine est étiquetée par la formule préfixée 1 ¬F les noeuds sont étiquetés par des formules préfixées les descendants de noeuds sont produits soit par des règles d’expansion (prolongation, ramification, double négation, nécessité, possibilité)
...
F : une formule de la logique modale.
F a une preuve par tableaux sémantiques si le tableau sémantique pour 1 ¬F est fermé un tableau sémantique est fermé (ou clos) si toutes ses branches sont fermées. une branche d’un tableau est fermée (ou close) si les formules préfixées σ F et σ ¬F apparaissent dans la branche
...
Exemple de formalisation en logique déontique SDL.
: pr édicats unaire : File, Public, Secret, Old Passwd, Acces System, Change Passwd
: pr édicats binaire : Play, Owner, Passwd, Cleared, Login, Read, Write, Downgrade
