Julien Thomas - Site de thèse : 2007 à 2011 - TELECOM Bretagne
french english

Formalisation des ECA rules, validation du modèle, preuves par systèmes d'inférence

Informations

Comme indiqué dans l'annexe « Modélisations en B - Analyse de propriétés de sécurité dans les ECA rules », les preuves en B sont limitées étant donné la complexité de celles-ci et la modélisation choisie. Afin de valider nos propositions, nous présentons donc dans ce document notre analyse à partir de « systèmes d'inférence ».

Notre approche est la suivante : afin de prouver la satisfaction de confidentiality, nous définissons progressivement des invariants nous permettant à la fin de prouver causalité, tel que décrit par l'invariant INV13.

Hypothèses générales

Preuve de la transitivité de relation inf_equal_level : INV1

Statut de la preuve :

Afin d'assurer la transitivité de la relation, nous avons définis l'invariant INV1 suivant :

∀ (level1,level2,level3).((level1:LEVELS & level2:LEVELS & level3:LEVELS) =>  ( 
	inf_equal_level(level1, level2) = TRUE & inf_equal_level(level2, level3) = TRUE ) =>  
	(inf_equal_level(level1, level3) = TRUE ))
ou encore 
∀ (level1,level2,level3).((level1:LEVELS & level2:LEVELS & level3:LEVELS) => (
	 inf_equal_level(level1, level3) = FALSE & inf_equal_level(level1, level2) = TRUE ) => 
	(inf_equal_level(level2, level3) = FALSE ))

À partir du modèle et d'AtelierB, la majeur partie des obligations de preuves (P.O.) associées ont été prouvées. Seule les opérations set_inf_level et set_equal_level sont à étudier, l'initialisation de inf_equal_level étant prouvée par construction.

Afin de valider l'invariant, plusieurs solutions sont possibles. La première serait de définir l'invariant INV1 au niveau de la machine Policy. Cette solution est la plus logique étant donné que Policy modifie explicitement le prédicat inf_equal_level. Dans notre cas, nous avons définis et prouvés cet invariant au niveau de la machine Causality. La raison est que nous avons besoin de cet invariant uniquement pour la machine Causality et donc nous avons définis celui-ci dans la machine concerné. Cependant, cela ne change aucunement la validité de la preuve si l'invariant était statué au niveau de la machine Policy, en supposant que l'invariant INVα (définie ci-dessous) soit également statué et donc prouvé dans l'ensemble des machines parentes de Policy (ce qui demanderait donc toutefois des preuves supplémentaires).

Suite à notre choix, la preuve de INV1 repose sur la méthode set_{inf,equal}_level(lvl1,lvl2) de Causality. Afin d'éviter de violer l'invariant INV1, deux solutions sont possibles :

Nous avons considéré dans notre cas la deuxième solution. Ainsi, la satisfaction de INV1 repose sur l'assertion de l'invariant INVα présenté ci-dessous et la preuve que INVα est suffisant pour prouver INV1. L' invariant INVα que nous avons spécifié est le suivant :

Pour prouver la satisfaction de INV1, nous avons alors considéré les cas suivants, sachant que l'on rajoute la relation inf_equal_level(lvl1,lvl2) et INV1p fait référence à INV1, avant l'opération :

Politique de sécurité – contrôle d'accès

La politique de sécurité étant associé aux relations fun_can_read, fun_can_write et fun_can_delete, comme spécifié dans le mémoire, les invariants permettant de spécifier la politique de contrôle d'accès sont les suivants :

∀( subject,predicate,lvl)
    .((predicate:DATABASE & lvl: LEVELS &  subject:USERS) => (
	( fun_can_read(subject,predicate,lvl)=TRUE <=>
		inf_equal_level(classification_level(predicate),lvl) = TRUE) &
	( fun_can_write(subject,predicate,lvl)=TRUE   <=>
		inf_equal_level(lvl,classification_level(predicate)) = TRUE) &
       	 (fun_can_delete(subject,predicate,lvl)=TRUE <=>
		(equal_level(lvl,classification_level(predicate)) = TRUE))))

Invariants sur le machine Causality

