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

Modélisations en B - Analyse de propriétés de sécurité dans les ECA rules

Information

Comme indiqué dans le mémoire, afin de valider mes travaux sur la modélisation de propriétés de sécurité dans les systèmes d'informations dynamiques, j'ai formalisé en B cette notion de comportement dynamique en se reposant sur la structure associée aux ECA rules et plus exactement le language Lactive.

Les dépendances entre les différentes machines spécifiées en B sont présentées dans la figure ci-dessous. On peut remarquer les liens suivants entre le modèle en B et le language Lactive :

Modèle de dépendances entre les machines

Project Configuration

FATB*ATB*Logic_Solver_Command:krt -a c85000d3000e100g10000h10000m10000000n130000o110400s60000t1100x5000y5500
ATB*PR*Time_Out_Auto:3
ATB*POG*Generate_Obvious_PO:FALSE
ATB*PR*Pr_3_7_compatibility:FALSE
ATB*PR*Pr_3_6_compatibility:FALSE
ATB*PR*Enable_TC_Command:FALSE
ATB*PR*Trace_User_Rules:FALSE
ATB*TC*Enable_Extended_Sees:FALSE

Machines Principales

Le but de ce deuxième projet en B fut de prouver la sécurité d'une politique de sécurité orientée confidentialité, dans des systèmes avec règles actives. Dans ce but, le modèle considère : la spécification de règles ECA, la spécification des informations de sécurité, la spécification de la politique de sécurité et l'analyse de la sécurité de la politique.

Spécification des règles ECA

Afin de proposer un modèle répondant aux besoins, plusieurs approches étaient possibles (en plus du choix du modèle). Dans notre cas, le modèle spécifié distinct et définit explicitement les notions d'actions, évènements et règles. Cela nous permet en effet de pouvoir par la suite spécifier séparément les contrôles et propriétés de sécurité. Cependant, ce choix, comme nous le verrons par la suite, aura eu plusieurs conséquences sur le projet.

La spécification des règles repose sur les machines ECA_actions, ECA_actionsHandle, ECA_EventAction et ECA_EventCall.

Dans le cas de ECA_actions, les opérations contrôlent les requètes en fonction de la politique de sécurité (fun_can_{READ,WRITE}). Toutefois, on peut remarquer que notre choix de modélisation faisant qu'il est impossible de spécifier des modifications successives (les boucles ne sont pas autorisées), nous devons également considérer des actions du type do_A1_A2 afin de pouvoir considérer les règles actives. La spécification des actions reposent sur l'appel aux méthodes de ECA_actions en fonctions de règles définies arbitrairement.

MACHINE ECA_actions
SEES ECA_Parameters,ECA_policy
OPERATIONS
    rep,dbinst_out <-- DO_select(subject,predicate ,lvl_do,action,dbinst_in) =
    PRE  rep : RESULTS  & subject:USERS &  predicate: DATABASE & action:ACTIONS
        & lvl_do:LEVELS &  dbinst_in <: DATABASE & dbinst_out <: DATABASE
    THEN        
        IF( fun_can_read(subject, predicate,lvl_do)=TRUE)  THEN
            IF( predicate: dbinst_in ) THEN
                 rep:= YES_RESULT || add_knowledge(subject, predicate, lvl_do,TRUE)
            ELSE
                 rep:= NO_RESULT || add_knowledge(subject, predicate, lvl_do,FALSE)
            END
        ELSE  rep := SECURITY_SKIP END
    END;

    rep,dbinst_out <-- DO_delete_insert(subject,  predicate, lvl_do,
        subject2,  predicate2, lvl_do2,dbinst_in) = PRE
            subject:USERS & predicate: DATABASE & rep: RESULTS & lvl_do:LEVELS & 
            subject2:USERS &  predicate2: DATABASE &  lvl_do2:LEVELS& 
            dbinst_in <: DATABASE & dbinst_out <: DATABASE
    THEN
        IF(fun_can_delete(subject, predicate,lvl_do)=TRUE) THEN
            IF( fun_can_insert(subject2, predicate2,lvl_do2)=TRUE ) THEN
                dbinst_out := (dbinst_in - {predicate} )\/ {predicate2}
            ELSE
                dbinst_out := dbinst_in - {predicate}
            END
            || rep := YES_RESULT 
        ELSE rep := SECURITY_SKIP END
