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

Modélisations en B - Politiques de déclassification

Information

Vous trouverez sur cette page des informations sur la modélisation en B des principes de déclassifications mis en avant dans mes articles.

Modèle de dépendances entre les machines

Comme indiqué dans le mémoire, afin de valider nos travaux sur la modélisation de propriétés associées à la notion de déclassification, nous avons formalisé nos travaux en B. Les dépendances entre les différents composants du projet, présentés dans l'article Modeling and Controlling Downgrading Operations in Information Systems, sont présentées dans le schéma suivant. Le schéma présente les dépendances pour le modèle Bell & La Padula mais ceux des modèles DAC et RBAC sont proches (seule la machine BLPPolicy est remplacée par respectivement DACPolicy et RBACPolicy).

Modèle de dépendances entre les machines

Machines Principales

Comme indiqué dans le mémoire, ce projet a pour but d'illustrer la définition d'une politique de déclassification. L'interface finale principale est donc celle spécifiée dans Environment.mch. Cependant, le modèle sous-jacent lié à la politique de sécurité est également important afin de mettre en évidence les propriétés de sécurité considérées ou exprimables dans le modèle. Les deux interfaces seront donc présentées dans ce rapport.

Politique de sécurité

La politique de sécurité est définie dans la machine Policy.

Tout d'abord, elle repose sur les machines sous-jacantes Metadata et Model :

Afin de pouvoir exprimer des politiques de sécurité concrètes et les tester avec le projet Prob, la machine Policy a été étendue (et non raffinée) comme suit :

Politique de déclassification

La politique de déclassification est gérée en surcouche de la politique de sécurité. Elle étend donc celle-ci pour définir les critères associées à l'évolution de prédicats précédemment supposés statique (principe de tranquillité), lorsque l'on considère les modèles de contrôle d'accès standard. Plus exactement, elle définit la politique de sécurité associée à ces opérations de déclassification.La politique de déclassification est gérée en surcouche de la politique de sécurité. Elle étend donc celle-ci pour définir les critères associées à l'évolution de prédicats précédemment supposés statique (principe de tranquillité), lorsque l'on considère les modèles de contrôle d'accès standard. Plus exactement, elle définit la politique de sécurité associée à ces opérations de déclassification.

Interface finale

La dernière machine « principale » est Environment.mch, laquelle est l'interface à utiliser dans le simulateur ProB en tant que point d'entrée. Elle instancie donc les différentes variables (SETS) et proposent (définies ou étend) les méthodes nécessaires à l'utilisation du système.

/* Environment
* Author: julien
* Creation date: jeu. juil. 30 2009
*/
MACHINE
    Downgrading_event
    
SETS
    USERS={alice,bob,carol,eve,mallory,nestor};
    ROLES={role_alice,role_bob,role_carol,role_eve,role_mallory, role_nestor};
    LEVELS={SD_LEVEL, TSD_LEVEL, CD_LEVEL, UNCLASSIF_LEVEL};
    OBJECTS={object1,object2,object3,object4,object5};
    CONTEXTS; 
    PROCESS
 
SEES
    Constants
    
PROPERTIES
    SD_LEVEL:LEVELS & TSD_LEVEL:LEVELS & CD_LEVEL:LEVELS & SD_LEVEL /= TSD_LEVEL
    & CD_LEVEL /= TSD_LEVEL & SD_LEVEL/= CD_LEVEL 

VARIABLES
    user_observe,object_observe,role_observe,result
    
CONCRETE_VARIABLES
    users, objects, roles
    
INCLUDES down.Downgrading(USERS, OBJECTS, CONTEXTS, LEVELS, ROLES,PROCESS)
    
...

