module Policy: sig .. end
Origin separation policy
val label_input : input_event -> Level.level
label_input input assigns a security level to an input event input
val label_output : output_event -> Level.level
label_output output assigns a security level to output event output
val pi : Level.level -> input_event -> Policyfun.input_event_pi
pi label input projection function of input event input to a level label
val ro : input_event -> Level.level list
ro input defines a of additional levels for input input