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

typecheckes, but not sure if working... 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@4433 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Jürgen Doser 2006-04-24 10:19:08 +00:00
parent 329b121a63
commit 24fc67da90
15 changed files with 65 additions and 182 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/codegen/codegen.cm
View File

@ -7,6 +7,7 @@ Group is
#endif
compiler/compiler_ext.sig
compiler/smlnj.sml
security_cartridge.sig
gcg_library.sml
gcg_helper.sml
tpl_parser.sig

13
src/codegen/codegen.sml
View File

@ -27,11 +27,16 @@ OS.FileSys.chDir "../../../src";
structure Codegen = struct
structure Base_Gcg = GCG_Core (Base_Cartridge);
structure CSharp_Gcg = GCG_Core (CSharp_Cartridge(Base_Cartridge));
structure CSharpSecure_Gcg = GCG_Core (CSharp_Cartridge(SecureUML_Cartridge(Base_Cartridge)));
structure Base_Gcg = GCG_Core (Base_Cartridge)
structure CSharp_Gcg = GCG_Core (CSharp_Cartridge(Base_Cartridge))
structure CSharpSecure_Gcg
= GCG_Core (CSharp_Cartridge(SecureUML_Cartridge(structure SuperCart=Base_Cartridge;
structure D=ComponentUML)))
structure CSharp_NET1_Gcg = GCG_Core (CSharp_NET1_Cartridge(Base_Cartridge));
structure CSharpSecure_NET1_Gcg = GCG_Core (CSharp_NET1_Cartridge(SecureUML_Cartridge(Base_Cartridge)));
structure CSharpSecure_NET1_Gcg = GCG_Core (CSharp_NET1_Cartridge(SecureUML_Cartridge(structure SuperCart=Base_Cartridge; structure D=ComponentUML)));
(*
structure Java_Gcg = GCG_Core (Java_Cartridge(Base_Cartridge));
structure JavaSecure_Gcg = GCG_Core (Java_Cartridge(SecureUML_Cartridge(Base_Cartridge)));

10
src/codegen/gcg_core.sml
View File

@ -66,8 +66,7 @@ fun eval s = (print ("<eval>\n");
(* map2EveryOther f l applies f to every other
* element in l starting with the second
(** applies f to every other element in l starting with the second
*)
fun map2EveryOther f [] = []
| map2EveryOther f [a] = [a]
@ -79,11 +78,10 @@ fun substituteVars e s = let val tkl = (Gcg_Helper.joinEscapeSplitted "$") (Gcg_
end
(*
* write is the main function of gcg_core.
* it traverses a templateParseTree and executes the given instructions
(**
* main function of gcg_core.
* traverses a templateParseTree and executes the given instructions
*)
(* write : C.environment -> TemplateTree -> () *)
fun write env (Tpl_Parser.RootNode(l)) = List.app (write env) l
| write env (Tpl_Parser.OpenFileLeaf(file)) = openFile (substituteVars env file)
| write env (Tpl_Parser.EvalLeaf(l)) = let fun collectEval [] = ""

4
src/codegen/gcg_helper.sml
View File

@ -140,10 +140,6 @@ fun is_contained_in a1 (a2 as (SimpleAction _)) = (a1 = a2)
(isSuffix p2 p1) andalso (actionTypes_compatible at1 at2)
end *)
fun is_contained_in a1 a2 = (a1 = a2) orelse
List.exists (fn x=> x=true) ((List.map (is_contained_in a1) (ComponentUML.subordinated_actions a2)))
fun isInPermission a (p:Rep_SecureUML_ComponentUML.Security.Permission) = List.exists (is_contained_in a) (#actions p)
(* fun resource_to_string (s,p) = "("^s^", "^(string_of_path p)^")"

12
src/codegen/secureuml_cartridge.sig
View File

@ -26,17 +26,13 @@ signature SECUREUML_CARTRIDGE =
sig
(* from CARTRIDGE *)
type environment
val initEnv : Rep_SecureUML_ComponentUML.Model -> environment
val lookup : environment -> string -> string
val evalCondition : environment -> string -> bool
val foreach : string -> environment -> environment list
include BASE_CARTRIDGE
(* specific for SECUREUML_CARTRIDGE *)
val curPermissionSet: environment -> Rep_SecureUML_ComponentUML.Security.Permission list option
val curPermission : environment -> Rep_SecureUML_ComponentUML.Security.Permission option
val curRole : environment -> string option
val curConstraint : environment -> Rep_OclTerm.OclTerm option
val isInPermission : Rep_SecureUML_ComponentUML.Security.Design.Action -> Rep_SecureUML_ComponentUML.Security.Permission -> bool
structure Security:SECURITY_LANGUAGE
end

135
src/codegen/secureuml_cartridge.sml
View File

@ -24,18 +24,14 @@
******************************************************************************)
functor SecureUML_Cartridge(SuperCart : BASE_CARTRIDGE) : SECUREUML_CARTRIDGE =
functor SecureUML_Cartridge(structure SuperCart : BASE_CARTRIDGE; structure D: DESIGN_LANGUAGE) : SECURITY_LANGUAGE_CARTRIDGE =
struct
(*
open Rep_SecureUML_ComponentUML.Security
open ComponentUML
open Gcg_Helper
open Ocl2String
*)
type environment = { curPermissionSet: Rep_SecureUML_ComponentUML.Security.Permission list option,
curPermission : Rep_SecureUML_ComponentUML.Security.Permission option,
structure Security = SecureUML(structure Design = D)
type environment = { curPermissionSet: Security.Permission list option,
curPermission : Security.Permission option,
curRole : string option,
curConstraint : Rep_OclTerm.OclTerm option,
extension : SuperCart.environment }
@ -79,56 +75,11 @@ fun curClassifier (env : environment) = SuperCart.curClassifier (unpack env)
fun curAttribute (env : environment) = SuperCart.curAttribute (unpack env)
fun curOperation (env : environment) = SuperCart.curOperation (unpack env)
type permissionContext = {permissions : Rep_SecureUML_ComponentUML.Security.Permission list,
setter_permissions : Rep_SecureUML_ComponentUML.Security.Permission list,
getter_permissions : Rep_SecureUML_ComponentUML.Security.Permission list,
constructor_permissions : Rep_SecureUML_ComponentUML.Security.Permission list,
destructor_permissions : Rep_SecureUML_ComponentUML.Security.Permission list}
fun is_contained_in a1 a2 = (a1 = a2) orelse
List.exists (fn x=> x=true) ((List.map (is_contained_in a1) (D.subordinated_actions a2)))
fun permissionsForAction (e : environment) a
= List.filter (Gcg_Helper.isInPermission a) (#permissions (#2 (getModel e)))
(* computePermissionContext: environment -> permissionContext
* compute Permissions according to actual environment
*)
fun computePermissionContext (env : environment)=
let
fun getAction "set" = ComponentUML.SimpleAction ("update", (ComponentUML.EntityAttribute (Option.valOf(curAttribute env))))
| getAction "get" = ComponentUML.SimpleAction ("read", (ComponentUML.EntityAttribute (Option.valOf(curAttribute env))))
| getAction "execute" = ComponentUML.SimpleAction ("execute", (ComponentUML.EntityMethod (Option.valOf(curOperation env))))
| getAction "create" = ComponentUML.SimpleAction ("create", (ComponentUML.Entity (Option.valOf(curClassifier env))))
| getAction "delete" = ComponentUML.SimpleAction ("delete", (ComponentUML.Entity (Option.valOf (curClassifier env))))
| getAction s = Gcg_Helper.gcg_error ("invalid action_type \""^s^"\" in secureUML_cartridge.computePermissionContext:getAction.")
in
if Option.isSome(curAttribute env) then
{permissions = [],
setter_permissions = (permissionsForAction env (getAction "set")),
getter_permissions = (permissionsForAction env (getAction "get")),
constructor_permissions = [],
destructor_permissions = []
}
else if Option.isSome(curOperation env) then
{permissions = permissionsForAction env (getAction "execute"),
setter_permissions = [],
getter_permissions = [],
constructor_permissions = [],
destructor_permissions = []
}
else if Option.isSome(curClassifier env) then
{permissions = [],
setter_permissions = [],
getter_permissions = [],
constructor_permissions = permissionsForAction env (getAction "create"),
destructor_permissions = permissionsForAction env (getAction "delete")
}
else
{permissions = #permissions (#2 (getModel env)),
setter_permissions = [],
getter_permissions = [],
constructor_permissions = [],
destructor_permissions = []
}
end
fun isInPermission a (p:Security.Permission) = List.exists (is_contained_in a) (#actions p)
fun name_of_role r = r
@ -154,66 +105,7 @@ fun evalCondition (env : environment) "first_permission" = (curPermission' env
(********** ADDING FOREACH TYPE **********************************************)
(* fun foreach_<new_list_type>: environment -> environment list *)
fun foreach_permission (env : environment)
= let val plist = #permissions (computePermissionContext env);
fun env_from_list_item c ={curPermissionSet = SOME plist,
curPermission = SOME c,
curRole = NONE,
curConstraint = NONE,
extension = #extension env
} : environment
in
List.map env_from_list_item plist
end
fun foreach_readPermission (env : environment)
= let val plist = #getter_permissions (computePermissionContext env);
fun env_from_list_item c ={curPermissionSet = SOME plist,
curPermission = SOME c,
curRole = NONE ,
curConstraint = NONE,
extension = #extension env
} : environment
in
List.map env_from_list_item plist
end
fun foreach_updatePermission (env : environment)
= let val plist = #setter_permissions (computePermissionContext env);
fun env_from_list_item c ={curPermissionSet = SOME plist,
curPermission = SOME c,
curRole = NONE ,
curConstraint = NONE,
extension = #extension env
} : environment
in
List.map env_from_list_item plist
end
fun foreach_createPermission (env : environment)
= let val plist = #constructor_permissions (computePermissionContext env);
fun env_from_list_item c ={curPermissionSet = SOME plist,
curPermission = SOME c,
curRole = NONE ,
curConstraint = NONE,
extension = #extension env
} : environment
in
List.map env_from_list_item plist
end
fun foreach_deletePermission (env : environment)
= let val plist = #destructor_permissions (computePermissionContext env);
fun env_from_list_item c ={curPermissionSet = SOME plist,
curPermission = SOME c,
curRole = NONE ,
curConstraint = NONE,
extension = #extension env
} : environment
in
List.map env_from_list_item plist
end
fun foreach_role (env : environment)
= let val roles = #roles (curPermission' env);
@ -240,12 +132,7 @@ fun foreach_constraint (env : environment)
end
fun foreach "permission_list" env = foreach_permission env
| foreach "readPermission_list" env = foreach_readPermission env
| foreach "updatePermission_list" env = foreach_updatePermission env
| foreach "createPermission_list" env = foreach_createPermission env
| foreach "deletePermission_list" env = foreach_deletePermission env
| foreach "role_list" env = foreach_role env
fun foreach "role_list" env = foreach_role env
| foreach "constraint_list" env = foreach_constraint env
(* pass unknown list types to superior cartridge by unpacking environments,
* having SuperCart compute environment list, pack into native environment again*)

19
src/codegen/tpl_parser.sml
View File

@ -46,8 +46,8 @@ datatype TemplateTree = RootNode of TemplateTree list
(* replaceSafely (s,v,x)
* replaces every v in s with x or if v is escaped removes "\"
(**
* replaceSafely (s,v,x) replaces every v in s with x or if v is escaped removes "\"
*)
fun replaceSafely ("",_,_) = ""
| replaceSafely (s,v,x) = let val v_size = size v and
@ -61,8 +61,7 @@ fun replaceSafely ("",_,_) = ""
end
(*
* cleanLine [string]
(**
* splits string into tokens and
* removes space- and tab-characters
*)
@ -104,9 +103,8 @@ fun tokenize line = let val l = joinEscapeSplitted "@" (fieldSplit line #"@");
(hd l)::(itemsUntil isComment (tl l))
end
(*
* getType line
* extracts the type of line
(**
* extracts the type of line.
* line type must be first token in line!
* if no control tag in line -> "text" returned
*)
@ -129,8 +127,7 @@ fun getContent l = let val sl = tokenize l
else String.concat(tl(fieldSplit (String.concat(tl(sl))) #" "))
end
(*
* preprocess [line]
(**
* cleans line, replaces nl and tabs
* so that no space char is left out
*)
@ -165,7 +162,7 @@ fun buildTree (SOME line) = let fun getNode ("text",c) = (TextLeaf(c))::(buil
fun codegen_env _ = getOpt(OS.Process.getEnv "CODEGEN_HOME",".")
(** calls the external cpp ( C PreProcessor)
(** calls the external cpp ( C PreProcessor).
* writes merged template to a file with extension .tmp instead of .tpl
* and returns this file
*)
@ -179,7 +176,7 @@ fun call_cpp file =
(** parse [template-file]
(** parse template-file
* @return the parsed template tree
*)
fun parse file = let val mergedTpl = call_cpp file;

9
src/library.sml
View File

@ -25,7 +25,7 @@
structure library =
struct
infix |>
fun (x |> f) = f x;
(* fun (x |> f) = f x;*)
fun filter (pred: 'a->bool) : 'a list -> 'a list =
@ -91,9 +91,8 @@ exception ERROR;
(* fun error_msg s = writeln(s) *)
fun error s = (print (s^"\n"); raise ERROR);
(* use #1 and #2 instead
fun fst (x, y) = x;
fun snd (x, y) = y;
*)
fun fst (x, y) = x
fun snd (x, y) = y
end

4
src/mds.sig
View File

@ -29,7 +29,7 @@
signature DESIGN_LANGUAGE =
sig
type Resource
eqtype Resource
(* val resource_types: string list *)
@ -64,7 +64,7 @@ sig
type User
val name_of : User -> string
type Permission
eqtype Permission
(* a bit unclear, which of the following we really need *)
val users_of : Permission -> User list

3
src/rep_secure.sml
View File

@ -39,3 +39,6 @@ end
structure Rep_SecureUML_ComponentUML
= Rep_Secure(structure Security = SecureUML(structure Design=ComponentUML))
(* structure Rep_SecureUML_ControllerUML
= Rep_Secure(structure Security = SecureUML(structure Design=ControllerUML))*)

6
src/rep_secureuml.sml
View File

@ -10,7 +10,6 @@ type Role = string
type RoleAssignment = (Subject * Role) list
type RoleHierarchy = (Role * Role) list
(* computes the reflexiv and transitive closure of rh starting from *)
@ -24,8 +23,8 @@ datatype Resource = Entity of Rep_OclType.Path
| EntityAttribute of Rep_OclType.Path
(* | EntityAssociationEnd of Rep.Path ??? *)
(* fun contained_resources e = ... *)
(* FIX: *)
fun contained_resources e = nil
datatype ActionName = Create | Read | Update | Delete | FullAccess | Execute
@ -42,7 +41,6 @@ fun subordinated_actions (SimpleAction _) = nil
(* | subordinated_actions (CompositeAction (_,_)) = ...*)
type Permission = { name: string,
roles: Role list,
constraints: Rep_OclTerm.OclTerm list,

20
src/secure_uml.sml
View File

@ -23,7 +23,7 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
(* SecureUML is a simple security language, based on RBAC, where permissions *)
(** SecureUML is a simple security language, based on RBAC, where permissions *)
(* can be further constrained using OCL: *)
functor SecureUML(structure Design: DESIGN_LANGUAGE):SECURITY_LANGUAGE =
struct
@ -41,13 +41,11 @@ datatype Subject = Group of string * (string list)
type Role = string
type SubjectAssignment = (Subject * (Role list)) list
(* fun actions_of (p:Permission) = #actions p*)
type Permission = {name: string,
roles: Role list,
constraints: Rep_OclTerm.OclTerm list,
actions: Design.Action list }
roles: Role list,
constraints: Rep_OclTerm.OclTerm list,
actions: Design.Action list }
fun actions_of (p:Permission) = #actions p
@ -61,11 +59,11 @@ fun closure_of (x:'a partial_order) = ...
*)
type Configuration = { config_type: Config_Type,
permissions: Permission list,
subjects: Subject list,
(* groups: Group partial_order,*)
roles: Role partial_order,
sa: SubjectAssignment }
permissions: Permission list,
subjects: Subject list,
(* groups: Group partial_order,*)
roles: Role partial_order,
sa: SubjectAssignment }
fun type_of (c:Configuration) = #config_type c

1
src/su4sml-cygwin.mlb
View File

@ -35,5 +35,6 @@ in
xmi2rep.sml
rep_secure.sig
rep_secure.sml
codegen/codegen.mlb
end
end

2
src/su4sml.cm
View File

@ -41,6 +41,7 @@ Group is
codegen/tpl_parser.sig
codegen/tpl_parser.sml
codegen/cartridge.sig
codegen/security_cartridge.sig
codegen/base_cartridge.sig
codegen/base_cartridge.sml
codegen/c#_cartridge.sml
@ -50,3 +51,4 @@ Group is
codegen/gcg_core.sig
codegen/gcg_core.sml
codegen/codegen.sml
codegen/componentuml_cartridge.sml

8
src/xmltree_parser.sml
View File

@ -56,21 +56,23 @@ sig
end =
struct
open library
exception IllFormed of string
(** A name-value pair. *)
type Attribute = (string * string)
(* Tags consist of element names, and a list of attribute name-value pairs *)
(** Tags consist of element names, and a list of attribute name-value pairs. *)
type Tag = string * Attribute list
datatype Tree = Node of Tag * Tree list
| Text of string
val filter_nodes = List.filter (fn Node x => true
| _ => false)
| _ => false)
val filter_text = List.filter (fn Text x => true
| _ => false)
| _ => false)
fun text_of (Text s) = s
| text_of _ = raise IllFormed "text_of called on Node element"