HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

some work on codegen for secureuml 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@5933 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Jürgen Doser 2007-01-22 16:31:26 +00:00
parent 29f3d7cfc1
commit 451a709fbe
10 changed files with 186 additions and 133 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/codegen/codegen.cm
View File

@ -1,24 +1,30 @@
Group is
#if(defined(SMLNJ_VERSION))
$/basis.cm
$smlnj/compiler/compiler.cm
$smlnj/compiler/current.cm
$/smlnj-lib.cm
#else
#endif
../su4sml.cm
compiler/compiler_ext.sig
compiler/smlnj.sml
security_cartridge.sig
cartridge.sig
security_cartridge.sig
gcg_library.sml
gcg_helper.sml
tpl_parser.sig
tpl_parser.sml
cartridge.sig
base_cartridge.sig
SM_helper.sml
stateMachine.sml
stateMachineTypes.sml
base_cartridge.sml
stringHandling.sml
c#_cartridge.sml
c#_net1_cartridge.sml
secureuml_cartridge.sig
secureuml_cartridge.sml
gcg_core.sig
design_cartridge.sig
componentuml_cartridge.sml
c#sm_cartridge.sml
java_cartridge.sml
junit_cartridge.sml
gcg_core.sml
codegen.sml

4
src/codegen/codegen.sml
View File

@ -49,6 +49,8 @@ structure Java_Gcg = GCG_Core (Java_Cartridge(Base_Cartridge))
structure Junit_Gcg = GCG_Core (Junit_Cartridge(Java_Cartridge(Base_Cartridge)))
structure SecureMova_Gcg = GCG_Core (ComponentUML_Cartridge(Base_Cartridge))
(*
structure JavaSecure_Gcg = GCG_Core (Java_Cartridge(SecureUML_Cartridge(Base_Cartridge)));
*)
@ -76,6 +78,8 @@ fun generate xmi_file "base" =
Base_Gcg.generate ( RepParser.readFile xmi_file) "templates/maude.tpl"
| generate xmi_file "maude_secure" =
SecureUML_Base_Gcg.generate ( Rep_SecureUML_ComponentUML.readXMI xmi_file) "templates/maude.tpl" *)
| generate xmi_file "securemova" =
SecureMova_Gcg.generate (RepParser.readFile xmi_file) "templates/securemova.tpl"
| generate _ s = print ("target language unknown : "^s^"\n"^
"usage: generate <xmi_file> \"base\" | \"c#\" | \"c#_secure\" | \"c#_net1\" | \"c#_secure_net1\" | \"java\" | \"junit\"\n")

32
src/codegen/componentuml_cartridge.sml
View File