END;

Les règles de la machine ECA_EventCall conditionnent les appels aux évènements. Par exemple, l'action delete engendre l'évènement event_insert si DB_I6 est vrai et event_delete si DB_I6 est faux et DB_I7 est vrai.

MACHINE ECA_EventCall
INCLUDES ea.ECA_EventAction
...    
OPERATIONS
    rep,dbinst_out <-- do(subject, action, predicate,lvl_do, dbinst_in) = PRE
        subject:USERS & action:ACTIONS & predicate: DATABASE & rep: RESULTS &
        lvl_do:LEVELS & dbinst_in <: DATABASE & dbinst_out <: DATABASE
    THEN
        IF(action = delete) THEN
            ANY lvl_event_delete WHERE
               lvl_event_delete:LEVELS  & lvl_do = lvl_event_delete
            THEN
                /* event(lvl_event_delete) after do(lvl_do) if r ... r*/
                IF(  DB_I6:dbinst_in) THEN
                    rep,dbinst_out <-- ea.do_event_insert(subject, delete, predicate,lvl_do,
                         subject,lvl_event_delete,dbinst_in)
                ELSE
                    IF(DB_I7:dbinst_in) THEN
                       rep,dbinst_out <-- ea.do_event_delete(subject, delete, predicate,lvl_do,
                           subject,lvl_event_delete,dbinst_in)
                ...

Enfin, la spécification des évènements repose sur la machine ECA_EventAction. Celle-ci contient les règles associées aux évènements considérées. Par exemple, l'évènement event_insert engendre un insert si les conditions DB_I10 et DB_I11 sont vraies. A noter que comme indiqué précédemment, la récursivité n'étant pas possible, les opérations appellent les méthodes do_A1_A2 si les conditions sont vraies et do_A1 sinon.

MACHINE ECA_EventAction
INCLUDES ECA_actionsHandle
...
OPERATIONS
    rep,dbinst_out <-- do_event_insert(subject,action,predicate,lvl, subject_event,lvl_event,dbinst_in) = PRE
        rep : RESULTS & subject:USERS & action:ACTIONS & predicate: DATABASE &
        lvl:LEVELS & subject_event:USERS & lvl_event: LEVELS & dbinst_in <: DATABASE & dbinst_out <: DATABASE
    THEN
        ANY var2, lvl_event_action WHERE
            var2 = get_predicate_insert(subject_event, action, predicate,lvl_event)  & lvl_event_action:LEVELS &
            lvl_event = lvl_event_action
        THEN
            /* IF t1(Z1) .... tn(Zn)  */
             IF(DB_I10:dbinst_in & DB_I11:dbinst_in) THEN
                 rep,dbinst_out <-- do_twice(subject, action, predicate,lvl,
                    subject_event, insert, var2,lvl_event_action,dbinst_in) 
             ELSE
                rep,dbinst_out <-- do(subject, action, predicate,lvl,dbinst_in)
             END
        END  END;

Spécification de la politique de sécurité

Comme précisé précédemment, le modèle a été définit dans le but de pouvoir exprimer simplement les propriétés de sécurité définies au cours de la thèse. La spécification de celles-ci consistent donc à étendre les méthodes mentionnées pour pouvoir exprimer la politique de sécurité considérée. Par exemple, les contrôles au niveau des évènements reposent sur le contrôle d'accès aux conditions et l'évolution des niveaux de sécurité. La politique de sécurité est donc spécifiée comme suit : 
 rep,dbinst_out <-- do_event_insert(subject, action,predicate,lvl,
      subject_event,lvl_event,dbinst_in) = PRE
        rep : RESULTS &  subject:USERS & action:ACTIONS & predicate: DATABASE &
        lvl:LEVELS & subject_event:USERS & lvl_event: LEVELS &  dbinst_in <: DATABASE & dbinst_out <: DATABASE
   THEN
        ANY var2, lvl_event_action WHERE
            var2 = get_predicate_insert(subject_event, action, predicate,lvl_event)  & lvl_event_action:LEVELS &
            inf_equal_level(lvl_event,lvl_event_action) = TRUE & lvl_event = lvl_event_action
        THEN
            /* IF t1(Z1) .... tn(Zn)  */
            IF(fun_can_read(subject, DB_I10, lvl_event)=TRUE &  fun_can_read(subject, DB_I11, lvl_event)=TRUE) THEN
                IF(DB_I10:dbinst_in & DB_I11:dbinst_in) THEN
                    rep,dbinst_out <-- do_twice(subject, action, predicate,lvl,
                        subject_event, insert, var2,lvl_event_action,dbinst_in) 
                ELSE
                    rep,dbinst_out <-- do(subject,action,predicate, lvl,dbinst_in)
                END
            ELSE
                rep,dbinst_out <-- do(subject, action, predicate,lvl,dbinst_in)
            END    
        END  END;

