module Policyfun: sig .. end
All functions for assigning security levels to inputs and outputs.
type
A type of input event with a special Suppress event
Operations on security levels
val leq : Level.level -> Level.level -> bool
leq l1 l2 defines whether security level l1 is less or equal than the security level l2
val domain_of_url : url -> domain option
domain_of_url u defines a domain of url u
val level_of_url : url -> Level.level
level_of_url u defines a level of url as M(domain)
val insert_new_level_acc : Level.level -> Level.level list -> Level.level list -> Level.level list
insert_new_level_acc lev ls acc is an auxiliary function to insert a new level lev into a list of levels ls, acc is an accumulative list assuming that lev is not in the list ls.
val insert_new_level : Level.level -> Level.level list -> Level.level list
insert_new_level lev ls inserts a new level lev into a list of levels ls using insert_new_level_acc
val insert_levels : Level.level list -> Level.level list -> Level.level list
insert_levels all_ls ls inserts list of levels ls into a list all_ls assuming that all_ls does not contain any level from list ls.
val levels_from_domains_acc : domain list -> Level.level list -> Level.level list
levels_from_domains_acc domains levels is an auxiliary function that builds a list of levels levels from domains domains
val levels_from_domains : domain list -> Level.level list
levels_from_domains domains builds a list of levels from domains domains using levels_from_domains_acc
Projections functions
val project_doclist : domain -> doc list -> doc list -> doc list
project_doclist dom doclist doclist' builds a projection of the doc list doclist on the domain dom. the result is doc list doclist'.
val proj : domain -> file_data -> file_data
proj dom body builds a projection of the body of the receive event body to the domain dom
val add_domains : doc list -> domain list -> domain list
add_domains doclist domains adds a list of domains of the remote script urls from the list of docs doclist into the list of domains domains.
val build_new_domains : file_data -> domain list
build_new_domains body in case body is an Html_file, builds a list of domains of the remote scripts in the body using function add_domains. Otherwise return an empty list.
val domain_of_net_connection : net_connection -> domain
domain_of_net_connection nc returns a domain of a Net_connection nc.
Printing and to_string operations
val string_of_string_list : string list -> string -> string
string_of_string_list ls acc transforms a string list ls to a string acc in a reversed order, e.g. "a", "b", "c" to "cba"
val string_of_domain : domain -> string
string_of_domain d transforms a domain d into a string
val string_of_level : Level.level -> string
string_of_level l transforms a security level l to a string
val string_of_url : url -> string
string_of_url url transforms a url url into a string, if url is empty, transforms to "blank".
val string_of_output : output_event -> string
string_of_output output transforms an output output to a string
val print_outputs : output_event list -> unit
print_outputs oes recursively prints a list of outputs oes
val print_levels : Level.level list -> unit
print_levels ls recursively prints a list of levels ls