Source file securityAnnotations.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
open Utils
open Prog

(* Abstract syntax for security annotations *)
type simple_level = Public | Secret | Named of Name.t

let named n = Named n

type level = { normal : simple_level; speculative : simple_level }

let diag d = { normal = d; speculative = d }
let public = diag Public
let transient = { normal = Public; speculative = Secret }
let secret = diag Secret

type typ = Msf | Direct of level | Indirect of { ptr : level; value : level }

let direct d = Direct d

type typs = typ list
type signature = { arguments : typs; results : typs }

let get_nth_argument n { arguments; _ } = List.nth_opt arguments n
let get_nth_result n { results; _ } = List.nth_opt results n

(** Pretty-printing *)
module PP = struct
  open Format

  let simple_level fmt = function
    | Public -> fprintf fmt "public"
    | Secret -> fprintf fmt "secret"
    | Named n -> fprintf fmt "%s" n

  let level fmt = function
    | { normal = Public; speculative = Secret } -> fprintf fmt "transient"
    | { normal = n; speculative = s } ->
        if n = s then simple_level fmt n
        else
          fprintf fmt "{ normal: %a, speculative: %a }" simple_level n
            simple_level s

  let typ fmt = function
    | Msf -> fprintf fmt "msf"
    | Direct t -> level fmt t
    | Indirect { ptr; value } ->
        fprintf fmt "{ ptr: %a, val: %a }" level ptr level value

  let typs fmt = function
    | [] -> fprintf fmt "()"
    | ts -> fprintf fmt "@[<h>%a@]" (pp_list "@ ×@ " typ) ts

  let signature fmt { arguments; results } =
    fprintf fmt "%a → %a" typs arguments typs results
end

(** Parsing *)
module Parse = struct
  open Angstrom

  let ws =
    skip_while (function
      | '\x20' | '\x0a' | '\x0d' | '\x09' -> true
      | _ -> false)

  let ident =
    take_while1 (function 'a' .. 'z' | '_' | 'A' .. 'Z' -> true | _ -> false)
    >>= fun hd ->
    take_while (function
      | 'a' .. 'z' | '_' | 'A' .. 'Z' | '0' .. '9' -> true
      | _ -> false)
    >>= fun tl -> return (hd ^ tl)

  let arrow = (string "->" <|> string "→") *> ws
  let times = char '*' *> ws <|> string "×" *> ws

  let simple_level =
    string "public" *> ws *> return Public
    <|> string "secret" *> ws *> return Secret
    <|> lift named (ident <* ws)

  (** Accepts a “key: value” pair where the key can be abbreviated by its first character. *)
  let labelled ~(key : string) value =
    char key.[0]
    *> option "" (string String.(sub key 1 (length key - 1)))
    *> ws *> char ':' *> ws *> value
    <* ws

  let level =
    char '{' *> ws
    *> ( labelled ~key:"normal" simple_level >>= fun normal ->
         char ',' *> ws *> labelled ~key:"speculative" simple_level <* ws
         >>= fun speculative -> return { normal; speculative } )
    <* char '}' <* ws
    <|> string "transient" *> ws *> return transient
    <|> lift diag simple_level

  let typ =
    char '{' *> ws
    *> ( labelled ~key:"ptr" level >>= fun ptr ->
         char ',' *> ws *> labelled ~key:"val" level >>= fun value ->
         return (Indirect { ptr; value }) )
    <* char '}' <* ws
    <|> string "msf" *> ws *> return Msf
    <|> lift direct level

  let typs =
    char '(' *> ws *> sep_by times typ <* char ')' <|> sep_by1 times typ

  let signature =
    ws *> typs >>= fun arguments ->
    ws *> arrow *> typs >>= fun results -> return { arguments; results }

  let string s =
    match parse_string ~consume:All signature s with
    | Ok v -> Some v
    | Error rule ->
        warning Always Location.i_dummy "ill-formed security signature (%s): %s"
          rule s;
        None
end

let get_sct_signature a =
  Option.bind (Annotations.get "sct" a) (function
    | Some { pl_desc = Astring s; _ } -> Parse.string s
    | _ -> None)