Spécification des contrôles associés à la politique de sécurité

Afin de conclure sur la spécification, la dernière étape consiste à valider la politique en s'assurant que les objets accédés le sont correctement. Pour cela, à chaque accès à une donnée, l'instruction suivante est générée : user.user_add_cond_knowledge(subject,{(Obj |-> Lvl |->Val)}) où Val est soit False, soit True.

Cette méthode est donc associée à la machine user qui assure que les informations accessibles (knowledge) soit autorisées. Il est à noter que seul le niveau de sécurité est pris en compte dans fun_can_read et que l'on a inf_equal_level(lvl_u,lvl)& clearance_level(lvl_u,subject).

 user_add_cond_knowledge(subject,set) = PRE
    subject:USERS & set: POW(DATABASE * LEVELS* BOOL) & 
    !(item,lvl, status).((item:DATABASE& lvl:LEVELS & status:BOOL &  (item|-> lvl|->status): set)=>
        fun_can_read(subject, item,lvl)=TRUE)

Dans un deuxième temps, afin de valider la sécurité du modèle, deux machines ont été ajoutées : database et causality. Ces deux spécifications ont pour but de

  1. considérer deux bases de données
  2. effectuer des actions équivalentes au niveau lvl_inv
  3. assurer que l'état final est équivalent

Ainsi, à partir des résultats, nous pouvons prouver

  1. la validation de notre politique dans l'implémentation (preuves sur la machine database)
  2. la sécurité de notre politique par rapport à la propriété de confidentialité

Interfaces finales

EventCall (show/hide)

MACHINE ECA_EventCall_event   
INCLUDES ECA_EventCall
PROMOTES ea.can_read,ea.can_write,ea.can_delete
SEES ECA_Parameters    
CONCRETE_VARIABLES result_event,rep_event 
INITIALISATION
   ...
INVARIANT
    result_event: RESULTS &  rep_event: BOOL
    
OPERATIONS

Main Operations

do_event(subject, action, predicate,lvl_do) = PRE
    subject:USERS & action:ACTIONS & predicate: DATABASE & lvl_do:LEVELS
THEN ... END;

Administration

set_inf_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_eq_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_user_level_event(user,lvl) = PRE user:USERS & lvl: LEVELS THEN... END;

set_classification_level_event(predicate, lvl) = PRE predicate:DATABASE & lvl: LEVELS THEN ... END

Policy Conslutation

can_read_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END;
    
can_write_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END ;
    
can_delete_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END
END

Transactions (show/hide)

MACHINE ECA_transactions_event
SEES ECA_Parameters
INCLUDES src.ECA_transactions
VARIABLES
    transaction_value, transactions_status, transaction_result, rep_event
INITIALISATION
    ...
INVARIANT
    transaction_value: seq(src.operations) & transactions_status: BOOL & transaction_result: RESULTS || rep_event := FALSE & rep_event:BOOL
    
OPERATIONS

Main Operations

do_transaction =  transaction_value <-- src.do_transaction;

evolv_state(transac_in) = PRE transac_in: seq(src.operations) THEN ... END;

init_transaction(user,action,item_db) = PRE 
    user: USERS & action: ACTIONS & item_db: DATABASE
THEN   ... END;

add_transaction(user,action,item_db) = PRE
    user: USERS & action: ACTIONS & item_db: DATABASE 
THEN  
    ...
END;

