• API
• FAQ
• Tools
• Archive
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.

Top