Advertisement
Guest User

RockSalt Diff

a guest
Aug 8th, 2017
145
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Diff 33.13 KB | None
  1. --- FastVerifier.v  2017-05-27 18:45:35.000000000 -0500
  2. +++ FastVerifier_new.v  2017-06-07 19:36:57.000000000 -0500
  3. @@ -114,6 +114,25 @@
  4.            end
  5.        end.
  6.  
  7. +(* --------------------------------- *)
  8. +Fixpoint process_buffer_align (loc: int32) (n: nat) (tokens:list token_id)
  9. +       (curr_res: Int32Set.t * Int32Set.t) :=
  10. +    let (start_instrs, check_list) := curr_res in
  11. +      match tokens with
  12. +        | nil => Some curr_res
  13. +        | _ => (* There are left over bytes in the buffer *)
  14. +          match n with
  15. +            | O => None
  16. +            | S p =>
  17. +       match process_buffer_aux loc n tokens (start_instrs, check_list) with
  18. +           | None => None
  19. +           | Some (start_instrs_new, check_list_new) => process_buffer_align ( loc +32_n Z.to_nat chunkSize) p (skipn (Z.to_nat chunkSize) tokens)
  20. +               (start_instrs_new, check_list_new)
  21. +           end
  22. +       end
  23. +   end.
  24. +(* --------------------------------- *)
  25. +
  26.    (* The idea here is, given a list of int8s representing the code,
  27.       we call process_buffer_aux with n := length of the list;
  28.       since each instruction is at least one byte long, this should
  29. @@ -123,7 +142,7 @@
  30.       at least one byte.
  31.       *)
  32.    Definition process_buffer (buffer: list int8) :=
  33. -    process_buffer_aux (Word.repr 0) (length buffer) (List.map byte2token buffer)
  34. +    process_buffer_align (Word.repr 0) (length buffer) (List.map byte2token buffer)
  35.       (Int32Set.empty, Int32Set.empty).
  36.  
  37.    Definition aligned_bool (a:int32):bool :=
  38. @@ -179,11 +198,18 @@
  39.              (checkJmpTargets check_addrs start_addrs),
  40.             start_addrs)
  41.      end.
  42. -
  43. +(*
  44. +Compute process_buffer_aux (Word.repr 0) (length buffer) (List.map byte2token buffer)
  45. +     (Int32Set.empty, Int32Set.empty).
  46. +Compute (checkProgram (nil) ).
  47. +*)
  48.  End BUILT_DFAS.
  49.  
  50.  Definition ncflow := make_dfa non_cflow_grammar.
  51.  Definition dbranch := make_dfa (alts dir_cflow).
  52.  Definition ibranch := make_dfa (alts nacljmp_mask).
  53. -
  54. +(*
  55. +Check checkProgram.
  56. +Variable initial_state : ParseState_t.
  57. +(*Compute (checkProgram ncflow dbranch ibranch initial_state ( (repr 55) ::nil)).*)  *)
  58.  (*Extraction "fastverif.ml" checkProgram ncflow dbranch ibranch.*)
  59.  
  60.  
  61. --- VerifierCorrectness.v   2017-05-27 18:45:35.000000000 -0500
  62. +++ VerifierCorrectness_new.v   2017-06-07 19:36:57.000000000 -0500
  63. @@ -388,6 +388,12 @@
  64.      FastVerifier.process_buffer non_cflow_dfa dir_cflow_dfa nacljmp_dfa
  65.        initial_state.
  66.  
  67. +(*---------------------------------------*)
  68. +  Definition process_buffer_align :=
  69. +    FastVerifier.process_buffer_align non_cflow_dfa dir_cflow_dfa nacljmp_dfa
  70. +      initial_state.
  71. +(*---------------------------------------------*)
  72. +
  73.    (* Checks whether the memory of s starting at addr_offset is equal
  74.       to buffer *)
  75.    Definition eqMemBuffer (buffer: list int8) (s: rtl_state) (addr_offset: int32) :=
  76. @@ -836,6 +842,15 @@
  77.        int32_to_Z_tac. crush.
  78.    Qed.
  79.  
  80. +  Lemma Int32Set_diff_diff_dichotomy : forall x A B C,
  81. +    Int32Set.In x (Int32Set.diff A C)
  82. +      -> (Int32Set.In x (Int32Set.diff A B) \/
  83. +          Int32Set.In x (Int32Set.diff B C)).
  84. +  Proof.
  85. +    intros. do 2 rewrite Int32Set.diff_spec in *.
  86. +    tauto.
  87. +  Qed.
  88. +
  89.    (** *** Properties of process_buffer *)
  90.  
  91.    (* process buffer prover *)
  92. @@ -951,7 +966,299 @@
  93.             apply IHn with (pc:=pc) in H; try (assumption || omega). clear IHn.
  94.             int32_simplify. lia.
  95.    Qed.
  96. +(*------------------------------*)
  97. +
  98. +(* The way _align uses skipn seems to require some more "obvious" facts
  99. +   about skipn than already exist in Coqlib.v: *)
  100. +
  101. +(* It would seem to me the intuitive way to reason about skipn to have
  102. +   an induction scheme that decrements n and cdrs down l in lockstep.
  103. +   But I don't know how to do that in Coq yet, so the next three lemmas
  104. +   (only the 3rd of which turns out to be needed) all do nested induction
  105. +   where we use the outer hypothesis in the inner case. *)
  106. +
  107. +(*
  108. +Lemma skipn_empty1 : forall (A : Type) (n:nat) (l : list A),
  109. +  (skipn n l) = nil -> (n >= (length l))%nat.
  110. +Proof.
  111. +  intros A.
  112. +  induction n as [| n'].
  113. +  Case "n = 0". intros l. simpl. intros H. rewrite H. simpl. apply le_n.
  114. +  Case "n = S n".
  115. +    intros l.
  116. +    induction l as [| a r].
  117. +      SCase "l = nil". simpl. omega.
  118. +      SCase "l = a :: r". simpl.
  119. +        intros Hnil.
  120. +        generalize (IHn' r). intros Ihnr.
  121. +        pose (Ihnr Hnil).
  122. +        omega.
  123. +Qed.
  124. +
  125. +Lemma skipn_empty2 : forall (A : Type) (l : list A) (n : nat),
  126. +  (n >= (length l))%nat -> (skipn n l) = nil.
  127. +Proof.
  128. +  intros A.
  129. +  induction l as [| a r].
  130. +  Case "l = nil". simpl. intros n H.
  131. +    destruct n as [| n']; reflexivity.
  132. +  Case "l = a :: r".
  133. +    simpl. intros n Hlen.
  134. +    destruct n as [| n'].
  135. +    SCase "n = 0".
  136. +      contradict Hlen. omega.
  137. +    SCase "n = S n'".
  138. +      simpl. apply IHr. omega.
  139. +Qed.
  140. +*)
  141.  
  142. +Lemma skipn_nonempty1: forall (A : Type) (l : list A) (n : nat),
  143. +  (skipn n l) <> nil -> (n < length l)%nat.
  144. +Proof.
  145. +  intros A.
  146. +  induction l as [| a r].
  147. +  Case "l = nil".
  148. +    simpl. intros n. destruct n as [| n'].
  149. +    SCase "n = 0". intros H. contradict H. reflexivity.
  150. +    SCase "n = S n'". intros H. contradict H. reflexivity.
  151. +  Case "l = a :: r".
  152. +    simpl. intros n Hlen.
  153. +    destruct n as [| n'].
  154. +    SCase "n = 0". omega.
  155. +    SCase "n = S n'".
  156. +      simpl in Hlen.
  157. +      assert (n' < length r)%nat by (apply IHr; assumption).
  158. +      omega.
  159. +Qed.
  160. +
  161. +Lemma skipn_length2 : forall (k n:nat) (A : Type) (l : list A),
  162. +  (length (skipn n l)) = S k -> (length l) = (S k + n)%nat.
  163. +Proof.
  164. +  intros k n A l.
  165. +  generalize (firstn_skipn n l). intros Hfnsn.
  166. +  assert(Hlfs: length (firstn n l ++ skipn n l) = length l)
  167. +    by (f_equal; assumption).
  168. +  rewrite app_length in Hlfs.
  169. +  generalize (firstn_length n l). intros Hlf.
  170. +  intros Hminlen.
  171. +  replace (min n (length l)) with n in Hlf.
  172. +  omega.
  173. +  Case "Length condition".
  174. +    symmetry. apply min_l.
  175. +    generalize (skipn_nonempty1 _ l n). intros Hsne.
  176. +    assert(Hnonempty: skipn n l <> nil).
  177. +    SCase "skipn nonempty".
  178. +      destruct (skipn n l) eqn:Hskipnl.
  179. +      SSCase "skipn is empty (can't happen)".
  180. +        contradict Hminlen. discriminate.
  181. +      SSCase "skipn nonempty". discriminate.
  182. +    generalize(Hsne Hnonempty).
  183. +    omega.
  184. +Qed.
  185. +
  186. +(* The next two lemmas let you reason about inequalities in terms of
  187. +   the existentially-quantified difference between the sides. I presume
  188. +   there must be something like somewhere in Coq's libraries, but it
  189. +   was easier to recreate than search for. *)
  190. +Lemma ge_to_ex : forall n m : nat,
  191. +  (n >= m)%nat <-> (exists d, n = m + d)%nat.
  192. +Proof.
  193. +  intros n m.
  194. +  split.
  195. +  Case "->".
  196. +    intros Hge.
  197. +    exists (n - m)%nat.
  198. +    omega.
  199. +  Case "<-".
  200. +    intros Hexd.
  201. +    destruct Hexd as [d].
  202. +    omega.
  203. +Qed.
  204. +
  205. +Lemma gt_to_ex : forall n m : nat,
  206. +  (n > m)%nat <-> (exists d, n = S (m + d))%nat.
  207. +Proof.
  208. +  intros n m.
  209. +  split.
  210. +  Case "->".
  211. +    intros Hgt.
  212. +    exists (n - m - 1)%nat.
  213. +    omega.
  214. +  Case "<-".
  215. +    intros Hexd.
  216. +    destruct Hexd as [d].
  217. +    omega.
  218. +Qed.
  219. +
  220. +Lemma skipn_length3 : forall (n : nat) (A : Type) (l : list A),
  221. +  (length (skipn n l) >= 1)%nat -> ((length l) > n)%nat.
  222. +Proof.
  223. +  intros n A l.
  224. +  intros Hskipn.
  225. +  rewrite ge_to_ex in Hskipn.
  226. +  destruct Hskipn as [d].
  227. +  replace (1+d)%nat with (S d) in H by reflexivity.
  228. +  rewrite gt_to_ex.
  229. +  exists d.
  230. +  replace (S (n + d)) with (S d + n)%nat by omega.
  231. +  apply skipn_length2. assumption.
  232. +Qed.
  233. +
  234. +(*
  235. +Lemma Z_of_to_nat : forall z,
  236. +  (0 <= z) -> Z.of_nat (Z.to_nat z) = z.
  237. +Proof.
  238. +  intros z.
  239. +  intros Hzge0.
  240. +  apply Z2Nat.id. assumption.
  241. +Qed.
  242. +*)
  243. +
  244. +(* An apparent gap in the existing tactics for reasoning about mixtures
  245. +   of naturals and integers. *)
  246. +Lemma misc_z_n_conv_rewrite : forall n z1 z2,
  247. +  (z2 >= 0) -> z1 + Z.of_nat (Z.to_nat z2 + n) = z1 + z2 + Z.of_nat n.
  248. +Proof.
  249. +  intros n z1 z2.
  250. +  intros Hz2ge0.
  251. +  autorewrite with nat_to_Z.
  252. +  rewrite Z2Nat.id. lia. lia.
  253. +Qed.
  254. +
  255. +Lemma process_buffer_align_addrRange :
  256. +   forall n start tokens currStartAddrs currJmpTargets
  257. +          allStartAddrs allJmpTargets pc,
  258. +    process_buffer_align start n tokens (currStartAddrs, currJmpTargets) =
  259. +      Some(allStartAddrs, allJmpTargets)
  260. +      -> noOverflow (start :: int32_of_nat (length tokens - 1) :: nil)
  261. +      -> Z_of_nat (length tokens) <= w32modulus
  262. +      -> Int32Set.In pc (Int32Set.diff allStartAddrs currStartAddrs)
  263. +      -> unsigned start <= unsigned pc
  264. +           < unsigned start + Z_of_nat (length tokens).
  265. +  Proof. induction n. intros.
  266. +    Case "n=0". intros. destruct tokens; pbprover.
  267. +    Case "S n".
  268. +      intros until 0.  intros HretSome HnoOverF HtokBound HpcAdded.
  269. +      destruct tokens as [| t tokens']. SCase "tokens=nil". pbprover.
  270. +      SCase "tokens<>nil".
  271. +        assert (HtokensLen: ((length (t::tokens') >= 1))%nat) by (simpl; omega).
  272. +        destruct (FastVerifier.process_buffer_aux non_cflow_dfa dir_cflow_dfa
  273. +          nacljmp_dfa initial_state start (S n) (t :: tokens')
  274. +          (currStartAddrs, currJmpTargets)) as [res_pair|] eqn:Hpb_aux.
  275. +          SSCase "pb_aux = Some".
  276. +            destruct res_pair as [start_instrs_new check_list_new].
  277. +            destruct (@Int32Set_diff_diff_dichotomy
  278. +                      pc _ start_instrs_new _ HpcAdded)
  279. +              as [Hdiff1|Hdiff2].
  280. +              SSSCase "pc added in recursion".
  281. +                use_lemma (IHn (start +32_n Z.to_nat chunkSize)
  282. +                       (skipn (Z.to_nat chunkSize) (t :: tokens'))
  283. +                       start_instrs_new check_list_new
  284. +                       allStartAddrs allJmpTargets pc) by assumption.
  285. +                rename H into IH.
  286. +                (* Most of the work in using the induction hypothesis has
  287. +                   to do with the side conditions that avoid overflow, and
  288. +                   proving that the address range condition translates properly,
  289. +                   which I haven't been able to automate very much. The
  290. +                   process_buffer_arith_facts lemma applies, but you need to
  291. +                   establish its hypotheses. Here I do that mostly by assert()s,
  292. +                   which was convenient for debugging but is not the
  293. +                   most concise. *)
  294. +                assert(HskipLen: (length (skipn (Z.to_nat chunkSize)
  295. +                                                (t :: tokens')) >= 1)%nat).
  296. +                SSSSCase "skipn chunkSize >= 1".
  297. +                  unfold process_buffer_align,
  298. +                         FastVerifier.process_buffer_align in HretSome.
  299. +                  rewrite Hpb_aux in HretSome.
  300. +                  assert(HnoPcContra:
  301. +                         ~(Some (start_instrs_new, check_list_new) =
  302. +                         Some (allStartAddrs, allJmpTargets))).
  303. +                  SSSSSCase "Proof of HnoPcContra".
  304. +                    injection. intros HnoCLN HnoSIN.
  305. +                    rewrite HnoSIN in Hdiff1. contradict Hdiff1.
  306. +                    rewrite Int32Set.diff_spec. tauto.
  307. +                  destruct n as [| p],
  308. +                           (skipn (Z.to_nat chunkSize) (t :: tokens'))
  309. +                           as [|tokens''] eqn:Hskipped.
  310. +                    SSSSSCase "n = 0, skipn = nil".
  311. +                      contradict HnoPcContra. assumption.
  312. +                    SSSSSCase "n = 0, skipn <> nil".
  313. +                      contradict HretSome. discriminate.
  314. +                    SSSSSCase "n = S p, skipn = nil".
  315. +                      contradict HnoPcContra. assumption.
  316. +                    SSSSSCase "n = Sp, skipn <> nil".
  317. +                      simpl. omega.
  318. +                generalize
  319. +                  (skipn_length3 (Z.to_nat chunkSize) _ (t :: tokens')).
  320. +                  intros Hlen3.
  321. +                generalize (Hlen3 HskipLen). intros Hgt32.
  322. +                assert(H32pskip: (length (t :: tokens') = (Z.to_nat chunkSize +
  323. +                     length (skipn (Z.to_nat chunkSize) (t :: tokens'))))%nat).
  324. +                SSSSCase "|tokens|=32+|rest|".
  325. +                  use_lemma (@skipn_length (Z.to_nat chunkSize)
  326. +                             _ (t :: tokens')) by assumption.
  327. +                  rename H into Hskipnl.
  328. +                  rewrite plus_comm. symmetry. apply Hskipnl.
  329. +                use_lemma (process_buffer_arith_facts start
  330. +                           (Z.to_nat chunkSize) (t :: tokens')
  331. +                           (skipn  (Z.to_nat chunkSize) (t :: tokens')))
  332. +                          by assumption.
  333. +                break_hyp.
  334. +                rename H into HnoOverFStartP32.
  335. +                rename H0 into HnoOverFStartPlen.
  336. +                rename H1 into HrestBound.
  337. +                assert(IHC: unsigned (start +32_n Z.to_nat chunkSize)
  338. +                       <= unsigned pc
  339. +                       < unsigned (start +32_n Z.to_nat chunkSize) +
  340. +                       Z.of_nat (length (skipn (Z.to_nat chunkSize)
  341. +                                               (t :: tokens')))).
  342. +                SSSSCase "Proof of IH conclusion".
  343. +                  apply IH.
  344. +                  SSSSSCase "pba returns Some".
  345. +                    unfold process_buffer_align,
  346. +                           FastVerifier.process_buffer_align in HretSome.
  347. +                    rewrite Hpb_aux in HretSome. exact HretSome.
  348. +                  SSSSSCase "noOverflow". assumption.
  349. +                  SSSSSCase "|rem. tokens|<2**32". assumption.
  350. +                  SSSSSCase "pc added in recursion". exact Hdiff1.
  351. +                assert(Hadd: unsigned start + chunkSize =
  352. +                             (unsigned (start +32_n Z.to_nat chunkSize))).
  353. +                  SSSSCase "Proving no overflow".
  354. +                    symmetry. apply noOverflow_2_iff. assumption.
  355. +                rewrite <- Hadd in IHC.
  356. +                destruct IHC as [IHC1 IHC2].
  357. +                split.
  358. +                  SSSSCase "start <= pc".
  359. +                    generalize (chunkSize_gt_0). omega.
  360. +                  SSSSCase "pc < start + length".
  361. +                    replace (length (t :: tokens')) with
  362. +                            (Z.to_nat chunkSize +
  363. +                             (length (skipn (Z.to_nat chunkSize)
  364. +                                     (t :: tokens'))))%nat
  365. +                                     by apply skipn_length.
  366. +                    assert(HcsGt0: chunkSize >= 0)
  367. +                      by (generalize chunkSize_gt_0; omega).
  368. +                    rewrite misc_z_n_conv_rewrite by assumption.
  369. +                    exact IHC2.
  370. +              SSSCase "pc added in aux".
  371. +                apply process_buffer_aux_addrRange with (n:=(S n))
  372. +                      (currStartAddrs:=currStartAddrs)
  373. +                      (currJmpTargets:=currJmpTargets)
  374. +                      (allStartAddrs:=start_instrs_new)
  375. +                      (allJmpTargets:=check_list_new).
  376. +                SSSSCase "pba returns Some".
  377. +                  unfold process_buffer_aux. exact Hpb_aux.
  378. +                SSSSCase "noOverflow". exact HnoOverF.
  379. +                SSSSCase "|tokens|<2**32". exact HtokBound.
  380. +                SSSSCase "pc added in aux". exact Hdiff2.
  381. +            SSCase "pb_aux = None".
  382. +              unfold process_buffer_align,
  383. +                     FastVerifier.process_buffer_align in HretSome.
  384. +              rewrite Hpb_aux in HretSome.
  385. +              contradict HretSome. discriminate.
  386. +Qed.
  387. +
  388. +(*--------------------------*)
  389.    Lemma process_buffer_addrRange : forall buffer startAddrs jmpTargets pc,
  390.      process_buffer buffer = Some (startAddrs, jmpTargets)
  391.        -> Z_of_nat (length buffer) <= w32modulus
  392. @@ -967,7 +1274,7 @@
  393.          int32_simplify. simpl. rewrite int32_modulus_constant. omega.
  394.          assert (length (b::buffer') >= 1)%nat by (simpl; omega).
  395.          int32_prover.
  396. -    apply process_buffer_aux_addrRange with (pc:=pc) in H;
  397. +    apply process_buffer_align_addrRange with (pc:=pc) in H;
  398.        [idtac | assumption | (rewrite list_length_map; trivial) | pbprover].
  399.      rewrite list_length_map in *; int32_prover.
  400.    Qed.
  401. @@ -1020,7 +1327,38 @@
  402.                apply Int32Set_subset_add.
  403.    Qed.
  404.  
  405. -  Lemma process_buffer_aux_start_in :
  406. +  Lemma process_buffer_align_subset :
  407. +    forall n start tokens currStartAddrs currJmpTargets allStartAddrs allJmpTargets,
  408. +      process_buffer_align start n tokens (currStartAddrs, currJmpTargets) =
  409. +        Some (allStartAddrs, allJmpTargets)
  410. +        -> Int32Set.Subset currStartAddrs allStartAddrs /\
  411. +           Int32Set.Subset currJmpTargets allJmpTargets.
  412. +
  413. +Proof. induction n. intros.
  414. +    Case "n=0". intros. destruct tokens; pbprover.
  415. +    Case "S n". intros.
  416. +      destruct tokens as [| t tokens']. pbprover.
  417. +      SCase "tokens<>nil".
  418. +      unfold process_buffer_align, FastVerifier.process_buffer_align in H.
  419. +          destruct (FastVerifier.process_buffer_aux non_cflow_dfa dir_cflow_dfa nacljmp_dfa
  420. +        initial_state start (S n) (t :: tokens')
  421. +        (currStartAddrs, currJmpTargets)) as [res_pair|] eqn:Hpba.
  422. +        SSCase "_aux_res <> None".
  423. +            destruct res_pair as [start_insn_new check_list_new].
  424. +            use_lemma process_buffer_aux_subset by eassumption.
  425. +            use_lemma IHn by eassumption.
  426. +            intuition.
  427. +            eapply Int32SetFacts.Subset_trans; [idtac | eassumption].
  428. +            assumption.
  429. +            eapply Int32SetFacts.Subset_trans; [idtac | eassumption].
  430. +            assumption.
  431. +        SSCase "_aux_res is None".
  432. +            discriminate.
  433. +Qed.
  434. +
  435. +(*  Admitted.*)
  436. +
  437. +  Lemma process_buffer_aux_start_in :
  438.      forall n start tokens currStartAddrs currJmpTargets allStartAddrs allJmpTargets,
  439.        process_buffer_aux start n tokens (currStartAddrs, currJmpTargets) =
  440.          Some(allStartAddrs, allJmpTargets)
  441. @@ -1049,12 +1387,39 @@
  442.            apply H2. apply Int32SetFacts.add_1. apply int_eq_refl.
  443.    Qed.
  444.  
  445. +  Lemma process_buffer_align_start_in :
  446. +    forall n start tokens currStartAddrs currJmpTargets allStartAddrs allJmpTargets,
  447. +      process_buffer_align start n tokens (currStartAddrs, currJmpTargets) =
  448. +        Some(allStartAddrs, allJmpTargets)
  449. +        -> (length (tokens) > 0)%nat
  450. +        -> Int32Set.In start allStartAddrs.
  451. +Proof. intros. destruct tokens as [| t tokens'].
  452. +    Case "tokens=nil". simpl in H0. contradict H0. omega.
  453. +    Case "tokens<>nil".
  454. +      assert (length (t::tokens') >= 1)%nat by (simpl; omega).
  455. +      destruct n.
  456. +      SCase "n=0". discriminate.
  457. +      SCase "S n".
  458. +          unfold process_buffer_align, FastVerifier.process_buffer_align in H.
  459. +          destruct (FastVerifier.process_buffer_aux non_cflow_dfa dir_cflow_dfa nacljmp_dfa
  460. +        initial_state start (S n) (t :: tokens')
  461. +        (currStartAddrs, currJmpTargets)) as [res_pair|] eqn:Hpba.
  462. +        SSCase "_aux_res <> None".
  463. +            destruct res_pair as [start_insn_new check_list_new].
  464. +            use_lemma process_buffer_aux_start_in by eassumption.
  465. +            use_lemma process_buffer_align_subset by eassumption.
  466. +            intuition.  
  467. +       SSCase "_aux_res is None".
  468. +            discriminate.
  469. +Qed.
  470. +(*  Admitted.*)
  471. +
  472.    Lemma process_buffer_start_in : forall code startAddrs jmpTargets,
  473.        process_buffer code =  Some (startAddrs, jmpTargets)
  474.          -> (length (code) > 0)%nat
  475.          -> Int32Set.In int32_zero startAddrs.
  476.    Proof. unfold process_buffer, FastVerifier.process_buffer; intros.
  477. -    eapply process_buffer_aux_start_in. eassumption.
  478. +    eapply process_buffer_align_start_in. eassumption.
  479.        rewrite list_length_map. assumption.
  480.    Qed.
  481.  
  482. @@ -1111,9 +1476,9 @@
  483.        -> Z_of_nat (length tokens) <= w32modulus
  484.        -> forall pc:int32, Int32Set.In pc (Int32Set.diff allStartAddrs currStartAddrs)
  485.             -> exists tokens', exists len, exists remaining,
  486. -                tokens' = (List.skipn (Zabs_nat (unsigned pc - unsigned start))
  487. +                tokens' = (List.skipn (Zabs_nat (unsigned pc - unsigned start))
  488.                               tokens) /\
  489. -                goodDefaultPC_aux (pc +32_n len) start allStartAddrs
  490. +                goodDefaultPC_aux (pc +32_n len) start allStartAddrs
  491.                    (length tokens) /\
  492.                  (dfa_recognize non_cflow_dfa tokens' = Some (len, remaining) \/
  493.                   (dfa_recognize dir_cflow_dfa tokens' = Some (len, remaining) /\
  494. @@ -1253,6 +1618,281 @@
  495.                split. trivial. split; assumption.
  496.    Qed.
  497.  
  498. +  Lemma merge_Znat_abs : forall x z, (0 <= x) -> (0 <= z) ->
  499. +    ((Zabs_nat x) + Z.to_nat z)%nat = Zabs_nat (x + z).
  500. +  Proof.
  501. +    intros x z.
  502. +    intros HxGt0 HzGt0.
  503. +    rewrite -> Zabs2Nat.abs_nat_nonneg by assumption.
  504. +    assert(HxpzGt0: 0 <= x + z) by lia.
  505. +    rewrite -> Zabs2Nat.abs_nat_nonneg by assumption.
  506. +    symmetry.
  507. +    apply Z2Nat.inj_add; assumption.
  508. +  Qed.
  509. +
  510. +  Lemma combine_p32_n : forall a n1 n2,
  511. +    a +32_n n1 +32_n n2 = a +32_n (n1 + n2)%nat.
  512. +  Proof.
  513. +    intros a n1 n2.
  514. +    unfold w32add.
  515. +    rewrite add_assoc.
  516. +    f_equal.
  517. +    replace (Z.of_nat (n1 + n2)) with ((Z.of_nat n1) + (Z.of_nat n2)).
  518. +    Case "After replace". apply add_repr.
  519. +    Case "Proof of replacement". symmetry. apply Nat2Z.inj_add.
  520. +  Qed.
  521. +
  522. +  Lemma includeAllJmpTargets_superset : forall pc len tokens set superset,
  523. +    (Int32Set.Subset set superset) ->
  524. +    (includeAllJmpTargets pc len tokens set) ->
  525. +    (includeAllJmpTargets pc len tokens superset).
  526. +  Proof.
  527. +    intros pc len tokens set superset.
  528. +    intros Hsubset.
  529. +    unfold includeAllJmpTargets.
  530. +    destruct_head. destruct p as [[pre ins] _].
  531. +    destruct ins; try trivial.
  532. +    Case "JMP".
  533. +      destruct near; try congruence.
  534. +      destruct absolute; try congruence.
  535. +      destruct op1; try congruence.
  536. +      destruct sel.
  537. +        trivial.
  538. +        intros. apply Int32Set_in_subset with (s:=set); assumption.
  539. +        intros. apply Int32Set_in_subset with (s:=set); assumption.
  540. +    Case "Call".
  541. +      destruct near; try congruence.
  542. +      destruct absolute; try congruence.
  543. +      destruct op1; try congruence.
  544. +      destruct sel.
  545. +        trivial.
  546. +        intros. apply Int32Set_in_subset with (s:=set); assumption.
  547. +        trivial.
  548. +  Qed.
  549. +
  550. +  Lemma process_buffer_align_inversion :
  551. +   forall n start tokens currStartAddrs currJmpTargets allStartAddrs allJmpTargets,
  552. +    process_buffer_align start n tokens (currStartAddrs, currJmpTargets) =
  553. +      Some (allStartAddrs, allJmpTargets)
  554. +      -> noOverflow (start :: int32_of_nat (length tokens - 1) :: nil)
  555. +      -> Z_of_nat (length tokens) <= w32modulus
  556. +      -> forall pc:int32, Int32Set.In pc (Int32Set.diff allStartAddrs currStartAddrs)
  557. +           -> exists tokens', exists len, exists remaining,
  558. +                tokens' = (List.skipn (Zabs_nat (unsigned pc - unsigned start))
  559. +                             tokens) /\
  560. +                goodDefaultPC_aux (pc +32_n len) start allStartAddrs
  561. +                  (length tokens) /\
  562. +                (dfa_recognize non_cflow_dfa tokens' = Some (len, remaining) \/
  563. +                 (dfa_recognize dir_cflow_dfa tokens' = Some (len, remaining) /\
  564. +                  includeAllJmpTargets pc len tokens' allJmpTargets) \/
  565. +                 dfa_recognize nacljmp_dfa tokens' = Some (len, remaining)).
  566. +  Proof.
  567. +    induction n as [| n'].
  568. +    Case "n = 0". intros. destruct tokens as [|t tokens2]; pbprover.
  569. +    Case "n = S n'".
  570. +    intros until 0.
  571. +    intros HretSome HnoOverF HtokBound pc HpcAdded.
  572. +    destruct tokens as [| t tokens2]. SCase "tokens = nil". pbprover.
  573. +    SCase "tokens <> nil".
  574. +    assert(HtokensLen: ((length (t::tokens2) >= 1))%nat) by (simpl; omega).
  575. +    destruct (FastVerifier.process_buffer_aux non_cflow_dfa dir_cflow_dfa
  576. +              nacljmp_dfa initial_state start (S n') (t :: tokens2)
  577. +              (currStartAddrs, currJmpTargets)) as [res_pair|] eqn:Hpb_aux.
  578. +    SSCase "pb_aux = Some".
  579. +      destruct res_pair as [start_instrs_new check_list_new].
  580. +      use_lemma (process_buffer_align_subset (S n') start
  581. +                 (t :: tokens2) currStartAddrs currJmpTargets
  582. +                 allStartAddrs allJmpTargets)
  583. +        by assumption.
  584. +      break_hyp.
  585. +      rename H into HcurAllStarts.
  586. +      rename H0 into HcurAllJmps.
  587. +      use_lemma (process_buffer_aux_subset (S n') start
  588. +                 (t :: tokens2) currStartAddrs currJmpTargets
  589. +                 start_instrs_new check_list_new)
  590. +        by assumption.
  591. +      break_hyp.
  592. +      rename H into HcurNextStarts.
  593. +      rename H0 into HcurNetJmps.
  594. +      assert(HrecSome:
  595. +             process_buffer_align (start +32_n Z.to_nat chunkSize) n'
  596. +                         (skipn (Z.to_nat chunkSize) (t :: tokens2))
  597. +                         (start_instrs_new, check_list_new) =
  598. +                Some (allStartAddrs, allJmpTargets)).
  599. +      SSSCase "Proof of HrecSome".
  600. +        unfold process_buffer_align,
  601. +               FastVerifier.process_buffer_align in HretSome.
  602. +        rewrite Hpb_aux in HretSome.
  603. +        exact HretSome.
  604. +      use_lemma (process_buffer_align_subset n'
  605. +                 (start +32_n Z.to_nat chunkSize)
  606. +                 (skipn (Z.to_nat chunkSize) (t :: tokens2))
  607. +                 start_instrs_new check_list_new
  608. +                 allStartAddrs allJmpTargets)
  609. +        by assumption.
  610. +      break_hyp.
  611. +      rename H into HnextAllStarts.
  612. +      rename H0 into HnextAllJmps.
  613. +      destruct (@Int32Set_diff_diff_dichotomy
  614. +                      pc _ start_instrs_new _ HpcAdded)
  615. +              as [Hdiff1|Hdiff2].
  616. +      SSSCase "pc added in recursion".
  617. +        use_lemma (IHn' (start +32_n Z.to_nat chunkSize)
  618. +                        (skipn (Z.to_nat chunkSize) (t :: tokens2))
  619. +                        start_instrs_new check_list_new
  620. +                        allStartAddrs allJmpTargets) by assumption.
  621. +        rename H into IH.
  622. +        assert(HskipLen: (length (skipn (Z.to_nat chunkSize)
  623. +                                        (t :: tokens2)) >= 1)%nat).
  624. +        SSSSCase "Proof of HskipLen".
  625. +          unfold process_buffer_align,
  626. +                 FastVerifier.process_buffer_align in HretSome.
  627. +          rewrite Hpb_aux in HretSome.
  628. +          assert(HnoPcContra:
  629. +                 ~(Some (start_instrs_new, check_list_new) =
  630. +                   Some (allStartAddrs, allJmpTargets))).
  631. +          SSSSSCase "Proof of HnoPcContra".
  632. +            injection. intros HnoCLN HnoSIN.
  633. +            rewrite HnoSIN in Hdiff1. contradict Hdiff1.
  634. +            rewrite Int32Set.diff_spec. tauto.
  635. +            destruct n' as [| p],
  636. +                     (skipn (Z.to_nat chunkSize) (t :: tokens2))
  637. +                           as [|tokens3] eqn:Hskipped.
  638. +            SSSSSCase "n' = 0, skipn = nil".
  639. +              contradict HnoPcContra. assumption.
  640. +            SSSSSCase "n' = 0, skipn <> nil".
  641. +              contradict HretSome. discriminate.
  642. +            SSSSSCase "n' = S p, skipn = nil".
  643. +              contradict HnoPcContra. assumption.
  644. +            SSSSSCase "n' = Sp, skipn <> nil".
  645. +              simpl. omega.
  646. +        generalize
  647. +          (skipn_length3 (Z.to_nat chunkSize) _ (t :: tokens2)).
  648. +          intros Hlen3.
  649. +        generalize (Hlen3 HskipLen). intros Hgt32.
  650. +        assert(H32pskip: (length (t :: tokens2) = (Z.to_nat chunkSize +
  651. +              length (skipn (Z.to_nat chunkSize) (t :: tokens2))))%nat).
  652. +        SSSSCase "|tokens|=32+|rest|".
  653. +          use_lemma (@skipn_length (Z.to_nat chunkSize)
  654. +                      _ (t :: tokens2)) by assumption.
  655. +          rename H into Hskipnl.
  656. +          rewrite plus_comm. symmetry. apply Hskipnl.
  657. +        use_lemma (process_buffer_arith_facts start
  658. +                   (Z.to_nat chunkSize) (t :: tokens2)
  659. +                   (skipn  (Z.to_nat chunkSize) (t :: tokens2)))
  660. +                   by assumption.
  661. +        break_hyp.
  662. +        rename H into HnoOverFStartP32.
  663. +        rename H0 into HnoOverFStartPlen.
  664. +        rename H1 into HrestBound.
  665. +        generalize (IH HnoOverFStartPlen HrestBound pc Hdiff1).
  666. +        intros H.
  667. +        destruct H as [tokens']. exists tokens'.
  668. +        destruct H as [len]. exists len.
  669. +        destruct H as [remaining]. exists remaining.
  670. +        break_hyp.
  671. +        rename H into HinsnToks.
  672. +        rename H0 into HgoodPC.
  673. +        rename H1 into Hdfas.
  674. +        split.
  675. +        SSSSCase "tokens' definition".
  676. +          rewrite skipn_twice_eq in HinsnToks.
  677. +          replace (Z.abs_nat (unsigned pc -
  678. +                    unsigned (start +32_n Z.to_nat chunkSize)) +
  679. +                   Z.to_nat chunkSize)%nat with
  680. +                  (Z.abs_nat (unsigned pc - unsigned start))
  681. +                  in HinsnToks. assumption.
  682. +          SSSSSCase "Arithmetic cancellation".
  683. +            assert(HrewA32: (unsigned (start +32_n Z.to_nat chunkSize)) =
  684. +                    ((unsigned start) + chunkSize)).
  685. +            SSSSSSCase "Proof of noOverflow replacement rule".
  686. +              generalize (noOverflow_2_iff start
  687. +                          (int32_of_nat (Z.to_nat chunkSize))).
  688. +              intros. break_hyp. clear H0.
  689. +              rename H into HnoO2if.
  690. +              rewrite HnoO2if by assumption.
  691. +              auto.
  692. +            rewrite HrewA32.
  693. +            replace (unsigned pc - (unsigned start + chunkSize)) with
  694. +                    (unsigned pc - unsigned start - chunkSize) by lia.
  695. +            generalize chunkSize_gt_0. intros HchunkGt0.
  696. +            generalize (process_buffer_align_addrRange
  697. +                        (S n') start (t :: tokens2)
  698. +                        currStartAddrs currJmpTargets
  699. +                        allStartAddrs allJmpTargets pc HretSome
  700. +                        HnoOverF HtokBound HpcAdded).
  701. +            intros HaddrRange.
  702. +            generalize (process_buffer_align_addrRange
  703. +                        n' (start +32_n Z.to_nat chunkSize)
  704. +                        (skipn (Z.to_nat chunkSize) (t :: tokens2))
  705. +                        start_instrs_new check_list_new
  706. +                        allStartAddrs allJmpTargets pc
  707. +                        HrecSome HnoOverFStartPlen HrestBound
  708. +                        Hdiff1).
  709. +            intros HaddrRange2.
  710. +            rewrite HrewA32 in HaddrRange2.
  711. +            replace ((Z.abs_nat (unsigned pc - unsigned start - chunkSize)
  712. +                     + Z.to_nat chunkSize)%nat) with
  713. +                    (Z.abs_nat (unsigned pc - unsigned start - chunkSize
  714. +                                + chunkSize)).
  715. +            SSSSSSCase "Proof after abs_nat merger".
  716. +              f_equal. lia.
  717. +            SSSSSSCase "Proof of abs_nat merger".
  718. +              assert(HdiffPos:
  719. +                     (0 <= unsigned pc - unsigned start - chunkSize))
  720. +                by lia.
  721. +              symmetry.
  722. +              apply merge_Znat_abs; lia.
  723. +        split.
  724. +        SSSSCase "HgoodPC displaced".
  725. +          unfold goodDefaultPC_aux.
  726. +          unfold goodDefaultPC_aux in HgoodPC.
  727. +          destruct HgoodPC as [HgoodPC_l | HgoodPC_r].
  728. +            SSSSSCase "Not last address". left. assumption.
  729. +            SSSSSCase "Last address". right.
  730. +              rewrite HgoodPC_r.
  731. +              rewrite combine_p32_n.
  732. +              f_equal. f_equal. f_equal.
  733. +              symmetry. assumption.
  734. +        SSSSCase "Hdfas". assumption.
  735. +      SSSCase "pc added in aux".
  736. +        use_lemma (process_buffer_aux_inversion (S n') start
  737. +                   (t :: tokens2) currStartAddrs currJmpTargets
  738. +                   start_instrs_new check_list_new
  739. +                   Hpb_aux HnoOverF HtokBound pc)
  740. +          by assumption.
  741. +        destruct H as [tokens']. exists tokens'.
  742. +        destruct H as [len]. exists len.
  743. +        destruct H as [remaining]. exists remaining.
  744. +        break_hyp.
  745. +        rename H into HinsnToks.
  746. +        rename H0 into HgoodPC.
  747. +        rename H1 into Hdfas.
  748. +        split.
  749. +        SSSSCase "HinsnToks". assumption.
  750. +        split.
  751. +        SSSSCase "HgoodPC subset".
  752. +          unfold goodDefaultPC_aux.
  753. +          unfold goodDefaultPC_aux in HgoodPC.
  754. +          assert(HstartSub:
  755. +                 Int32Set.In (pc +32_n len) start_instrs_new ->
  756. +                 Int32Set.In (pc +32_n len) allStartAddrs).
  757. +           SSSSSCase "Proof of HstartSub".
  758. +             intros HinNext.
  759. +             apply Int32Set_in_subset with (s:=start_instrs_new);
  760. +               assumption.
  761. +          tauto.
  762. +        SSSSCase "Hdfas subset".
  763. +          use_lemma (includeAllJmpTargets_superset pc len tokens'
  764. +                     check_list_new allJmpTargets) by assumption.
  765. +          tauto.
  766. +    SSCase "pb_aux = None".
  767. +      unfold process_buffer_align,
  768. +             FastVerifier.process_buffer_align in HretSome.
  769. +      rewrite Hpb_aux in HretSome.
  770. +      contradict HretSome. discriminate.
  771. +  Qed.
  772. +
  773.    Hint Rewrite Zminus_0_r : pbDB.
  774.  
  775.    Lemma process_buffer_inversion :
  776. @@ -1278,7 +1918,7 @@
  777.          simpl. int32_simplify. rewrite int32_modulus_constant. simpl. lia.
  778.          assert (length (b::buffer') >= 1)%nat by (simpl; omega).
  779.          int32_prover.
  780. -    apply process_buffer_aux_inversion with (pc:=pc) in H;
  781. +    apply process_buffer_align_inversion with (pc:=pc) in H;
  782.        [idtac | assumption | (rewrite list_length_map; omega) | pbprover].
  783.      destruct H as [tokens' [len [remaining H]]].
  784.      break_hyp.
Advertisement
RAW Paste Data Copied
Advertisement