equal_transactions(trans1, trans2, level) = PRE
    level: LEVELS & trans1: seq(src.operations) & trans2: seq(src.operations)
THEN ... END;

Policy Administration

set_inf_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_eq_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_user_level_event(user,lvl) = PRE user:USERS & lvl: LEVELS THEN... END;

set_classification_level_event(predicate, lvl) = PRE predicate:DATABASE & lvl: LEVELS THEN ... END

Policy Conslutation

can_read_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END;
    
can_write_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END ;
    
can_delete_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END
END

Causality (show/hide)

MACHINE
    ECA_causality_event
    
SEES
    ECA_Parameters
    
INCLUDES
    ECA_causality

PROMOTES
   set_first_transaction,  set_second_transaction,
   ...
    
VARIABLES
    transaction_value, rep_event
CONCRETE_VARIABLES (inherited from ECA_causality)
    transac1,transac2
INITIALISATION
    ...
INVARIANT
    transaction_value: seq(tr1.operations) & rep_event:BOOL

OPERATIONS

Main Operations

do_transaction_event
    
init_transaction_event(user,action,item_db) = PRE
    user: USERS & action: ACTIONS & item_db: DATABASE 
THEN ... END;
    
add_transaction_event(user,action,item_db) = PRE
    user: USERS & action: ACTIONS & item_db: DATABASE 
THEN ... END;
    
create_equal_transactions(level) = PRE level:LEVELS
THEN ... END;

/*
  Operation to be called before causality(level) if level differs
*/
setLevelEquality(level) = PRE level:LEVELS
THEN ... END;

/* single step : immediate causality check */
causality(level) = PRE level:LEVELS &   ...
THEN ... END;

Policy Administration

set_inf_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_eq_level_event(lvl1,lvl2) = PRE lvl1:LEVELS & lvl2: LEVELS THEN... END;

set_user_level_event(user,lvl) = PRE user:USERS & lvl: LEVELS THEN... END;

set_classification_level_event(predicate, lvl) = PRE predicate:DATABASE & lvl: LEVELS THEN ... END

Policy Conslutation

can_read_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END;
    
can_write_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END ;
    
can_delete_event(subject,predicate,lvl) = PRE
    predicate:DATABASE & lvl: LEVELS &  subject:USERS
THEN ... END ;
END

Réflexion sur les résultats

