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 |