hphp/hack/src/ifc/ifc_security_lattice.ml

   1 (*
   2  * Copyright (c) 2015, Facebook, Inc.
   3  * All rights reserved.
   4  *
   5  * This source code is licensed under the MIT license found in the
   6  * LICENSE file in the "hack" directory of this source tree.
   7  *
   8  *)
   9
  10 open Hh_prelude
  11 open Ifc_types
  12
  13 (* This file contains code related to the security lattice we use to
  14  * check our constraint results against.
  15  *)
  16
  17 exception Invalid_security_lattice
  18
  19 let parse_policy pos purpose_str =
  20   match String.uppercase purpose_str with
  21   | "PUBLIC" -> Pbot pos
  22   | "PRIVATE" -> Ptop pos
  23   | purpose -> Ppurpose (pos, purpose)
  24
  25 (* Parses a Hasse diagram written in a ';' separated format,
  26  * e.g., "A < B; B < C; A < D"
  27  *)
  28 let parse_exn str =
  29   let pos = PosSet.empty in
  30   String.filter ~f:(fun chr -> not @@ Char.equal ' ' chr) str
  31   |> String.split ~on:';'
  32   |> (fun xs ->
  33        if List.equal String.equal xs [""] then
  34          []
  35        else
  36          xs)
  37   |> List.map ~f:(fun str ->
  38          match String.lsplit2 ~on:'<' str with
  39          | Some (l, r) -> (parse_policy pos l, parse_policy pos r)
  40          | None -> raise Invalid_security_lattice)
  41   |> FlowSet.of_list
  42
  43 (* A naive implementation of transitive closure *)
  44 let rec transitive_closure set =
  45   let immediate_consequence (x, y) set =
  46     let add (y', z) set =
  47       if equal_policy y y' then
  48         FlowSet.add (x, z) set
  49       else
  50         set
  51     in
  52     FlowSet.fold add set set
  53   in
  54   let new_set = FlowSet.fold immediate_consequence set set in
  55   if FlowSet.cardinal new_set = FlowSet.cardinal set then
  56     set
  57   else
  58     transitive_closure new_set
  59
  60 let mk_exn str = parse_exn str |> transitive_closure