OPERATIONS

    /* *************************
	environment
    ************************* */

    createUser = PRE  not(USERS - users = {})
    THEN ... END;
    
    createObject(owners) = PRE not(OBJECTS - objects = {}) & owners : POW1(users)
    THEN ... END;
    
    createRole = PRE  not(ROLES - roles = {})
    THEN ... END;
    
    /* *************************
	admin operations 
    ************************* */

    setEmpower(user, role) = PRE
        role: roles & user : users & role /:down.pol.empower(user)
    THEN ... END;
    
    setInf_levelEnv(lvl1,lvl2) = PRE
        lvl1:LEVELS & lvl2:LEVELS
    THEN ... END;
    
    setRoleLevelEnv(role, level,rig) = PRE
        role: roles & level : LEVELS & rig: RIGHTS
    THEN ... END;
    
    setAccessEnv(issuer, role, object, rig) = PRE
        issuer: users & rig : RIGHTS  & role: roles & object : objects
    THEN ... END;
    
    
    set_trust(obj,userReq,userDest,action, boo) = PRE
        obj: objects & userReq:users & userDest:users & action:RIGHTS  & boo:BOOL
    THEN ... END ;

    setTrustedPath(path)  = PRE
        path: down.pol.execution_path
    THEN ... END;

    /* *************************
	test
    ************************* */

    isAccessEnv(user, object, rig) = PRE
        user: users & rig : RIGHTS  &     object : objects
    THEN ... END;
    
    /* *************************
	declassification
    ************************* */

    downgrade_automatic(user1,obj,user2) =
    PRE
        user1 : users & user2 : users &  obj : objects
        /* user2 should be an active user, which means (global req.) at least one role empowered in */
        & card(down.pol.empower(user2)) > 0
    THEN ... END;
    
    downgrade_trust(issuer,obj,user2)  =
    PRE
       issuer : users & user2 : users &  obj : objects
        /* user2 should be an active user, which means (global req.) at least one role empowered in */
        & card(down.pol.empower(user2)) > 0
    THEN ... END;

END

Réflexion sur les résultats

La première réflexion sur cette modélisation repose sur la modélisation elle-même et les notions associées. En effet, à partir de ce modèle, nous avons pu mettre en évidence les différentes propriétés nécessaire à la bonne spécification d'une politique de déclassification. Ces notions sont présentées dans le mémoire, chapitre 3, section 3.5 :

Deuxièmement, nous avons à partir de ce modèle présenté une abstraction des éléments de configurations de la politique de sécurité (Policy.mch, Metadata.mch) et de la politique de déclassification (Downgrading.mch) :

Troisièmement, bien que l'évaluation de la politique de sécurité via l'outil ProB fut impossible (boucle infinie due probablement au nombre important de possibilités sur les opérations, après plusieurs actions), nous avons également construit un logiciel pouvant gérer la configuration des différents paramètres du système et donc montrer la possiblité d'en concevoir un.

État des preuves

Petite légende :

Modèle Bell & La Padula (98 %)

Component		TC	POG	nPO	nUN	%Pr	B0C
BLPPolicy		OK	OK	18	6	66	-
Remaining proof status (Afficher/ Cacher) 
BLPPolicy_event		OK	OK	8	0	100	-
BLPPolicy_i		OK	OK	1016	7	99	-	
Constants		OK	OK	0	0	-	-
Downgrading		OK	OK	5	0	100	-
Downgrading_event	OK	OK	28	0	100	-
Downgrading_i		OK	OK	34	5	85	-
Metadatas		OK	OK	37	0	100	-
Metadatas_event		OK	OK	0	0	-	-
Metadatas_i		OK	OK	117	1	99	-
Model			OK	OK	25	0	100	-
Model_event		OK	OK	0	0	-	-
Model_i			OK	OK	160	1	99	-
Policy			OK	OK	31	11	64	-
Remaining proof status (Afficher/ Cacher)
  • addUser#PO3: considered as true (15/01/2010)
  • addUser#PO4: considered as true (15/01/2010)
  • addRole#PO2: considered as true (15/01/2010)
  • addObject#PO4: considered as true (15/01/2010)
  • addObject#PO5: considered as true (15/01/2010)
  • updateKnowledge#PO3: considered as true (15/01/2010)
  • updateKnowledge#PO4: considered as true (15/01/2010)
  • setEmpower#PO3: considered as true (15/01/2010)
  • setEmpower#PO4: considered as true (15/01/2010)
  • setAccess#PO1: considered as true (15/01/2010)
  • setAccess#PO2: considered as true (15/01/2010)
