From 22ac7ba5234d4373cdc1cbfe69718cb40042472e Mon Sep 17 00:00:00 2001 From: Manuel Krucker Date: Mon, 12 May 2008 13:02:41 +0000 Subject: [PATCH] git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7959 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/wfcpog/SecureUML_constraint.sml | 215 ++------------------- 1 file changed, 21 insertions(+), 194 deletions(-) diff --git a/su4sml/src/wfcpog/SecureUML_constraint.sml b/su4sml/src/wfcpog/SecureUML_constraint.sml index 413ed87..d2d56b6 100644 --- a/su4sml/src/wfcpog/SecureUML_constraint.sml +++ b/su4sml/src/wfcpog/SecureUML_constraint.sml @@ -50,19 +50,17 @@ sig val get : WFCPOG.wfpo -> T val put : T -> WFCPOG.wfpo -> WFCPOG.wfpo val map : (T -> T) -> WFCPOG.wfpo -> WFCPOG.wfpo + end - (* - (** sub constraint, included in operational consistency.*) - val generate_secureUML_creators_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - (** sub constraint, included in operational consistency.*) - val generate_secureUML_destructors_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - (** sub constraint, included in operational consistency.*) - val generate_secureUML_getters_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - val generate_secureUML_setters_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - val generate_secureUML_op_sec_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - val generate_pos : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list - *) +(* + val are_roles_mutex : WFCPOG.wfpo -> Rep_Core.transform_model -> bool + val rh_is_tree : WFCPOG.wfpo -> Rep_Core.transform_model -> bool + + val executable_by_some_role : WFCPOG.wfpo -> Rep_Core.transform_model -> bool + + val authorized_for_some_action : WFCPOG.wfpo -> Rep_Core.transform_model -> bool +*) val separation_of_duty : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list val binding_of_duty : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list @@ -84,17 +82,9 @@ open Rep_SecureUML (* oclparser *) open ModelImport - - (* wfcpo-gen *) open WFCPOG_Library - - -exception WFCPO_SecureUMLError of string - - - type SSD_args = {key : int, mutex_perm_sets: (Permission list) list @@ -108,183 +98,9 @@ structure WFCPOG_SSD_Data = WFCPOG_DataFun fun extend T = T; end); - -fun case_insensitive "" = "" - | case_insensitive s:string = - let - fun to_lower [x] = [Char.toLower x] - | to_lower (h::tail) = (Char.toLower h)::(to_lower tail) - in - String.implode (to_lower (String.explode s)) - end - - -(* get corresponding operation x from x_sec of. *) -fun secureUML_real_op oper class model = - let - val name = name_of_op oper - val len = String.size name - val substr = String.substring (name,0,len-4) - in - get_operation substr class model - end - -fun secureUML_sec_op oper class model = - let - val name = name_of_op oper ^ "_sec" - in - get_operation name class model - end - - -fun secureUML_get_att_name oper = - let - val name = name_of_op oper - val len = String.size name - in - String.substring (name,0,len-4) - end - -(* *) -fun secureUML_getter_operations_of class model = List.filter (fn a => String.isPrefix "get" (name_of_op a)) (local_operations_of class) -(* *) -fun secureUML_setter_operations_of class model = List.filter (fn a => String.isPrefix "set" (name_of_op a)) (local_operations_of class) -(* *) -fun secureUML_op_sec_operations_of class model = List.filter (fn a => String.isSuffix "_sec" (name_of_op a)) (local_operations_of class) - -fun secureUML_substitute_terms (OperationCall(src,typ,path,args,rtyp)) class = - let - val op_name = List.last path - val p_len = List.length path - val p = List.take (path,p_len-1) - in - if (name_of class) = p - then (* substitute operation x with x_sec *) - (OperationCall(src,typ,p@[op_name^"_sec"],args,rtyp)) - else OperationCall(src,typ,path,args,rtyp) - end - | secureUML_substitute_terms (AttributeCall(src,typ,path,rtyp)) class = - let - val att_name = List.last path - val p_len = List.length path - val p = List.take (path,p_len-1) - in - if (name_of class) = p - then (* substitute attribute x with operation getX() *) - OperationCall(src,typ,p@["get"^att_name],[],rtyp) - else AttributeCall(src,typ,path,rtyp) - end - | secureUML_substitute_terms x class = x - -fun generate_secureUML_creators_po class (model as (clist,alist)) = - let - val creators = creation_operations_of class model - in - (List.map (fn a => - let - val op_res = result_of_op a - val result = Variable("result",op_res) - val term1 = OperationCall(result,op_res,(name_of class)@["oclIsUndefined"],[],Boolean) - val term2 = OperationCall(result,op_res,(name_of class)@["modifiedOnly"],[],Boolean) - in - (("oper_model_constr"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)) - end - ) creators) - end - -fun generate_secureUML_destructors_po class (model as (clist,alist)) = - let - val destructors = destruction_operations_of class model - in - (List.map (fn a => - let - val self = Variable("self",type_of class) - val term1 = OperationCall(self,type_of class,(name_of class)@["oclIsUndefined"],[],Boolean) - val atPre = OperationCall(self,type_of class,["oclLib","OclAny","atPre"],[],type_of class) - val term2 = OperationCall(atPre,type_of class,(name_of class)@["modifiedOnly"],[],Boolean) - in - (("oper_model_destr_"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)) - end - ) destructors) - end - -fun generate_secureUML_getters_po class (model as (clist,alist)) = - let - val getter = secureUML_getter_operations_of class model - in - (List.map (fn a => - let - val op_res = result_of_op a - val att_name = secureUML_get_att_name a - val result = Variable("result",op_res) - val self = Variable("self",type_of class) - val atCall = AttributeCall(self,type_of class,(name_of class)@[(att_name)],op_res) - in - (("oper_model_getters_"^(string_of_path (name_of class))),OperationCall(result,op_res,["oclLib","Boolean","="],[(atCall,op_res)],Boolean)) - end - ) getter) - end - -fun generate_secureUML_setters_po class (model as (clist,alist)) = - let - val setter = secureUML_setter_operations_of class model - in - (List.map (fn a => - let - val (name,arg_type)= hd(arguments_of_op a) - val self = Variable("self",type_of class) - val att_name = secureUML_get_att_name a - val arg = Variable(name,arg_type) - val att = AttributeCall(self,type_of class,(name_of class)@[att_name],arg_type) - val term1 = OperationCall(att,arg_type,["oclLib","Boolean","="],[(arg,arg_type)],Boolean) - val term2 = OperationCall(att,arg_type,(name_of class)@["modifiedOnly"],[],Boolean) - in - (("oper_model_setters_"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)) - end - ) setter) - end - -fun generate_secureUML_op_sec_po class (model as (clist,alist)) = - let - val op_sec = secureUML_op_sec_operations_of class model - in - List.concat (List.map (fn a => - let - val real_op = secureUML_real_op a class model - val add_pres = List.map (fn (a,b) => (case a of - NONE => (("pre_"^(string_of_path(name_of class))),b) - | SOME(x) => (x,b))) (precondition_of_op real_op) - val real_posts = postcondition_of_op real_op - val add_posts = List.map (fn (a,b) => (case a of - NONE => (("post_"^(string_of_path(name_of class))),(secureUML_substitute_terms b class)) - | SOME(x) => (x,(secureUML_substitute_terms b class)))) (real_posts) - in - add_pres@add_posts - end - ) op_sec) - end - - - -fun generate_pos wfpo (model as (clist,alist)) = (* [Variable("s",DummyT)] *) - let - val design_model_classes = removeOclLibrary clist - val po1 = List.map (fn a => generate_secureUML_creators_po a model) design_model_classes - val po2 = List.map (fn a => generate_secureUML_destructors_po a model) design_model_classes - val po3 = List.map (fn a => generate_secureUML_getters_po a model) design_model_classes - val po4 = List.map (fn a => generate_secureUML_setters_po a model) design_model_classes - val po5 = List.map (fn a => generate_secureUML_op_sec_po a model) design_model_classes - in - List.concat(po1@po2@po3@po4@po5) - end - - - - fun ssd_generate_pos [] classes model = [] | ssd_generate_pos perms class model = [] - fun separation_of_duty_help [] classes model = []:((Path * OclTerm) list ) | separation_of_duty_help (h::perm_sets) classes model = let @@ -300,9 +116,20 @@ fun separation_of_duty_help [] classes model = []:((Path * OclTerm) list ) fun binding_of_duty_help [] (cl::clist) model = [] +(* +fun rh_is_tree wfpo (model as (clist,alist)) = + let + val _ = trace funciton_calls ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Role a)) cl + - + val _ = trace funciton_calls ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") + in + res + end +*) fun separation_of_duty wfpo (model as (clist,alist)) = let val _ = trace function_calls ("WFCPOG_SecureUML_Constraint.separation_of_duty\n")