(**************************************************************** Michel St-Martin and Amy Felty December 2015, Coq version V8.4 A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, Michel St-Martin and Amy P. Felty, In Proceedings of the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), January 2016. ***************************************************************) Require Export Rules. Definition rule_set := list rule. (* Projection on lists, without default value. *) Fixpoint Nth (A:Set)(l:list A){struct l}: forall i:nat, (i A := match l return forall i:nat, (i A with nil => fun i H => False_rec A (lt_n_O i H) | cons a l => fun i => match i return (i A with 0%nat => fun H => a | S i => fun H => Nth A l i (lt_S_n i (length l) H) end end. Implicit Arguments Nth [A]. Lemma Nth_proof_independent: forall (A:Set)(l:list A)(i:nat)(H1 H2:(iProp): Prop := dep_pair: forall (a:A)(b:B a), dep_and A B. Notation " { A ** B } " := (dep_and A B). (* Some small lemmas about order on natural numbers not provided by the library. *) Lemma lt_0_lt_minus: forall n m:nat, lt n m -> lt 0 (m-n). Proof. intros n m H. apply plus_lt_reg_l with n. rewrite plus_0_r. rewrite le_plus_minus_r. exact H. apply lt_le_weak. exact H. Qed. Lemma minus_S_pred: forall n m:nat, (n-(S m))%nat = pred (n-m). Proof. induction n; simpl. trivial. intros m; case m; simpl. symmetry; apply minus_n_O. exact IHn. Qed. (* Finds conflicts between a rule and a rule set: i = position of the rule r in the original rule set n = position of the first rule of rs in the original rule set *) Fixpoint rrs_conflicts (i n:nat)(r:rule)(rs:rule_set){struct rs}: list (nat*nat) := match rs with nil => nil | (cons rh rt) => if (conflict_check r rh) then (i,n)::(rrs_conflicts i (S n) r rt) else (rrs_conflicts i (S n) r rt) end. (* Find conflicts (assuming that rs starts with rule number n *) Fixpoint conflicts_aux (n:nat)(rs:rule_set){struct rs}: list (nat*nat) := match rs with nil => nil | (cons r rs') => (rrs_conflicts n (S n) r rs') ++ (conflicts_aux (S n) rs') end. (* The conflict-detection program. *) Definition find_conflicts: rule_set -> list (nat*nat) := conflicts_aux 0. (* rrs_conflict_res r rs n means that there is a conflict between r and the nth rule of rs *) Inductive rrs_conflict_rel (r:rule): rule_set -> nat -> Prop := rrs_conflict_head: forall (rh:rule)(rt:rule_set), rule_conflict r rh -> rrs_conflict_rel r (rh::rt) 0 | rrs_conflict_tail: forall (rh:rule)(rt:rule_set)(n:nat), rrs_conflict_rel r rt n -> rrs_conflict_rel r (rh::rt) (S n). Lemma rrs_conflicts_n_le_j: forall (i i':nat)(r:rule)(rs:rule_set)(j n:nat), In (i,j) (rrs_conflicts i' n r rs) -> (n<=j)%nat. Proof. intros i i' r rs; elim rs; simpl. intros j n H; elim H. intros r0 rs' IH j n. case (conflict_check r r0); simpl. intros H; case H; clear H; intro H. injection H; clear H; intros Hi Hj. rewrite Hi; apply le_n. apply le_Sn_le; apply IH; exact H. intro H; apply le_Sn_le; apply IH; exact H. Qed. (* Soundness *) Lemma rrs_conflicts_soundness: forall (i i':nat)(r:rule)(rs:rule_set)(j n:nat), In (i,j) (rrs_conflicts i' n r rs) -> i'=i /\ rrs_conflict_rel r rs (j-n)%nat. Proof. intros i i' r rs; elim rs; simpl. intros j n H; elim H. intros r0 rs' IH j n. generalize (conflict_check_soundness r r0). case (conflict_check r r0); simpl. intros H0 H; case H; clear H; intro H. injection H; clear H; intros H1 H2. split. exact H2. rewrite H1; rewrite <- minus_n_n. apply rrs_conflict_head. apply H0; trivial. generalize (IH j (S n) H); intros [IH1 IH2]. split. exact IH1. rewrite (S_pred (j-n) 0). apply rrs_conflict_tail. rewrite <- minus_S_pred. exact IH2. apply lt_0_lt_minus. red; eapply rrs_conflicts_n_le_j; apply H. intros _ H; generalize (IH j (S n) H); intros [IH1 IH2]. split. exact IH1. rewrite (S_pred (j-n) 0). apply rrs_conflict_tail. rewrite <- minus_S_pred. exact IH2. apply lt_0_lt_minus. red; eapply rrs_conflicts_n_le_j; apply H. Qed. Definition rs_conflict: rule_set -> nat -> nat -> Prop := fun rs i j => {(i < (length rs))%nat ** fun Hi => {(j < (length rs))%nat ** fun Hj => (rule_conflict (Nth rs i Hi) (Nth rs j Hj))}}. Lemma rrs_conflict_rel_rs_conflict_aux: forall (r:rule)(rs:rule_set)(m:nat), rrs_conflict_rel r rs m -> forall n:nat, (n = S m) -> rs_conflict (r::rs) 0 n. Proof. intros r rs m H; elim H. intros rh rt Hr n Hn1. rewrite Hn1; red. cut (0 rrs_conflict_rel r rs (pred n) -> rs_conflict (r::rs) 0 n. Proof. intros r rs n Hn H; apply rrs_conflict_rel_rs_conflict_aux with (m:=pred n). exact H. apply S_pred with (m:=0%nat). exact Hn. Qed. Lemma rs_conflict_cons: forall (r:rule)(rs:rule_set)(i j:nat), rs_conflict rs i j -> rs_conflict (r::rs) (S i) (S j). Proof. intros r rs i j [H1 [H2 H3]]; red. exists (lt_n_S _ _ H1). exists (lt_n_S _ _ H2). simpl. rewrite Nth_proof_independent with (H2:=H1). rewrite Nth_proof_independent with (H2:=H2). exact H3. Qed. Lemma conflicts_aux_le: forall (rs:rule_set)(i j n:nat), In (i,j) (conflicts_aux n rs) -> (n<=i)%nat /\ (n<=j)%nat. Proof. intro rs; elim rs; simpl. intros i j n H; elim H. clear rs; intros r rs IH i j n H. case in_app_or with (1:=H); clear H; intro H. split. generalize (rrs_conflicts_soundness _ _ _ _ _ _ H); intros [Hi _]. rewrite Hi; apply le_n. apply lt_le_weak. apply rrs_conflicts_n_le_j with (1:=H). generalize (IH _ _ _ H); intros [H1 H2]. split; apply lt_le_weak; assumption. Qed. Lemma conflicts_aux_soundness: forall (rs:rule_set)(n i j:nat), In (i,j) (conflicts_aux n rs) -> rs_conflict rs (i-n)%nat (j-n)%nat. Proof. intros rs; elim rs; simpl. intros n i j H; elim H. intros r rs' IH n i j H. case in_app_or with (1:=H); clear H; intro H. generalize (rrs_conflicts_soundness i n r rs' j (S n) H); intros [Hi HH]. rewrite <- Hi; rewrite <- minus_n_n. apply rrs_conflict_rel_rs_conflict. apply lt_0_lt_minus. red. apply rrs_conflicts_n_le_j with (1:=H). rewrite <- minus_S_pred. exact HH. generalize (conflicts_aux_le _ _ _ _ H); intros [H1 H2]. rewrite (S_pred (i-n) 0). rewrite (S_pred (j-n) 0). apply rs_conflict_cons. rewrite <- (minus_S_pred i n); rewrite <- (minus_S_pred j n). apply IH; exact H. apply lt_0_lt_minus; exact H2. apply lt_0_lt_minus; exact H1. Qed. Theorem conflicts_soundness: forall (rs:rule_set)(i j:nat), In (i,j) (find_conflicts rs) -> rs_conflict rs i j. Proof. intros rs i j H. rewrite (minus_n_O i); rewrite (minus_n_O j). apply conflicts_aux_soundness. exact H. Qed. (* Completeness *) Lemma Nth_singleton: forall (A:Set)(a:A)(i:nat)(hi:(i<1)%nat), Nth (a::nil) i hi = a. Proof. intros A a i; case i; simpl. trivial. intros i' hi'. red in hi'. elim (le_Sn_O i'). apply le_S_n; exact hi'. Qed. Lemma rule_permit_no_deny: forall (rl:rule)(r: list reqValue), rule_permit r rl -> rule_deny r rl -> False. Proof. intros rl r [H1 _] [H2 _]. rewrite H1 in H2. discriminate H2. Qed. Lemma no_rule_conflict_self: forall r:rule, ~ (rule_conflict r r). Proof. intros r [q H]; case H; intros [H1 H2]; apply rule_permit_no_deny with r q; assumption. Qed. Lemma rs_conflict_singleton: forall (r:rule)(i j:nat), ~ (rs_conflict (r::nil) 0 j). Proof. intros r i j [h1 [h2 H]]. rewrite Nth_singleton in H. rewrite Nth_singleton in H. apply no_rule_conflict_self with r; exact H. Qed. Lemma rrs_conflicts_S: forall (r:rule)(rs:rule_set)(n j m:nat), In (n, j) (rrs_conflicts n m r rs) -> In (n, S j) (rrs_conflicts n (S m) r rs). Proof. intros r rs; elim rs; simpl. trivial. clear rs; intros r1 rs IH n j m; case (conflict_check r r1). intro H; case H. intro Heq. replace m with (snd (n,m)). rewrite Heq; simpl. left; trivial. trivial. intro H'. right. apply IH. exact H'. apply IH. Qed. Lemma conflicts_0_Sj_rrs_conflicts: forall (n:nat)(r:rule)(rs:rule_set)(j:nat), rs_conflict (r::rs) 0 (S j) -> In (n,j+(S n))%nat (rrs_conflicts n (S n) r rs). Proof. intros n r rs j; generalize rs; clear rs; elim j. intro rs; case rs. intro H; elim (rs_conflict_singleton r 0 1 H). clear rs; intros r1 rs. intros [h1 [h2 H]]. simpl in H. simpl. rewrite (conflict_check_completeness). simpl. left; trivial. exact H. clear j; intros j IH. intro rs; case rs. intro H; elim (rs_conflict_singleton r 0 (S (S j)) H). clear rs; intros r1 rs H. simpl. cut (In (n, S (j+S n)) (rrs_conflicts n (S (S n)) r rs)). intro HH. case (conflict_check r r1). right. exact HH. exact HH. apply rrs_conflicts_S. apply IH. case H; clear H; intros h1 [h2 H]. simpl in h1; simpl in h2; simpl in H. exists (lt_O_Sn (length rs)). esplit. simpl. apply H. Qed. Lemma conflicts_0_rrs_conflicts: forall (n:nat)(r:rule)(rs:rule_set)(j:nat), (0 rs_conflict (r::rs) 0 j -> In (n,j+n)%nat (rrs_conflicts n (S n) r rs). Proof. intros n r rs j Hj; rewrite S_pred with (m:=0%nat)(1:=Hj). intro H. rewrite plus_Sn_m; rewrite plus_n_Sm. apply conflicts_0_Sj_rrs_conflicts. exact H. Qed. Lemma rs_conflict_S: forall (r:rule)(rs:rule_set)(i j:nat), rs_conflict (r::rs) (S i) (S j) -> rs_conflict rs i j. Proof. intros r rs i j [Hi [Hj H]]. simpl in Hi; simpl in Hj; simpl in H. esplit. esplit. apply H. Qed. Lemma conflicts_aux_completeness: forall (i j:nat), (i forall (n:nat)(rs:rule_set), rs_conflict rs i j -> In (i+n,j+n)%nat (conflicts_aux n rs). Proof. intro i; elim i. intros j h n rs; case rs. intros [Hi H]. elim lt_n_O with O. exact Hi. clear rs; intros r rs H; simpl. apply in_or_app. left. apply conflicts_0_rrs_conflicts. exact h. exact H. clear i; intros i IH j h. rewrite (S_pred j (S i) h). intros n rs; case rs. intros [Hi H]. elim lt_n_O with (S i). exact Hi. clear rs; intros r rs Hj; simpl. apply in_or_app; right. rewrite plus_n_Sm with i n. rewrite plus_n_Sm with (pred j) n. apply IH with (j:=pred j)(n:=S n). apply lt_pred. exact h. apply rs_conflict_S with r. exact Hj. Qed. Theorem conflicts_completeness: forall (rs:rule_set)(i j:nat), (i rs_conflict rs i j -> In (i,j) (find_conflicts rs). Proof. intros rs i j Hlt H; unfold find_conflicts; simpl. rewrite <- plus_0_r with (n:=i); rewrite <- plus_0_r with (n:=j). apply conflicts_aux_completeness. exact Hlt. exact H. Qed.