Étant donné les choix au niveau de notre modèle, les preuves ne sont possible que pour la première étape (validation de l'implémentation). En effet, la complexité associée aux preuves fait que l'outil AtelierB est incapable de valider l'ensemble des invariants restants (Database, Causality). Cependant, il n'est pas dit qu'un changement dans la modélisation permettrait de prouver l'ensemble des invariants nécessaires. Toutefois, ce deuxième projet nous a permis de premièrement spécifier formellement l'ensemble des propriétés considérées, leur implémentations et les notions de sécurité associés. Deuxièmement, la première étape de validation nous a permis de montrer qu'il est possible d'implémenter notre politique de sécurité.

Associé à ces preuves en B, nous avons également analysé les invariants non prouvés. À partir de systèmes d'inférence (Voir le document associé), nous avons alors montré qu'il est possible de prouver ces invariants et donc de valider le fait que notre politique de sécurité assure la préservation de la confidentialité des données dans le cadre des systèmes d'information avec règles actives. Malgré le besoin d'utiliser des outils supplémentaires et non seulement l'atelierB, nous avons donc pu montrer la robustesse de notre politique de sécurité.

État des preuves

Petite légende :

| Original proofs | New model | 
__Global__ 				OK 	OK	-	-	-	-
Component				TC	POG	nPO	nUN	%Pr	B0C
Database_Predicate			OK	OK	1	0	100	-
Database_Predicate_i			OK	OK	1	1	0	-
ECA_actions				OK	OK	10	0	100	-
ECA_actions_i				OK	OK	51	42	17	-
ECA_actionsHandle			OK	OK	0	0	-	-
ECA_actionsHandle_i			OK	OK	36	3	91	-
Remaining proof status (Afficher/ Cacher)
  • do_twice#PO1: considered as true (11/02/2010)
  • set_inf_level#PO3: considered as true (11/02/2010)
  • set_eq_level#PO3: considered as true (11/02/2010)
ECA_actionsHandle_event			OK	OK	2	0	100	-
ECA_actionsHandle_event_i		OK	OK	38	10	72	-
ECA_actionsHandle_event_insecure1	OK	OK	0	0	-	-
ECA_actionsHandle_event_insecure1_i	OK	OK	36	5	86	-
ECA_actionsHandle_event_insecure4	OK	OK	0	0	-	-
ECA_actionsHandle_event_insecure4_i	OK	OK	32	14	53	-
ECA_actionsHandle_insecure1		OK	OK	0	0	-	-
ECA_actionsHandle_insecure1_i		OK	OK	25	16	36	-
ECA_actionsHandle_insecure4		OK	OK	6	6	0	-
ECA_actionsHandle_insecure4_i		OK	OK	27	17	37	-
ECA_actions_insecure1			OK	OK	18	10	44	-
ECA_actions_insecure1_i			OK	OK	32	26	18	-
ECA_causality				OK	OK	6	6	0	-
Note: required /* tr1.evolv_state(transac1_in) ||     tr2.evolv_state(transac2_in)*/ on ECA_databases_double
and /*|| evolv_states(transac1,transac2) */ on ECA_causality
Remaining proof status (Afficher/ Cacher)
  • set_inf_level#PO1: considered as true (24/02/2010)
  • set_inf_level#PO2: considered as true (24/02/2010)
  • set_eq_level#PO1: considered as true (24/02/2010)
  • set_eq_level#PO2: considered as true (24/02/2010)
  • set_classification_level#PO1: considered as true (24/02/2010)
  • set_classification_level#PO2: considered as true (24/02/2010)
ECA_causality_i				OK	OK	18	8	60	-
Note: required /* tr1.evolv_state(transac1_in) ||     tr2.evolv_state(transac2_in)*/ on ECA_databases_double
and /*|| evolv_states(transac1,transac2) */ on ECA_causality
Remaining proof status (Afficher/ Cacher)
  • causality#PO2: defined as true (24/02/2010)
  • causality#PO3: defined as true (24/02/2010)
  • causality#PO4: defined as true (24/02/2010)
  • causality#PO5: defined as true (24/02/2010)
  • causality#PO6: defined as true (24/02/2010)
  • causality#PO7: defined as true (24/02/2010)
  • all_set_inf_level#PO3: considered as true (24/02/2010)
  • all_set_eq_level#PO3: considered as true (24/02/2010)
ECA_causality_event			OK	OK	5	0	100	-
ECA_databases_double			OK	OK	17	12	29	-
Remaining proof status (Afficher/ Cacher)
  • initialisation#P01: considered as true (24/02/2010)
  • initialisation#P03: considered as true (24/02/2010)
  • all_set_inf_level#PO1: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_inf_level#PO2: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_inf_level#PO4: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_eq_level#PO1: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_eq_level#PO2: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_eq_level#PO3: considered as true (tr1 & tr2 equality) (11/02/2010)
  • all_set_eq_level#PO4: considered as true (10/02/2010)
  • all_set_classification_level#PO1: considered as true (10/02/2010)
  • all_set_classification_level#PO2: considered as true (10/02/2010)
  • all_set_classification_level#PO3: considered as true (10/02/2010)
ECA_databases_double_i			OK	OK	13	2	84	-
Note: required /* tr1.evolv_state(transac1_in) ||     tr2.evolv_state(transac2_in)*/ on ECA_databases_double
Remaining proof status (Afficher/ Cacher)
  • all_set_inf_level#PO3: considered as true (24/02/2010)
  • all_set_eq_level#PO3: considered as true (24/02/2010)
ECA_EventAction				OK	OK	2	0	100	-
ECA_EventAction_i			OK	OK	238	238	100	-
Remaining proof status (Afficher/ Cacher)
  • set_inf_level#PO3: considered as true (11/02/2010)
  • set_eq_level#PO3: considered as true (11/02/2010)
ECA_EventAction_insecure2		OK	OK	7	5	28	-
ECA_EventAction_insecure2_i		OK	OK	24	6	75	-
ECA_EventCall				OK	OK	0	0	-	-
ECA_EventCall_event			OK	OK	0	0	-	-
ECA_EventCall_i				OK	OK	76	29	61	-
Remaining proof status (Afficher/ Cacher)
  • do#PO38: considered as true (11/02/2010)
  • do#PO39: considered as true (11/02/2010)
  • do#PO40: considered as true (11/02/2010)
  • do#PO41: considered as true (11/02/2010)
  • do#PO42: considered as true (11/02/2010)
  • do#PO61: considered as true (11/02/2010)
  • do#PO62: considered as true (11/02/2010)
  • easet_inf_level#PO3: considered as true (11/02/2010)
ECA_EventCall_event_i			OK	OK	70	30	57	-
ECA_EventCall_event_insecure2		OK	OK	0	0	-	-
ECA_EventCall_event_insecure2_i		OK	OK	39	35	10	-
ECA_EventCall_event_insecure5		OK	OK	0	0	-	-
ECA_EventCall_event_insecure5_i		OK	OK	78	18	76	-
ECA_EventCall_insecure2			OK	OK	0	0	-	-
ECA_EventCall_insecure2_i		OK	OK	18	5	72	-
ECA_EventCall_insecure5			OK	OK	5	5	0	-
ECA_EventCall_insecure5_i		OK	OK	49	20	59	-
ECA_EventCall_r				OK	OK	217	52	76	-
ECA_EventDefinition			OK	OK	1	0	100	-
ECA_EventDefinition_i			OK	OK	8	3	62	-
ECA_Parameters				OK	OK	0	0	-	-
ECA_policy				OK	OK	50	22	56	-
Remaining proof status (Afficher/ Cacher)
  • initialisation#PO1: considered as true (23/02/2010) - ProB validated
  • initialisation#PO2: considered as true (23/02/2010) - ProB validated
  • >initialisation#PO5: considered as true (23/02/2010) - ProB validated
  • initialisation#PO7: considered as true (2/02/2010) - ProB validated
  • initialisation#PO9: considered as true (23/02/2010) - ProB validated
  • set_inf_level#PO5: considered as true (10/02/2010)
  • set_inf_level#PO6: considered as true (10/02/2010)
  • >set_inf_level#PO7: considered as true (10/02/2010)
  • set_inf_level#PO8: considered as true (10/02/2010)
  • set_inf_level#PO9: considered as true (10/02/2010) ((inf_equal_level(classification_level(predicate),lvl$0) = TRUE or (classification_level(predicate) = lvl1 & lvl$0 = lvl2) => func_r(subject,predicate,lvl$0) = TRUE)))
  • set_inf_level#PO10: considered as true (10/02/2010)
  • set_inf_level#PO11: unknown ((inf_equal_level(lvl$0,classification_level(predicate)) = TRUE or (classification_level(predicate) = lvl2 & lvl$0 = lvl1) => func_w(subject,predicate,lvl$0))
  • set_eq_level#PO5: considered as true (10/02/2010)
  • set_eq_level#PO6: considered as true (10/02/2010)
  • set_eq_level#PO7: considered as true (10/02/2010)
  • set_eq_level#PO8: considered as true (10/02/2010)
  • set_eq_level#PO9: unknown ((inf_equal_level(classification_level(predicate),lvl$0) = TRUE or (classification_level(predicate) = lvl1 & lvl$0 = lvl2) => func_r(subject,predicate,lvl$0) = TRUE))
  • set_eq_level#PO10: considered as true (10/02/2010)
  • set_eq_level#PO11: unknown ((inf_equal_level(lvl$0,classification_level(predicate)) = TRUE or (classification_level(predicate) = lvl2 & lvl$0 = lvl1) => func_w(subject,predicate,lvl$0) = TRUE)) )
  • set_eq_level#PO12: considered as true (10/02/2010)
  • set_eq_level#PO13: unknown ((equal_level(lvl$0,classification_level(predicate)) = TRUE or (classification_level(predicate) = lvl2 & lvl$0 = lvl1) => func_d(subject,predicate,lvl$0) = TRUE)))
  • set_classification_level#PO3: defined as true (10/02/2010)
  • et_classification_level#PO4: defined as true (10/02/2010)
  • set_classification_level#PO5: defined as true (10/02/2010)
  • set_classification_level#PO6: defined as true (10/02/2010)
  • set_classification_level#PO7: defined as true (10/02/2010)
  • set_classification_level#PO8: defined as true (10/02/2010)
ECA_policy_i				OK	OK	1895	0	100	-
ECA_transactions			OK	OK	0	0	-	-
ECA_transactions_i			OK	OK	22	9	60	-
Note: required /*  rep_tr <--do(user,action,db_item,level)  */ on evolv_state
Remaining proof status (Afficher/ Cacher)
  • evolv_state#PO2: defined as true (24/02/2010)
  • evolv_state#PO3: defined as true (24/02/2010)
  • equal_transaction#PO2: defined as true (24/02/2010)
  • equal_transaction#PO5: defined as true (24/02/2010)
  • equal_transaction#PO6: defined as true (24/02/2010)
  • equal_transaction#PO7: defined as true (24/02/2010)
  • equal_transaction#PO8: defined as true (24/02/2010)
  • easet_eq_level#PO3: considered as true (24/02/2010)
  • easet_inf_level#PO3: considered as true (24/02/2010)
  

ECA_transactionsParameters		OK	OK	0	0	-	-
ECA_transactions_event			OK	OK	335	0	100	-
Messages 				OK	OK	0	0	-	-
OperationStruct				OK	OK	0	0	-	-
Set_seq					OK	OK	1	0	100	-

__Global__ 				OK 	OK	-	-	-	-
Component				TC	POG	nPO	nUN	%Pr	B0C
Database_Predicate			OK	OK	1	0	100	-
Database_Predicate_i			OK	OK	1	1	0	-
ECA_actions				OK	OK	10	0	100	-
ECA_actions_i				OK	OK	51	42	17	-
ECA_actionsHandle			OK	OK	0	0	-	-
ECA_actionsHandle_i			OK	OK	36	3	91	-
ECA_actionsHandle_event			OK	OK	2	0	100	-
ECA_actionsHandle_event_i		OK	OK	38	10	72	-
ECA_actionsHandle_event_insecure1	OK	OK	0	0	-	-
ECA_actionsHandle_event_insecure1_i	OK	OK	36	5	86	-
ECA_actionsHandle_event_insecure4	OK	OK	0	0	-	-
ECA_actionsHandle_event_insecure4_i	OK	OK	32	14	53	-
ECA_actionsHandle_insecure1		OK	OK	0	0	-	-
ECA_actionsHandle_insecure1_i		OK	OK	25	16	36	-
ECA_actionsHandle_insecure4		OK	OK	6	6	0	-
ECA_actionsHandle_insecure4_i		OK	OK	27	17	37	-
ECA_actions_insecure1			OK	OK	18	10	44	-
ECA_actions_insecure1_i			OK	OK	32	26	18	-
ECA_causality				OK	OK	6	6	0	-
ECA_causality_i				OK	OK	18	8	60	-
ECA_causality_event			OK	OK	8	0	100	-
ECA_databases_double			OK	OK	340	0	100	-
ECA_databases_double_i			OK	OK	13	2	84	-
ECA_EventAction				OK	OK	2	0	100	-
ECA_EventAction_i			OK	OK	238	238	100	-
ECA_EventAction_insecure2		OK	OK	7	5	28	-
ECA_EventAction_insecure2_i		OK	OK	24	6	75	-
ECA_EventCall				OK	OK	0	0	-	-
ECA_EventCall_event			OK	OK	0	0	-	-
ECA_EventCall_i				OK	OK	76	29	61	-
ECA_EventCall_event_i			OK	OK	70	30	57	-
ECA_EventCall_event_insecure2		OK	OK	0	0	-	-
ECA_EventCall_event_insecure2_i		OK	OK	39	35	10	-
ECA_EventCall_event_insecure5		OK	OK	0	0	-	-
ECA_EventCall_event_insecure5_i		OK	OK	78	18	76	-
ECA_EventCall_insecure2			OK	OK	0	0	-	-
ECA_EventCall_insecure2_i		OK	OK	18	5	72	-
ECA_EventCall_insecure5			OK	OK	5	5	0	-
ECA_EventCall_insecure5_i		OK	OK	49	20	59	-
ECA_EventCall_r				OK	OK	217	52	76	-
ECA_EventDefinition			OK	OK	1	0	100	-
ECA_EventDefinition_i			OK	OK	8	3	62	-
ECA_Parameters				OK	OK	0	0	-	-
ECA_policy				OK	OK	50	22	56	-
ECA_policy_i				OK	OK	1895	0	100	-
Messages 				OK	OK	0	0	-	-
OperationStruct				OK	OK	0	0	-	-
Set_seq					OK	OK	1	0	100	-

Invariants essentiels

Policy Invariants

    
    /* logical assumptions */
    !(lvl).(lvl:LEVELS => equal_level(lvl,lvl)=TRUE) &

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

Causality Invariant

    /* causality condition on partially defined level matrice */
    !(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 ))
    /*
    avoid illegal matric: (illegal on level2 --> level3)
    level1 -/-> level3
      |       /
    level2  /
    */
    & 
    /*
    assert database equals at level_inv !! */
    level_inv:LEVELS & 
    ((causality_processing = 0) =>
        !(item).(item: database1 &  inf_equal_level(classification_level(item), level_inv)= TRUE => (item:database2 )))
    & 
    ((causality_processing = 0) =>
        !(item).(item: database2 &  inf_equal_level(classification_level(item), level_inv)= TRUE => (item:database1 )))
    /* ..end assertion */
    &

