SHARE
TWEET

Exercise Chapter 12 Practical Binary Analysis Z3

Fare9 May 26th, 2019 (edited) 550 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
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
 
Top