git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7959 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Manuel Krucker
parent
30cf12552a
commit
22ac7ba523
|
|
@ -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")
|
||||
|
|
|
|||
Loading…
Reference in New Issue