44 lines
1.1 KiB
OCaml
44 lines
1.1 KiB
OCaml
|
module IFC = struct
|
||
|
(*
|
||
|
"Principals" are people (or hosts, or organizations) that may have
|
||
|
different access to information. It's described here by a string;
|
||
|
each principal has a unique string.
|
||
|
*)
|
||
|
type principal = string
|
||
|
|
||
|
(*
|
||
|
Labels represent who is allowed to have access to a certain piece
|
||
|
of information. Labels form a lattice, with Public at the bottom and
|
||
|
Secret at the top.
|
||
|
|
||
|
Every time information flows through the program,
|
||
|
it must be checked to make sure that it's not revealing information
|
||
|
when it isn't allowed to.
|
||
|
|
||
|
For example,
|
||
|
*)
|
||
|
type label =
|
||
|
(* a list of principals that have access to the information described
|
||
|
by this label *)
|
||
|
| LCanRead of principal list
|
||
|
|
||
|
(* join of 2 labels *)
|
||
|
| LJoin of label * label
|
||
|
|
||
|
(* bottom of the lattice *)
|
||
|
| LPublic
|
||
|
|
||
|
(* base type of bytes *)
|
||
|
type bytes =
|
||
|
(* a literal string *)
|
||
|
| BLit of string
|
||
|
(* 2 sets of byte-strings concatenated *)
|
||
|
| BConcat of bytes * bytes
|
||
|
(* cryptographically random set of bytes *)
|
||
|
| BRand of principal
|
||
|
end
|
||
|
|
||
|
module type CryptoPrims = sig
|
||
|
(* A function for generating a random nonce of n bytes *)
|
||
|
(* val rand : *)
|
||
|
end
|