Causality Invariant: reasons for causality success

    /* reason why causality works - TMP assert 1 - evolv2 &  evolv3 
       can be also defined in EventCall || database_double
    */
    (((causality_processing = 2) or (causality_processing = 3)) =>
        ((inf_equal_level(classification_level_transac(transac1_causality), level_inv)= FALSE) =>
            (!item.((item:database1_tmp &  item /:database1) =>
                    ( inf_equal_level(classification_level(item), level_inv)=FALSE
                    )))))
    & 
    /* reason why causality works - TMP assert2 - evolv3 
       can be also defined in EventCall || database_double
    */
    ((causality_processing = 3) =>
        ((inf_equal_level(classification_level_transac(transac2_causality), level_inv)= FALSE) =>
            (!item.((item:database2_tmp &  item /:database2) =>
                    ( inf_equal_level(classification_level(item), level_inv)=FALSE
                    )))))
    & 
    /* reason why causality works - TMP assert3 - evolv3 */
    ((causality_processing = 3) =>
        (inf_equal_level(classification_level_transac(transac2_causality), level_inv)= TRUE) =>
        !item.((item:database2_tmp &  inf_equal_level(classification_level(item), level_inv)=FALSE) => item:database1_tmp ))
    & 
    /* reason why causality works - TMP assert4 - evolv3 */
    ((causality_processing = 3) =>
        (inf_equal_level(classification_level_transac(transac1_causality), level_inv)= TRUE) =>
        !item.((item:database1_tmp &  inf_equal_level(classification_level(item), level_inv)=FALSE) => item:database2_tmp ))

Proofs of causality satisfaction

coming ...

Théories utilisées

ECA_Policy.mch:

THEORY updateEquivalence IS
   ( (lvl1 /= lvl1$0 or lvl2 /= lvl2$0) & inf_equal_level(lvl1$0,lvl2$0) = TRUE)
    => (({lvl1|->lvl2}<<|inf_equal_level\/{lvl1|->lvl2|->TRUE} 
        )(lvl1$0,lvl2$0) = TRUE)
    ;
       ( (lvl1 /= lvl1$0 or lvl2 /= lvl2$0) & inf_level(lvl1$0,lvl2$0) = TRUE)
    => (({lvl1|->lvl2}<<|inf_level\/{lvl1|->lvl2|->TRUE} 
        )(lvl1$0,lvl2$0) = TRUE)
    ;
       ( (lvl1 /= lvl1$0 or lvl2 /= lvl2$0) & equal_level(lvl1$0,lvl2$0) = TRUE)
    => (({lvl1|->lvl2}<<|equal_level\/{lvl1|->lvl2|->TRUE} 
        )(lvl1$0,lvl2$0) = TRUE)
END

Exemple de commandes utiles

te((dd & se(lvl_event) & pr), Replace.Gen.Unproved)

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