@ -9,9 +9,10 @@ open library
(* TODO: fill out *)
type environment = { curPermissionList: SuperCart.Security.Permission list option,
curPermission: SuperCart.Security.Permission option,
curEntity: Rep.Classifier option,
extension: SuperCart.environment}
type Model = SuperCart.Model
(* unpack : environment -> SuperCart.environment *)
fun unpack (env : environment) = #extension env
@ -19,12 +20,14 @@ fun unpack (env : environment) = #extension env
fun pack (env: environment) (new_env : SuperCart.environment) =
{ curPermissionList = #curPermissionList env,
curPermission = #curPermission env,
curEntity = #curEntity env,
extension = new_env}
fun initEnv model = { curPermissionList = NONE,
curPermission = NONE,
curEntity = NONE,
extension = SuperCart.initEnv model}
(* fun getModel (env : environment) = SuperCart.getModel (unpack env) *)
fun curClassifier (env : environment) = SuperCart.curClassifier (unpack env)
fun curAttribute (env : environment) = SuperCart.curAttribute (unpack env)
@ -37,17 +40,17 @@ fun curArgument (env : environment) = SuperCart.curArgument (unpack env)
* Maybe sme of this should be moved to component_uml.sml...
*)
fun atomic_actions_from_context env =
if Option.isSome (curAttribute env) then
if Option.isSome (curAttribute env) then
let fun make_action s =
ComponentUML.SimpleAction (s, ComponentUMLResource.EntityAttribute
(Option.valOf (curAttribute env)))
in [make_action "read", make_action "update"] end
else if Option.isSome (curOperation env) then
else if Option.isSome (curOperation env) then
let fun make_action s =
ComponentUML.SimpleAction (s, ComponentUMLResource.EntityMethod
(Option.valOf (curOperation env)))
in [make_action "execute"] end
else if Option.isSome (curClassifier env) then
else if Option.isSome (curClassifier env) then
let fun make_action s =
ComponentUML.SimpleAction (s, ComponentUMLResource.Entity
(Option.valOf (curClassifier env)))
@ -68,6 +71,10 @@ fun lookup (env:environment) "permission_name" =
(case #curPermission env of
SOME x => #name x
| NONE => SuperCart.lookup (unpack env) "permission_name")
| lookup env "entity_name" =
(case #curEntity env
of SOME s => Rep.short_name_of s
| NONE => SuperCart.lookup (unpack env) "entity_name")
| lookup env s = SuperCart.lookup (unpack env) s
(********** ADDING IF-CONDITION TYPE *****************************************)
@ -91,16 +98,29 @@ fun foreach_permission env name =
val permissions = permissions_for_action env action
fun env_from_list_item c = { curPermissionList = SOME permissions,
curPermission = SOME c,
curEntity = #curEntity env,
extension = #extension env} : environment
in
List.map env_from_list_item permissions
end
fun foreach_entity (env:environment) =
let val entities = List.filter (fn x => ListEq.includes (Rep.stereotypes_of x) "compuml.entity" )
(#1 (#model (#extension env)))
fun env_from_list_item c = { curPermissionList = #curPermissionList env,
curPermission = #curPermission env,
curEntity = SOME c,
extension = #extension env}:environment
in
List.map env_from_list_item entities
end
fun foreach "readPermission_list" env = foreach_permission env "read"
| foreach "updatePermission_list" env = foreach_permission env "update"
| foreach "createPermission_list" env = foreach_permission env "create"
| foreach "deletePermission_list" env = foreach_permission env "delete"
| foreach "executePermission_list" env = foreach_permission env "execute"
| foreach "entity_list" env = foreach_entity env
| foreach listType env = map (pack env) (SuperCart.foreach listType (unpack env))
end

154
src/codegen/secureuml_cartridge.sml
View File

@ -50,21 +50,20 @@ end
* Permissions, Roles, and Constraints.
*)
functor SecureUML_Cartridge(structure SuperCart : BASE_CARTRIDGE;
structure D: DESIGN_LANGUAGE)
: SECUREUML_CARTRIDGE =
structure D: DESIGN_LANGUAGE) : SECUREUML_CARTRIDGE =
struct
structure Security = SecureUML(structure Design = D)
type Model = Rep.Classifier list * Security.Configuration
type environment = { model : Model,
PermissionSet : Security.Permission list,
curPermission : Security.Permission option,
curRole : string option,
curConstraint : Rep_OclTerm.OclTerm option,
extension : SuperCart.environment }
PermissionSet : Security.Permission list,
curPermission : Security.Permission option,
curRole : string option,
curConstraint : Rep_OclTerm.OclTerm option,
extension : SuperCart.environment }
fun PermissionSet (env : environment) = (#PermissionSet env)
fun curPermission (env : environment) = (#curPermission env)
fun curRole (env : environment) = (#curRole env)
@ -75,14 +74,14 @@ fun curRole' (env : environment) = Option.valOf (#curRole env)
fun curConstraint' (env : environment) = Option.valOf (#curConstraint env)
fun initEnv model = let val m = Security.parse model
in
{ model = m,
PermissionSet = (#permissions (#2 m)),
curPermission = NONE,
curRole = NONE,
curConstraint = NONE,
extension = SuperCart.initEnv (#1 m) } : environment
end
in
{ model = m,
PermissionSet = (#permissions (#2 m)),
curPermission = NONE,
curRole = NONE,
curConstraint = NONE,
extension = SuperCart.initEnv (#1 m) } : environment
end
(* unpack : environment -> SuperCart.environment *)
fun unpack (env : environment) = #extension env
@ -90,19 +89,19 @@ fun unpack (env : environment) = #extension env
(* pack : environment -> SuperCart.environment -> environment *)
fun pack (env: environment) (new_env : SuperCart.environment)
= { model = #model env,
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = #curRole env,
curConstraint = #curConstraint env,
extension = new_env}
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = #curRole env,
curConstraint = #curConstraint env,
extension = new_env}
(* Helper functions that get the SuperCartridge's needed environment values *)
fun getModel (env : environment) = #model env
fun getModel (env : environment) = #model env
fun curClassifier (env : environment) = SuperCart.curClassifier (unpack env)
fun curAttribute (env : environment) = SuperCart.curAttribute (unpack env)
fun curOperation (env : environment) = SuperCart.curOperation (unpack env)
fun curArgument (env : environment) = SuperCart.curArgument (unpack env)
fun curAttribute (env : environment) = SuperCart.curAttribute (unpack env)
fun curOperation (env : environment) = SuperCart.curOperation (unpack env)
fun curArgument (env : environment) = SuperCart.curArgument (unpack env)
fun name_of_role r = r
@ -114,67 +113,74 @@ fun name_of_role r = r
* might override some lookup entries of the base cartridge
*)
fun lookup env "permission_name" = #name (curPermission' env)
| lookup env "role_name" = name_of_role (curRole' env)
| lookup env "constraint" = Ocl2String.ocl2string false (curConstraint' env)
| lookup env "role_name" = name_of_role (curRole' env)
| lookup env "constraint" = Ocl2String.ocl2string false (curConstraint' env)
| lookup env s = SuperCart.lookup (unpack env) s
(********** ADDING IF-CONDITION TYPE *****************************************)
fun test env "first_permission" = (curPermission' env = hd (PermissionSet env))
| test env "first_role" = (curRole' env = hd (#roles (curPermission' env)))
| test env "first_constraint" = (curConstraint' env
= hd (#constraints (curPermission' env)))
| test env "last_permission" = (curPermission' env
= List.last (PermissionSet env))
| test env "last_role" = (curRole' env
= List.last (#roles (curPermission' env)))
| test env "last_constraint" = (curConstraint' env
= List.last (#constraints (curPermission' env)))
| test env "first_constraint" = (curConstraint' env = hd (#constraints (curPermission' env)))
| test env "last_permission" = (curPermission' env = List.last (PermissionSet env))
| test env "last_role" = (curRole' env = List.last (#roles (curPermission' env)))
| test env "last_constraint" = (curConstraint' env
= List.last (#constraints (curPermission' env)))
| test env s = SuperCart.test (unpack env) s
(********** ADDING FOREACH TYPE **********************************************)
fun foreach_role env
= let val roles = #roles (curPermission' env);
fun env_from_list_item r ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = SOME r ,
curConstraint = NONE,
extension = #extension env } : environment
in
List.map env_from_list_item roles
end
(* FIXME: in the context of a permission, return the roles of this permission.
* outside of such a context, return all roles. *)
fun foreach_role (env:environment)
= let val roles = case #curPermission env
of SOME p => #roles p
| NONE => Security.all_roles (#2 (#model env))
fun env_from_list_item r ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = SOME r ,
curConstraint = NONE,
extension = #extension env } : environment
in
List.map env_from_list_item roles
end
fun foreach_constraint env
= let val cons = #constraints (curPermission' env);
fun env_from_list_item c ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = NONE ,
curConstraint = SOME c,
extension = #extension env } : environment
in
List.map env_from_list_item cons
end
(* FIXME: in the context of a permission, return the constraints of this permission.
* outside of such a context, return all constraints. *)
fun foreach_constraint (env:environment)
= let val cons = case #curPermission env
of SOME p => #constraints p
| NONE => Security.all_constraints (#2 (#model env))
fun env_from_list_item c ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = #curPermission env,
curRole = #curRole env ,
curConstraint = SOME c,
extension = #extension env } : environment
in
List.map env_from_list_item cons
end
(* FIXME (when possible): in the context of a role, return the permissions of this role.
* outside of such a context, return all permissions.*)
fun foreach_permission env
= let val perms = PermissionSet env
fun env_from_list_item p ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = SOME p,
curRole = NONE ,
curConstraint = NONE ,
extension = #extension env } : environment
in
List.map env_from_list_item perms
end
fun env_from_list_item p ={ model = #model env,
PermissionSet = #PermissionSet env,
curPermission = SOME p,
curRole = NONE ,
curConstraint = NONE ,
extension = #extension env } : environment
in
List.map env_from_list_item perms
end
fun foreach "role_list" env = foreach_role env
| foreach "constraint_list" env = foreach_constraint env
| foreach "permission_list" env = foreach_permission env
| foreach listType env = map (pack env)
(SuperCart.foreach listType (unpack env))
| foreach listType env = map (pack env) (SuperCart.foreach listType (unpack env))
end

37
src/codegen/templates/securemova.tpl Normal file
View File

@ -0,0 +1,37 @@
@// base template
@// assumption: all classifiers are classes
@openfile generated/securemova/$classifier_package$.mova
// generated by su4sml GCG - Generic Code Generator
@nl@nl
(create-security-diagram $classifier_package$) @nl
@foreach permission_list
(insert-permission $classifier_package$ : $permission_name$ ) @nl
@end
@// FIXME: insert-permission-assignment
@foreach role_list
(insert-role $classifier_package$ : $role_name$) @nl
@end
@// FIXME: insert-role-hierarchy
@foreach entity_list
(insert-entity $classifier_package$ : $entity_name$) @nl
@end
@foreach constraint_list
(insert-authorization-constraint $classifier_package$: auth1 )
@end
@// FIXME: insert-attribute
@// FIXME: insert-entity-update et al.
@// FIXME: insert-authorization-constraint
@// FIXME: insert-authorization-constraint-assignment

16
src/rep_ocl.sml
View File

@ -25,18 +25,18 @@
(** Repository datatypes and helper functions for UML/OCL types. *)
signature REP_OCL_TYPE =
sig
type Path = string list
datatype OclType = Integer | Real | String | Boolean | OclAny
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType
| Classifier of Path | OclVoid | DummyT | TemplateParameter of string
val string_of_OclType : OclType -> string
val string_of_path : Path -> string
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType
| Classifier of Path | OclVoid | DummyT | TemplateParameter of string
val string_of_OclType : OclType -> string
val string_of_path : Path -> string
val pathstring_of_path: Path -> string
val is_Classifier : OclType -> bool
val is_Classifier : OclType -> bool
val is_Collection : OclType -> bool
end

26
src/rep_parser.sml
View File

@ -344,19 +344,19 @@ fun transform_classifier t (XMI.Class {xmiid,name,isActive,visibility,isLeaf,
val checked_invariants = filter_exists t invariant
in
Rep.Class {name = (* path_of_classifier *) (find_classifier_type t xmiid),
parent = case filtered_parents
of [] => NONE
| xs => SOME ((* path_of_classifier *) (hd xs)),
attributes = map (transform_attribute t) attributes,
operations = map (transform_operation t) operations,
invariant = map ((transform_constraint t) o
(find_constraint t)) checked_invariants,
associationends = map (transform_aend t)
(find_aends t xmiid),
stereotypes = map (find_stereotype t) stereotype,
interfaces = nil, (* FIX *)
activity_graphs = List.concat [map (transform_activitygraph t) activity_graphs,
map (transform_statemachine t) state_machines],
parent = case filtered_parents
of [] => NONE
| xs => SOME ((* path_of_classifier *) (hd xs)),
attributes = map (transform_attribute t) attributes,
operations = map (transform_operation t) operations,
invariant = map ((transform_constraint t) o
(find_constraint t)) checked_invariants,
associationends = map (transform_aend t)
(find_aends t xmiid),
stereotypes = map (find_stereotype t) stereotype,
interfaces = nil, (* FIX *)
activity_graphs = List.concat [map (transform_activitygraph t) activity_graphs,
map (transform_statemachine t) state_machines],
thyname = NONE}
end
| transform_classifier t (XMI.AssociationClass {xmiid,name,isActive,visibility,

5
src/rep_su2holocl.sml
View File

@ -452,14 +452,13 @@ fun add_operations c =
visibility=public}
val destructor = {name="delete",
precondition=nil,
(* post: self.oclIsUndefined() *)
(* FIXME: and self@pre->modifiedOnly() *)
(* 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,

3
src/secure_uml.sml
View File

@ -33,6 +33,7 @@ sig
include SECURITY_LANGUAGE
type Role
val all_roles : Configuration -> Role list
val all_constraints: Configuration -> Rep_OclTerm.OclTerm list
val constraints_of : Permission -> Rep_OclTerm.OclTerm list
val roles_of: Permission -> Role list
end
@ -82,6 +83,8 @@ fun roles_of (x:Permission) = #roles x
fun actions_of (p:Permission) = #actions p
fun all_roles (c:Configuration) = #roles c
fun all_constraints (c:Configuration) = List.concat (List.map constraints_of (#permissions c))
(** test whether a1 is (transitively) a subordinated_action of a2 *)
fun is_contained_in a1 a2 = (a1 = a2) orelse
List.exists (is_contained_in a1)

22
src/su4sml.cm
View File

@ -35,25 +35,3 @@ Group is
xmltree_writer.sml
xmi_idtable.sml
ocl2string.sml
codegen/compiler/compiler_ext.sig
codegen/compiler/smlnj.sml
codegen/gcg_library.sml
codegen/gcg_helper.sml
codegen/tpl_parser.sml
codegen/cartridge.sig
codegen/base_cartridge.sml
codegen/c#_cartridge.sml
codegen/c#_net1_cartridge.sml
codegen/java_cartridge.sml
codegen/junit_cartridge.sml
codegen/secureuml_cartridge.sml
codegen/design_cartridge.sig
codegen/componentuml_cartridge.sml
codegen/SM_helper.sml
codegen/stateMachineTypes.sml
codegen/stringHandling.sml
codegen/stateMachine.sml
"codegen/c#sm_cartridge.sig"
"codegen/c#sm_cartridge.sml"
codegen/gcg_core.sml
codegen/codegen.sml