583 lines
24 KiB
Standard ML
583 lines
24 KiB
Standard ML
(*****************************************************************************
|
|
* su4sml --- an SML repository for managing (Secure)UML/OCL models
|
|
* http://projects.brucker.ch/su4sml/
|
|
*
|
|
* rep_su2holocl.sml --- a SecureUML to UML/OCL model transformation
|
|
* This file is part of su4sml.
|
|
*
|
|
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
|
|
*
|
|
* All rights reserved.
|
|
*
|
|
* Redistribution and use in source and binary forms, with or without
|
|
* modification, are permitted provided that the following conditions are
|
|
* met:
|
|
*
|
|
* * Redistributions of source code must retain the above copyright
|
|
* notice, this list of conditions and the following disclaimer.
|
|
*
|
|
* * Redistributions in binary form must reproduce the above
|
|
* copyright notice, this list of conditions and the following
|
|
* disclaimer in the documentation and/or other materials provided
|
|
* with the distribution.
|
|
*
|
|
* * Neither the name of the copyright holders nor the names of its
|
|
* contributors may be used to endorse or promote products derived
|
|
* from this software without specific prior written permission.
|
|
*
|
|
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
|
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
|
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
|
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
|
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
|
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
|
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
|
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
|
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
|
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
******************************************************************************)
|
|
(* $Id$ *)
|
|
|
|
structure SecureUML2HolOcl:sig
|
|
val transform : Rep_SecureUML_ComponentUML.Model -> Rep.Model
|
|
end = struct
|
|
|
|
open Rep_Helper
|
|
open Rep_Core
|
|
open XMI_DataTypes
|
|
open Rep_OclTerm
|
|
open Rep_OclHelper
|
|
open Rep_SecureUML_ComponentUML
|
|
open StringHandling
|
|
|
|
(* can this be expressed more combinatorially? *)
|
|
fun deep_atpre (t as Literal _) = t
|
|
| deep_atpre (t as CollectionLiteral _) = t
|
|
| deep_atpre (t as If (cond,cond_type,then_term,then_type,
|
|
else_term,else_type,result_type) )
|
|
= If (deep_atpre cond, cond_type,
|
|
deep_atpre then_term, then_type,
|
|
deep_atpre else_term, else_type,
|
|
result_type)
|
|
| deep_atpre (t as AssociationEndCall (source,source_type,
|
|
path, result_type))
|
|
= atpre (AssociationEndCall (deep_atpre source,
|
|
source_type, path, result_type))
|
|
| deep_atpre (t as AttributeCall (source,source_type,path,result_type))
|
|
= atpre (AttributeCall (deep_atpre source, source_type,
|
|
path, result_type))
|
|
| deep_atpre (t as OperationCall (source, source_type, path, args, result_type))
|
|
= atpre (OperationCall (deep_atpre source, source_type, path,
|
|
ListPair.zip (map (deep_atpre o #1) args, map #2 args),
|
|
result_type))
|
|
| deep_atpre (t as OperationWithType (source, source_type, param, param_type,
|
|
result_type))
|
|
(* FIXME: do we have to wrap it with atPre? *)
|
|
= OperationWithType (deep_atpre source, source_type, param, param_type,
|
|
result_type)
|
|
| deep_atpre (t as Variable _)
|
|
(* FIXME: we probably want to wrap this, to get self@pre? *)
|
|
= t
|
|
| deep_atpre (t as Let (var,var_type,rhs,rhs_type,in_term,in_type))
|
|
= Let (var,var_type,
|
|
deep_atpre rhs, rhs_type,
|
|
deep_atpre in_term, in_type)
|
|
| deep_atpre (t as Iterate (vars,acc,acc_type,acc_init,source,source_type,
|
|
body, body_type, result_type))
|
|
= Iterate (vars, acc, acc_type, deep_atpre acc_init,
|
|
deep_atpre source, source_type,
|
|
deep_atpre body, body_type,
|
|
result_type)
|
|
| deep_atpre (t as Iterator (name, vars, source, source_type,
|
|
body, body_type, result_type))
|
|
= Iterator (name, vars, deep_atpre source, source_type,
|
|
deep_atpre body, body_type, result_type)
|
|
|
|
|
|
|
|
(* FIXME: find appropriate name for this function *)
|
|
fun transform_postconds {name, precondition, postcondition, body,arguments, result,
|
|
isQuery, scope, visibility} =
|
|
{ name=name,
|
|
precondition=precondition,
|
|
postcondition=map (fn (s,t) => (s,deep_atpre t)) postcondition,
|
|
arguments=arguments,
|
|
result=result,
|
|
body=body,
|
|
isQuery=isQuery,
|
|
scope=scope,
|
|
visibility=visibility
|
|
}
|
|
|
|
|
|
|
|
|
|
(** replace all operation calls in the given expression with calls to
|
|
* the "secured" variant.
|
|
*)
|
|
fun replace_opcalls (t as Literal _) = t
|
|
| replace_opcalls (t as CollectionLiteral _) = t
|
|
| replace_opcalls (t as If (cond,ctype,then_term,then_type,
|
|
else_term,else_type,result_type)) =
|
|
If (replace_opcalls cond, ctype,
|
|
replace_opcalls then_term, then_type,
|
|
replace_opcalls else_term, else_type,
|
|
result_type)
|
|
| replace_opcalls (t as AssociationEndCall (source,source_type,path,result_type)) =
|
|
AssociationEndCall (replace_opcalls source, source_type,
|
|
path, result_type)
|
|
| replace_opcalls (t as AttributeCall (source,source_type,path,result_type)) =
|
|
AttributeCall (replace_opcalls source, source_type, path, result_type)
|
|
| replace_opcalls (t as OperationCall (source,source_type,path,args,result_type))=
|
|
OperationCall (replace_opcalls source, source_type,
|
|
let val oper = List.hd (List.rev path)
|
|
val pth = List.tl (List.rev path)
|
|
in
|
|
List.rev (oper^"_sec"::pth)
|
|
end,
|
|
ListPair.zip (map (replace_opcalls o #1) args,
|
|
map #2 args),
|
|
result_type)
|
|
| replace_opcalls (t as OperationWithType (source,source_type,
|
|
param,param_type,result_type)) =
|
|
OperationWithType (replace_opcalls source, source_type,
|
|
param, param_type, result_type)
|
|
| replace_opcalls (t as Variable _) = t
|
|
| replace_opcalls (t as Let (var,var_type,rhs,rhs_type,in_term,in_type)) =
|
|
Let (var,var_type,
|
|
replace_opcalls rhs, rhs_type,
|
|
replace_opcalls in_term, in_type)
|
|
| replace_opcalls (t as Iterate (vars,acc,acc_type,acc_init,source,source_type,
|
|
body, body_type, result_type)) =
|
|
Iterate (vars,
|
|
acc,acc_type, replace_opcalls acc_init,
|
|
replace_opcalls source, source_type,
|
|
replace_opcalls body, body_type,
|
|
result_type)
|
|
| replace_opcalls (t as Iterator (iter,vars,source,source_type,body,body_type,
|
|
result_type))=
|
|
Iterator (iter,vars,
|
|
replace_opcalls source, source_type,
|
|
replace_opcalls body, body_type,
|
|
result_type)
|
|
|
|
(** replace all attribute calls in the given expression with calls to the
|
|
* corresponding getter operation.
|
|
*)
|
|
fun replace_attcalls (t as Literal _) = t
|
|
| replace_attcalls (t as CollectionLiteral _) = t
|
|
| replace_attcalls (t as If (cond,ctype,then_term,then_type,
|
|
else_term,else_type,result_type)) =
|
|
If (replace_attcalls cond, ctype,
|
|
replace_attcalls then_term, then_type,
|
|
replace_attcalls else_term, else_type,
|
|
result_type)
|
|
| replace_attcalls (t as AssociationEndCall (source,source_type,path,result_type)) =
|
|
AssociationEndCall (replace_attcalls source, source_type,
|
|
path, result_type)
|
|
| replace_attcalls (t as AttributeCall (source,source_type,path,result_type)) =
|
|
OperationCall (replace_attcalls source, source_type,
|
|
let val att = List.hd (List.rev path)
|
|
val pth = List.tl (List.rev path)
|
|
in
|
|
List.rev ("get"^(capitalize att)::pth)
|
|
end,
|
|
nil, (* the getter has no arguments *)
|
|
result_type)
|
|
| replace_attcalls (t as OperationCall (source,source_type,path,args,result_type))=
|
|
OperationCall (replace_attcalls source, source_type,
|
|
path,args, result_type)
|
|
| replace_attcalls (t as OperationWithType (source,source_type,
|
|
param,param_type,result_type)) =
|
|
OperationWithType (replace_attcalls source, source_type,
|
|
param, param_type, result_type)
|
|
| replace_attcalls (t as Variable _) = t
|
|
| replace_attcalls (t as Let (var,var_type,rhs,rhs_type,in_term,in_type)) =
|
|
Let (var,var_type,
|
|
replace_attcalls rhs, rhs_type,
|
|
replace_attcalls in_term, in_type)
|
|
| replace_attcalls (t as Iterate (vars,acc,acc_type,acc_init,source,source_type,
|
|
body, body_type, result_type)) =
|
|
Iterate (vars,
|
|
acc,acc_type, replace_attcalls acc_init,
|
|
replace_attcalls source, source_type,
|
|
replace_attcalls body, body_type,
|
|
result_type)
|
|
| replace_attcalls (t as Iterator (iter,vars,source,source_type,body,body_type,
|
|
result_type))=
|
|
Iterator (iter,vars,
|
|
replace_attcalls source, source_type,
|
|
replace_attcalls body, body_type,
|
|
result_type)
|
|
|
|
(** creates a getter function for the given attribute.
|
|
* The name of the function is get<Attributename>, and it has
|
|
* a postcondition of result=self.att
|
|
* should be moved to Rep_Core?
|
|
*)
|
|
fun create_getter c {name,attr_type,visibility,scope,stereotypes,init} =
|
|
{ name="get"^(capitalize name),
|
|
precondition=nil,
|
|
body=nil,
|
|
(* post: result=self.att *)
|
|
postcondition=[(SOME ("generated_getter_for_"^name),
|
|
ocl_eq (result attr_type)
|
|
(ocl_attcall (self (Classifier (name_of c)))
|
|
((name_of c)@[name])
|
|
attr_type))],
|
|
arguments=nil,
|
|
result=attr_type,
|
|
isQuery=true,
|
|
scope=scope,
|
|
visibility=public,
|
|
stereotypes=[]
|
|
}
|
|
|
|
(** creates a setter function for the given attribute.
|
|
* The name of the function is set<Attributename>, and it has
|
|
* a postcondition of self.att=arg and self.att->modifiedOnly()
|
|
* Should be moved to rep_core?
|
|
*)
|
|
fun create_setter c {name,attr_type,visibility,scope,stereotypes,init} =
|
|
let val self_att = ocl_attcall (self (Classifier (name_of c)))
|
|
((name_of c)@[name])
|
|
attr_type
|
|
in
|
|
{ name="set"^(capitalize name),
|
|
precondition=nil,
|
|
body=nil,
|
|
postcondition=[(SOME ("generated_setter_for_"^name),
|
|
ocl_and (ocl_eq self_att
|
|
(Variable ("arg", attr_type)))
|
|
(ocl_modifiedOnly (ocl_set [self_att] attr_type)))
|
|
],
|
|
arguments=[("arg",attr_type)],
|
|
result=OclVoid,
|
|
isQuery=false,
|
|
scope=scope,
|
|
visibility=public,
|
|
stereotypes=[]
|
|
}
|
|
end
|
|
|
|
(** creates a "secured" version of the given operation.
|
|
* The main change: in the postcondition, attribute calls are replaced with
|
|
* calls to appropriate getter functions, and operation calls with calls
|
|
* to corresponding "secured" operations.
|
|
*)
|
|
fun create_secured {name, body,precondition, postcondition, arguments, result,
|
|
isQuery, scope,stereotypes,visibility} =
|
|
{ name=name^"_sec",
|
|
precondition=precondition,
|
|
postcondition=map (fn (name,t) => (name,replace_attcalls (replace_opcalls t)))
|
|
postcondition,
|
|
arguments=arguments,
|
|
result=result,
|
|
body=body,
|
|
isQuery=isQuery,
|
|
scope=scope,
|
|
stereotypes=stereotypes,
|
|
visibility=visibility
|
|
}
|
|
|
|
|
|
|
|
(** The design model transformation for a single class.
|
|
* generates constructors, destructors, setters, getters, and "secured" operations.
|
|
*)
|
|
fun add_operations c =
|
|
let
|
|
val self_type = Classifier (name_of c)
|
|
val res = result (Classifier (name_of c))
|
|
val constructor =
|
|
{name="new",
|
|
precondition=nil,
|
|
(* post: result.oclIsNew() and result->modiefiedOnly() *)
|
|
postcondition=[(SOME "generated_constructor",
|
|
ocl_and (ocl_isNew (result self_type))
|
|
(ocl_modifiedOnly (ocl_set [res]
|
|
(self_type))))
|
|
],
|
|
body = [],
|
|
arguments=nil,
|
|
result=Classifier (name_of c),
|
|
isQuery=false,
|
|
scope=ClassifierScope,
|
|
visibility=public,
|
|
stereotypes=[]}
|
|
val destructor =
|
|
{name="delete",
|
|
precondition=nil,
|
|
body=nil,
|
|
(* post: self.oclIsUndefined() and self@pre->modifiedOnly() *)
|
|
postcondition=[(SOME "generated_destructor",
|
|
ocl_and (ocl_isUndefined (self self_type))
|
|
(ocl_modifiedOnly
|
|
(ocl_set [atpre (self self_type)]
|
|
self_type)))
|
|
],
|
|
arguments=nil,
|
|
result=OclVoid,
|
|
isQuery=false,
|
|
scope=InstanceScope,
|
|
visibility=public,
|
|
stereotypes=[]}
|
|
val getters = map (create_getter c) (attributes_of c)
|
|
val setters = map (create_setter c) (attributes_of c)
|
|
val sec_ops = map create_secured (operations_of c)
|
|
val generated_ops = [constructor,destructor]@getters@setters@sec_ops
|
|
in
|
|
List.foldl (uncurry addOperation) c generated_ops
|
|
end
|
|
|
|
|
|
|
|
val identity_role_association =
|
|
{name=["AuthorizationEnvironment","IdentityRoleAssociation"],
|
|
aends=[{name=["AuthorizationEnvironment","Association","identity"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Identity"],
|
|
init=NONE,
|
|
multiplicity=[(0,~1)],
|
|
ordered=false,
|
|
visibility=public},
|
|
{name=["AuthorizationEnvironment","Association","roles"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Role"],
|
|
init=NONE,multiplicity=[(0,~1)],
|
|
ordered=false,
|
|
visibility=public}
|
|
],
|
|
qualifiers=[],
|
|
aclass=NONE}
|
|
|
|
val identity_principal_association =
|
|
{name=["AuthorizationEnvironment","IdentityPrincipalAssociation"],
|
|
aends=[{name=["AuthorizationEnvironment","Association","identity"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Identity"],
|
|
init=NONE,
|
|
multiplicity=[(1,1)],
|
|
ordered=false,
|
|
visibility=public},
|
|
{name=["AuthorizationEnvironment","Association","principal"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Principal"],
|
|
init=NONE,multiplicity=[(0,~1)],
|
|
ordered=false,
|
|
visibility=public}
|
|
],
|
|
qualifiers=[],
|
|
aclass=NONE}
|
|
|
|
val context_principal_association =
|
|
{name=["AuthorizationEnvironment","ContextPrincipalAssociation"],
|
|
aends=[{name=["AuthorizationEnvironment","ContextPrincipalAssociation",
|
|
"principal"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Principal"],
|
|
init=NONE,
|
|
multiplicity=[(1,1)],
|
|
ordered=false,
|
|
visibility=public},
|
|
{name=["AuthorizationEnvironment","ContextPrincipalAssociation",
|
|
"context"],
|
|
aend_type=Classifier ["AuthorizationEnvironment","Context"],
|
|
init=NONE,
|
|
multiplicity=[(0,~1)],
|
|
ordered=false,
|
|
visibility=public}
|
|
],
|
|
qualifiers=[],
|
|
aclass=NONE}
|
|
|
|
val role =
|
|
Class {activity_graphs=[],
|
|
(* associationends=[{aend_type=Classifier
|
|
["AuthorizationEnvironment","Identity"],
|
|
init=NONE,multiplicity=[(0,~1)],
|
|
name="identity",
|
|
ordered=false,
|
|
visibility=public}],
|
|
*)
|
|
associations=[["AuthorizationEnvironment",
|
|
"IdentityRoleAssociation"]],
|
|
attributes=[{attr_type=String,
|
|
init=NONE,name="name",
|
|
scope=InstanceScope,
|
|
stereotypes=[],
|
|
visibility=public
|
|
}],
|
|
interfaces=[],
|
|
invariant=[],
|
|
name=Classifier ["AuthorizationEnvironment","Role"],
|
|
operations=[{arguments=[("s",String)],
|
|
isQuery=false,
|
|
name="getRoleByName",
|
|
postcondition=[],
|
|
precondition=[],
|
|
body=[],
|
|
result=Classifier ["AuthorizationEnvironment","Role"],
|
|
scope=ClassifierScope,
|
|
stereotypes=[],
|
|
visibility=public}
|
|
],
|
|
parent=NONE,
|
|
stereotypes=[],
|
|
thyname=NONE,
|
|
visibility=public}
|
|
|
|
val identity =
|
|
Class { activity_graphs=[],
|
|
(* associations=[{aend_type=Classifier
|
|
["AuthorizationEnvironment","Role"],
|
|
init=NONE,multiplicity=[(0,~1)],
|
|
name="roles",
|
|
ordered=false,
|
|
visibility=public},
|
|
{aend_type=Classifier
|
|
["AuthorizationEnvironment","Principal"],
|
|
init=NONE,
|
|
multiplicity=[(0,~1)],
|
|
name="principal",
|
|
ordered=false,
|
|
visibility=public}],
|
|
*) associations= [["AuthorizationEnvironment","IdentityRoleAssociation"],
|
|
["AuthorizationEnvironment","IdentityPrincipalAssociation"]
|
|
],
|
|
attributes=[{attr_type=String,
|
|
init=NONE,name="name",
|
|
scope=InstanceScope,
|
|
stereotypes=[],
|
|
visibility=public}],
|
|
interfaces=[],
|
|
invariant=[],
|
|
name=Classifier ["AuthorizationEnvironment","Identity"],
|
|
operations=[],
|
|
parent=NONE,
|
|
visibility=public,
|
|
stereotypes=[],
|
|
thyname=NONE
|
|
}
|
|
|
|
val static_auth_env = [
|
|
Class { activity_graphs=[],
|
|
(* associations=[{aend_type=Classifier
|
|
["AuthorizationEnvironment","Principal"],
|
|
init=NONE,
|
|
multiplicity=[(1,1)],
|
|
name="principal",
|
|
ordered=false,
|
|
visibility=public}],
|
|
*) associations=[["AuthorizationEnvironment","ContextPrincipalAssociation"]],
|
|
attributes=[],
|
|
interfaces=[],
|
|
invariant=[],
|
|
name=Classifier ["AuthorizationEnvironment","Context"],
|
|
operations=[],
|
|
parent=NONE,
|
|
visibility=public:Rep_Core.Visibility,
|
|
stereotypes=[],
|
|
thyname=NONE},
|
|
Class
|
|
{ activity_graphs=[],
|
|
(* associations=[{aend_type=Classifier
|
|
["AuthorizationEnvironment","Identity"],
|
|
init=NONE,
|
|
multiplicity=[(1,1)],
|
|
name="identity",
|
|
ordered=false,
|
|
visibility=public},
|
|
{aend_type=Classifier
|
|
["AuthorizationEnvironment","Context"],
|
|
init=NONE,
|
|
multiplicity=[(0,~1)],
|
|
name="context",
|
|
ordered=false,
|
|
visibility=public}],
|
|
*) associations=[["AuthorizationEnvironment","IdentityPrincipalAssociation"],
|
|
["AuthorizationEnvironment","ContextPrincipalAssociation"]
|
|
],
|
|
attributes=[],
|
|
interfaces=[],
|
|
invariant=[],
|
|
name=Classifier ["AuthorizationEnvironment","Principal"],
|
|
operations=[{arguments=[("s",String)],
|
|
isQuery=false,
|
|
name="isInRole",
|
|
postcondition=[],
|
|
precondition=[],
|
|
body=[],
|
|
result=Boolean,
|
|
stereotypes=[],
|
|
scope=InstanceScope:Rep_Core.Scope,
|
|
visibility=public:Rep_Core.Visibility }],
|
|
parent=NONE,
|
|
visibility=public:Rep_Core.Visibility,
|
|
stereotypes=[],
|
|
thyname=NONE}]
|
|
|
|
(** defines the role hierarchy. *)
|
|
(* FIXME: context Identity inv: self.roles.name->includes(r1) implies *)
|
|
(* self.roles.name->includes(r2) *)
|
|
fun define_role_hierarchy (sc:Security.Configuration) =
|
|
let val identity_name = ["AuthorizationEnvironment","Identity"]
|
|
val identity_type = Classifier identity_name
|
|
val role_name = ["AuthorizationEnvironment","Role"]
|
|
val role_type = Classifier role_name
|
|
val self_roles =
|
|
ocl_aendcall (self identity_type)
|
|
["AuthorizationEnvironment" , "Identity", "roles"]
|
|
(Bag (Classifier ["AuthorizationEnvironment","Role"]))
|
|
val self_roles_name = ocl_collect self_roles "anonIterVar_0"
|
|
(ocl_attcall (Variable ("anonIterVar_0",
|
|
role_type))
|
|
["AuthorizationEnvironment","Role","name"]
|
|
String)
|
|
fun is_in_role x = ocl_includes self_roles_name x
|
|
fun invariant_for_role_inheritance (sub,super) =
|
|
ocl_implies (is_in_role (Literal (sub,String)))
|
|
(is_in_role (Literal (super,String)))
|
|
in
|
|
List.foldl (fn (rh,ident) => addInvariant
|
|
(SOME "role_hierarchy",
|
|
invariant_for_role_inheritance rh) ident)
|
|
identity
|
|
(#rh sc)
|
|
end
|
|
|
|
(** defines the list or roles in the model.
|
|
* context Role inv: Role.allInstances().name = Bag{...}
|
|
*)
|
|
fun define_roles sc =
|
|
let val roles = Security.all_roles sc
|
|
val role_collection = map (fn x =>CollectionItem(Literal (x,String),String))
|
|
roles
|
|
val role_type = Classifier ["AuthorizationEnvironment", "Role"]
|
|
val inv = ocl_eq (ocl_collect (ocl_allInstances (self role_type))
|
|
"anonIterVar_0"
|
|
(ocl_attcall (Variable ("anonIterVar_0",role_type))
|
|
["AuthorizationEnvironment","Role","name"]
|
|
String))
|
|
(CollectionLiteral (role_collection, Bag String))
|
|
in
|
|
addInvariant (SOME "list_of_roles",inv) role
|
|
end
|
|
|
|
(** transform the postconditions to also include the authorization constraints. *)
|
|
(* FIXME: implement this *)
|
|
fun create_sec_postconds sc c = c
|
|
|
|
|
|
fun transform (model:Rep.Model,sc) =
|
|
let
|
|
val transformedDesignModel = (map add_operations (#1 model),#2 model)
|
|
val transformedModel = create_sec_postconds sc transformedDesignModel
|
|
val authEnv = map (normalize (#2 transformedModel))
|
|
(define_roles sc::define_role_hierarchy sc::
|
|
static_auth_env)
|
|
in
|
|
((#1 transformedModel) @ authEnv,identity_role_association::
|
|
identity_principal_association::
|
|
context_principal_association::
|
|
(#2 transformedModel))
|
|
end
|
|
|
|
end
|