Policy_event		OK	OK	0	0	-	-
Policy_i		OK	OK	643	2	99	-
Set			OK	OK	4	0	100	-
Set_seq			OK	OK	1	0	100	-
Set_seq_pow		OK	OK	2	0	100	-
tuples			OK	OK	1	0	100	-
tuples_time		OK	OK	1	0	100	-

Modèle DAC (97 %)

Component		TC	POG	nPO	nUN	%Pr	B0C
Constants		OK	OK	0	0	-	-
DACPolicy		OK	OK	12	6	50	-
Remaining proof status (Afficher/ Cacher)
  • UpdateKnowledgePolicy#PO2: considered as true (18/01/2010)
  • addUserPolicy#PO3: considered as true (18/01/2010)
  • addRolePolicy#PO3: considered as true (18/01/2010)
  • setEmpowerPolicy#PO1: considered as true (18/01/2010)
  • setEmpowerPolicy#PO2: considered as true (18/01/2010)
  • setAccess#PO1: considered as true (18/01/2010)
DACPolicy_i		OK	OK	33	2	93	-
Downgrading		OK	OK	3	0	100	-
Downgrading_event	OK	OK	24	0	100	-
Downgrading_i		OK	OK	31	5	83	-
Metadatas		OK	OK	37	0	100	-
Metadatas_event		OK	OK	0	0	-	-
Metadatas_i		OK	OK	117	1	99	-
Model			OK	OK	25	0	100	-
Model_event		OK	OK	0	0	-	-
Model_i			OK	OK	160	1	99	-
Policy			OK	OK	31	11	64	-
Remaining proof status: see Bell & La Padula 
Policy_event		OK	OK	0	0	-	-
Policy_i		OK	OK	643	2	99	-
Set			OK	OK	4	0	100	-
Set_seq			OK	OK	1	0	100	-
Set_seq_pow		OK	OK	2	0	100	-
tuples			OK	OK	1	0	100	-
tuples_time		OK	OK	1	0	100	-

Modèle RBAC (97 %)

Component		TC	POG	nPO	nUN	%Pr	B0C
Constants		OK	OK	0	0	-	-
Downgrading		OK	OK	3	0	100	-
Downgrading_event	OK	OK	24	0	100	-
Downgrading_i		OK	OK	29	5	82	-
Metadatas		OK	OK	37	0	100	-
Metadatas_event		OK	OK	0	0	-	-
Metadatas_i		OK	OK	117	1	99	-
Model			OK	OK	25	0	100	-
Model_event		OK	OK	0	0	-	-
Model_i			OK	OK	160	1	99	-
Policy			OK	OK	31	11	64	-
Remaining proof status: see Bell & La Padula 
Policy_event		OK	OK	0	0	-	-
Policy_i		OK	OK	643	2	99	-
RBACPolicy		OK	OK	26	5	80	-
Remaining proof status (Afficher/ Cacher)
  • UpdateKnowledgePolicy#PO1: considered as true (19/01/2010)
  • addRolePolicy#PO7: considered as true (19/01/2010)
  • setEmpowerPolicy#PO2: considered as true (19/01/2010)
  • setEmpowerPolicy#PO3: unknown: considered as true (19/01/2010)
  • setAccess#PO1: considered as true (19/01/2010)
RBACPolicy_i		OK	OK	102	2	98	-
Set			OK	OK	4	0	100	-
Set_seq			OK	OK	1	0	100	-
Set_seq_pow		OK	OK	2	0	100	-
tuples			OK	OK	1	0	100	-
tuples_time		OK	OK	1	0	100	-

«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/