(* CONFLICT DETECTION PROGRAM FOR FIREWALLS                         *)
(* Modified version of the file extracted from the Coq development  *)
(* Venanzio Capretta, June 2008                                     *)
(* See V. Capretta, B. Stepien, A. Felty, and S. Matwin,            *)
(* "Formal correctness of conflict detection for firewalls",        *)
(* Proceedings of FMSE 2007, pp. 22-30                              *)

(* Changes: use ML native types instead of the extracted inductive types *)
(*          some fixing of the notation                                  *)
(*          tail-recursive version of rrs_conflicts and conflicts_aux    *)

type ip_address = int

(** val ip : int -> int -> int -> int -> ip_address **)
(* Different from the Coq version, because we use *)
(* int for IP addresses in place of four bytes    *)

let ip z1 z2 z3 z4 = 
  (z1 lsl 24) + (z2 lsl 16) + (z3 lsl 8)  + z4

type ip_range = { ip_base : ip_address; ip_mask : ip_address }

(** val ip_address_bool : ip_range -> ip_range -> bool **)
(* Simpler than the Coq version because we can apply bitwise *)
(* operations directly on the IP addresses                   *)
let ip_address_bool ip1 ip2 =
  let { ip_base = ipb1; ip_mask = ipm1 } = ip1 in
  let { ip_base = ipb2; ip_mask = ipm2 } = ip2 in
    let m = (ipm1 lor ipm2) in (ipb1 lor m)=(ipb2 lor m)

type action =
  | Permit
  | Deny

type protocol =
  | Udp
  | Tcp

type port_number = int

type pn_interval = port_number*port_number

type access_rule = { r_action : action;
                     r_protocol : protocol;
                     r_source_ip : ip_range;
                     r_source_pn : pn_interval;
                     r_dest_ip : ip_range;
                     r_dest_pn : pn_interval }

type rule_set = access_rule list

(** val action_bool : action -> action -> bool **)

let action_bool a1 a2 = a1=a2

(** val protocol_bool : protocol -> protocol -> bool **)

let protocol_bool pt1 pt2 = pt1=pt2

(** val pn_bool : pn_interval -> pn_interval -> bool **)

let pn_bool pn1 pn2 = 
  let (x1, y1) = pn1 in
  let (x2, y2) = pn2 in
    ((x1 <= y1) && (x2 <= y2)) &&
    ((x1 <= y2) && (x2 <= y1))

(** val conflict_check : access_rule -> access_rule -> bool **)

let conflict_check r1 r2 =
  let { r_action = a1;
        r_protocol = pt1; 
        r_source_ip = sip1;
        r_source_pn = spn1; 
        r_dest_ip = dip1; 
        r_dest_pn = dpn1 } = r1
  in
  let { r_action = a2;
        r_protocol = pt2;
        r_source_ip = sip2;
        r_source_pn = spn2; 
        r_dest_ip = dip2;
        r_dest_pn = dpn2 } = r2
  in if (action_bool a1 a2)
     then false
     else (protocol_bool pt1 pt2) &&
          (ip_address_bool sip1 sip2) &&
          (pn_bool spn1 spn2) &&
          (ip_address_bool dip1 dip2) &&
          (pn_bool dpn1 dpn2)

(** val rrs_conflicts : int -> (int*int) list -> int ->
                        access_rule -> rule_set ->
                        (int*int) list **)
(* Slightly different from the Coq version : tail recursive *)

let rec rrs_conflicts i l n r = function
  | [] -> l
  | rh::rt -> if conflict_check r rh 
              then rrs_conflicts i ((i, n)::l) (n+1) r rt
              else rrs_conflicts i l (n+1) r rt

(** val conflicts_aux : (int*int) list -> int -> rule_set ->
                        (int*int) list **)
(* Slightly different from the Coq version : tail recursive *)

let rec conflicts_aux l n = function
  | [] -> l
  | r::rs' ->
       (conflicts_aux (rrs_conflicts n l (n+1) r rs') (n+1) rs')

(** val conflicts : rule_set -> (int, int) prod list **)

let find_conflicts rs =
  conflicts_aux [] 0 rs