Au niveau de la machine Causality, nous avons spécifié plusieurs invariants non prouvés par l'AtelierB. Ceux-ci concernent les effets d'une transaction sur la base de données. Une transaction est définie sur USERS*ACTIONS_EMPTY * DATABASE*LEVELS telle qu'un action est soit une action valide, soit l'opération nulle (pas d'action).

A partir de cette observation, nous avons définis les invariants suivants. Il est à noter cependant que les preuves sur INV4 et INV5 ne sont pas présentées, étant donnés qu'elles sont similaires à INV2 et INV3, respectivement.

Invariant INV2 : résultat d'une action haut niveau sur les faits (insert)

Étant donnée notre politique de sécurité, il est possible d'assurer l'invariant INV2 suivant, qui considère les conséquences d'une action haut niveau et plus spécifiquement (C1) sur les faits. Cet invariant atteste qu'il est impossible d'engendrer une insertion bas niveau à partir d'une action haut niveau quelconque. 

 ((causality_processing = 2) or (causality_processing = 3)) =>
	(inf_equal_level(classification_level_transac(transac1_tmp),level_inv)= FALSE) =>
		∀(item).((item:database1_tmp and item notin database1) =>
		inf_equal_level(classification_level(item), level_inv)=FALSE)

La preuve de la satisfaction de INV2 repose sur les points suivants. Nous partons premièrement du postulat suivant : l'objet item de transac1_tmp est associée à une action exécutée au niveau de sécurité lvl_tr (classification_level_transac(transac1_tmp)) tel que inf_equal_level(lvl_tr, lvl_inv) = FALSE. À noter que dans le cas d'une lecture, nous avons seulement besoin de l'invariant formulé ci-dessus pour raisonner, étant donné que INV2 n'est pas affecté par cette action unitaire

Cette action pouvant engendrer d'autres actions, il nous a ensuite fallut considérer la fermeture transitive sur les règles actives, ceci par une preuve récursive.

Invariant INV3 : résultat d'une action haut niveau sur les non-faits (prédicats non présents)

Étant donnée notre politique de sécurité, il est possible d'assurer l'invariant INV2 suivant, qui considère les conséquences d'une action haut niveau et plus spécifiquement (C2) sur les non faits.

((causality_processing = 2) or (causality_processing = 3)) =>  
	(inf_equal_level(classification_level_transac(transac1_tmp),level_inv)= FALSE) =>  
		∀(item).((item:database1 and item notin database1_tmp) =>
			inf_equal_level(classification_level(item), level_inv)=FALSE)

Les preuves sont similaires à INV2 excepté que l'on considère fun_can_delete, non fun_can_write.

Invariants INV4 et INV5 : cas de la deuxième base de données

Les preuves sont similaires à INV2 et INV3, pour database2 et database2_tmp.

Invariants sur la machine Causality_event

Explications sur la raison de la séparation des invariants

Plusieurs raisons peuvent justifier notre choix de séparer les invariants entre les machines Causality et Causality_event. Bien qu'infructueuse étant donné la complexité de certains invariants de Causality, le premier objectif fut de définir dans Causality les invariants essentiels (INV1 à INV5), sur lesquels reposent fortement les invariants restants. Cela nous permet ainsi de définir une hiérarchie des invariants et de les prouver progressivement. Bien que nous n'ayons pas pu prouver les invariants avec AtelierB, nous conservons cette logique. Ce premier objectif rejoint également le second : en séparant les invariants, nous diminuons les PO générées par AtelierB et donc essayer d'accélérer le processus de génération mais aussi d'analyse des preuves. Enfin, les invariants définis dans Causality nous permettent de prouver que notre politique de sécurité est satisfaite, telle que nous l'avons définie. Les invariants de Causality_event sont donc ceux nous permettant de prouver que notre politique de sécurité permet d'assurer la propriété de Confidentialité via Causalité.

Non interférence pour lvl_invariant et les niveaux de sécurité inférieurs

transac2_tmp et lvl_invariant ou un niveau de sécurité inférieur (INV6)

(causality_processing = 3) =>
	(inf_equal_level(classification_level_transac(transac2_tmp), level_inv)= TRUE ) &
	¬(operation_transac(transac2_tmp)  = empty) =>
		∀(item).((item:database2_tmp & inf_equal_level(classification_level(item), level_inv))
		= TRUE => item:database1_tmp)

Cependant, ce théorème repose sur un modèle trop contraignant. En effet, rien n'oblige nos deux bases à se comporter d'une manière similaire lors des situations à choix valides multiples. On ne peut pas par exemple empêcher la prise en compte de niveaux de sécurité différents sur EventCall, dans le cas des deux bases (e.g. lvl_do pour l'un, lvl_2 | inf_equal_level(lvl_2,lvl_do) =FALSE pour l'autre). INV3 et INV9 sont alors violés. Pour éviter cela, soit le niveau est fixé (à lvl_do) ou alors on laisse l'indéterminisme et fixe toutefois la prise de décisions via des tampons mémoires réinitialisés à evolv3.

Implémentation

Nous considérons ici le cas des tampons de mémoire. Afin de prouver INV6, nous avons considéré l'implémentation suivante :


ECA_EventCall: action --> event: lvl_event_X 
ANY lvl_event_delete WHERE lvl_event_delete:LEVELS  &
	(subject, action, predicate,lvl_do) ∈ dom(decision.get_eventLevel) =>
		lvl_event_delete = decision.get_eventLevel(subject,action,predicate,lvl_do) & 
	(subject,action,predicate,lvl_do) ∉ dom(decision.get_eventLevel) =>
		inf_equal_level(lvl_do,lvl_event_delete) = TRUE
ECA_EventAction: event --> ECA action: level_event_action 
ANY var2, lvl_event_action WHERE lvl_event_action:LEVELS &
	var2 = get_predicate_insert(subject_event, action, predicate,lvl_event)  &
	(subject, action, predicate,lvl,subject_event, insert,...) ∈ dom(decision.get_ECAactionLevel) =>
		 lvl_event_action = decision.get_ECAactionLevel(...) &
	(subject, action, predicate,lvl, subject_event, insert,...) ∉ dom(decision.get_ECAactionLevel)  =>
		inf_equal_level(lvl_event,lvl_event_action) = TRUE  
        THEN        
            decision.set_all(subject, action, predicate,lvl,subject_event, insert, var2, ...)

transac1_tmp et lvl_invariant ou un niveau de sécurité inférieur (INV8)

inf_equal_level(classification_level_transac(transac1_tmp), level_inv)= TRUE 
& ¬(operation_transac(transac1_tmp)  = empty) =>
	inf_equal_level(classification_level_transac(transac2_tmp), level_inv)= TRUE

Databases indistinguishability (INV11 & INV12)

(INV11)
∀(item).(item: database1 & inf_equal_level(classification_level(item), level_inv)= TRUE) => (item:database2)

Situations à considérer : INV9 & INV10

(INV9)
(inf_equal_level(classification_level_transac(transac1_tmp), level_inv)= TRUE & 
operation_transac(transac1_tmp)  = empty) =>
	inf_equal_level(classification_level_transac(transac2_tmp), level_inv)= TRUE
		& (operation_transac(transac2_tmp)  = empty) 
	or inf_equal_level(classification_level_transac(transac2_tmp), level_inv)= FALSE

Preuves

cas a --> inf_equal_level(classification_level_transac(transac1_tmp), level_inv)= TRUE
cas a1 --> operation_transac(transac1_tmp) = empty: database1 n'est pas modifié
cas a2 --> operation_transac(transac1_tmp) /= empty
cas b --> inf_equal_level(classification_level_transac(transac1_tmp), level_inv) = FALSE

Causalité (INV13)

Soit database1 une base de données tels que tout utilisateurs user à l'origine d'une requête satisfait inf_equal_level(clearance_level(user), level_inv). chaque requête initiale est donc émise à un niveau de sécurité l tel que inf_equal_level(l, level_inv). Soit database2 une base de donnée quelconque.

Nous disons ensuite que (item,value) appartient à knowledge(user), si fun_can_read(item) (politique de sécurité) ou item est une condition associée à une action visible pour user. (closure(user)). Causalité est alors satisfaite si 

∀(user: USERS).(inf-equal-level(clearance-level(user), level-inv) = TRUE => 
 knowledge(user)_{database1} = knowledge(user)_{database2}

Preuve de la satisfaction de Causality

preuve a: fun_can_read(item) 

D'après INV11 et INV12, ∀(item).(fun_can_read(item) => (item, valueof(item)) ∈  knowledge(user))

preuve b: item: closure(user)

Représentation des preuves sous forme de systèmes d'inférences

Pour simplifier l'analyse des preuves, nous avons également formaliser celles-ci en utilisant des arbres de preuveset donc des systèmes d'inférences. Ceux-ci sont disponibles dans le mémoire et les annexes associées. Voir la page Mon Mémoire.

«Design-by-assumption works as long as assumptions hold. Assumptions are shortcuts to useful efficiencies, provided they are not violated. »
David S. Isenberg

«If the kernel is not evaluated to an MLS-capable protection profile, MLS features cannot be trusted regardless of how impressive the demonstration looks.»
J. Davidson

DGA CNRS

Valid XHTML 1.0 Strict Valid XHTML 1.0 Strict

http://www.julienthomas.eu/