Fare9

Exercise Chapter 12 Practical Binary Analysis Z3

May 26th, 2019
1,298
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. ; Z3 script solver to do the next exercises
  2. ; 2. Proving Reachability
  3. ;   Use Z3 to figure out which of the calls to foo, bar, and baz are reachable
  4. ;   in the listing from the previous exercise. Model the relevant operations and branches
  5. ;   using bitvectors
  6. ; 3. Finding Opaque Predicates
  7. ;   Use Z3 to check whether any of the conditionals in the previous
  8. ;   listing are opaque predicates. If so, are they opaque true or false?
  9. ;   which code is unreachable and therefore safe to eliminate from the listing
  10. ;
  11. ; For the next code
  12. ;
  13. ;   x = int(argv[0])
  14. ;   y = int(argv[1])
  15. ;  
  16. ;   z = x*x
  17. ;   w = y*y
  18. ;  
  19. ;   if(z <= 1)
  20. ;       if( ((z + w) % 7 == 0) && (x % 7 != 0) )
  21. ;           foo(z, w
  22. ;  
  23. ;   else
  24. ;       if((2**z - 1) % z != 0)
  25. ;           bar(x, y, z)
  26. ;  
  27. ;       else
  28. ;           z = z + w
  29. ;           baz(z, y, x)
  30. ;  
  31. ;   z = z*z
  32. ;   qux(x, y, z)
  33.  
  34.  
  35. (declare-const x (_ BitVec 32))
  36. (declare-const y (_ BitVec 32))
  37. (declare-const z (_ BitVec 32))
  38. (declare-const w (_ BitVec 32))
  39. (assert (= z (bvmul x x)))
  40. (assert (= w (bvmul y y)))
  41.  
  42. (push)
  43. ; Solver to call the function foo
  44. (assert (bvsle z (_ bv1 32)))
  45.  
  46. (push)
  47. (assert (and (= (bvsmod (bvadd z w) (_ bv7 32)) (_ bv0 32)) (not (= (bvsmod x (_ bv7 32)) (_ bv0 32)))))
  48. (check-sat)
  49. (get-model)
  50. (pop)
  51.  
  52. (push)
  53. ; check if the sentence "if" after "if z <= 1" is opaque predicate
  54. (assert (not (and (= (bvsmod (bvadd z w) (_ bv7 32)) (_ bv0 32)) (not (= (bvsmod x (_ bv7 32)) (_ bv0 32))))))
  55. (check-sat)
  56. (get-model)
  57. (pop)
  58.  
  59. (pop)
  60.  
  61.  
  62. (push)
  63. (assert (bvsgt z (_ bv1 32)))
  64.  
  65. (push)
  66. ; Solver to call the function bar after else if
  67. (assert (not (= (bvsmod (bvsub (ite (= z (_ bv0 32)) (_ bv1 32) (bvshl (_ bv2 32) z)) (_ bv1 32)) z) (_ bv0 32))))
  68. (check-sat)
  69. (get-model)
  70. (pop)
  71.  
  72. (push)
  73. ; Solver to call the function baz after the else else
  74. (assert (= (bvsmod (bvsub (ite (= z (_ bv0 32)) (_ bv1 32) (bvshl (_ bv2 32) z)) (_ bv1 32)) z) (_ bv0 32)))
  75. (assert (= z (bvadd z w)))
  76. (check-sat)
  77. (get-model)
  78. (pop)
  79.  
  80. (pop)
RAW Paste Data

Adblocker detected! Please consider disabling it...

We've detected AdBlock Plus or some other adblocking software preventing Pastebin.com from fully loading.

We don't have any obnoxious sound, or popup ads, we actively block these annoying types of ads!

Please add Pastebin.com to your ad blocker whitelist or disable your adblocking software.

×