API tools faq
paste
Advertisement
Guest User

RockSalt Diff

a guest
Aug 8th, 2017
191
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Diff 33.13 KB | None | 0 0
raw download clone embed print report
  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
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!