From 95f388b5ced93330665da581ee8804fd8e445bfe Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Fri, 18 Feb 2022 11:23:29 +0100
Subject: [PATCH] added example Z3 scripts

---
 farm_animals/bare.py                  | 37 +++++++++++++++++
 farm_animals/final.py                 | 59 +++++++++++++++++++++++++++
 farm_animals/version1.py              | 45 ++++++++++++++++++++
 farm_animals/version2.py              | 48 ++++++++++++++++++++++
 password_cracking/password_cracker.py | 46 +++++++++++++++++++++
 password_cracking/password_storage.sh | 38 +++++++++++++++++
 6 files changed, 273 insertions(+)
 create mode 100644 farm_animals/bare.py
 create mode 100644 farm_animals/final.py
 create mode 100644 farm_animals/version1.py
 create mode 100644 farm_animals/version2.py
 create mode 100644 password_cracking/password_cracker.py
 create mode 100755 password_cracking/password_storage.sh

diff --git a/farm_animals/bare.py b/farm_animals/bare.py
new file mode 100644
index 0000000..2ea0151
--- /dev/null
+++ b/farm_animals/bare.py
@@ -0,0 +1,37 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# No need to parse anything for this example
+
+#################################### Farm Animals ####################################
+solver = Solver()
+
+# We have 100€ ( == 10000c) and we want to buy **exactly** 100 animals, where
+# price(cow) = 10€
+# price(chicken) = 3€
+# price(mouse) = 25c
+
+# todo
+# Create Z3 variables which hold the number of animals and the price respectively
+
+# todo
+# Create Z3 variables which hold the amount of the different animals our farmes is going to buy
+
+# todo
+# Add constraints which model our real life requirements
+
+# Check for satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+################################################################################
+# print the model
+#  get the model
+m = solver.model()
+#  print all Z3 variables which have an assignment in the model
+for d in m.decls():
+    print("%s = %s" % (d.name(), m[d]))
+################################################################################
diff --git a/farm_animals/final.py b/farm_animals/final.py
new file mode 100644
index 0000000..0887acf
--- /dev/null
+++ b/farm_animals/final.py
@@ -0,0 +1,59 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# No need to parse anything for this example
+
+#################################### Farm Animals ####################################
+solver = Solver()
+
+# todo
+# Create Z3 variables which hold the number of animals and the price respectively
+amount_of_animals = Int("amount_of_animals")
+total_price = Int("total_price")
+target_price = 10000
+target_amount = 100
+
+# todo
+# Create Z3 variables which hold the amount of the different animals our farmes is going to buy
+cows = Int("cows")
+mice = Int("mice")
+chicken = Int("chicken")
+
+# todo
+# Add constraints which model our real life requirements
+solver.add(cows + chicken + mice == amount_of_animals)
+solver.add(cows * 1000 + chicken * 300 + mice * 25 == total_price)
+solver.add(total_price == target_price)
+solver.add(amount_of_animals == target_amount)
+# Done?
+
+solver.add(cows > 1)
+solver.add(chicken > 1)
+solver.add(mice > 1)
+
+print(solver.sexpr())
+
+# Check for satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+################################################################################
+# print the model
+#  get the model
+m = solver.model()
+#  print all Z3 variables which have an assignment in the model
+result =  str(m[cows]) + " cows and "
+result += str(m[chicken]) + " chicken and "
+result += str(m[mice]) + " mice -> "
+print(result)
+print(m[cows].as_long() * 10 + m[chicken].as_long() * 3 + m[mice].as_long() * 0.25)
+solver.add(mice != m[mice])
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+################################################################################
diff --git a/farm_animals/version1.py b/farm_animals/version1.py
new file mode 100644
index 0000000..e62844e
--- /dev/null
+++ b/farm_animals/version1.py
@@ -0,0 +1,45 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# No need to parse anything for this example
+
+#################################### Farm Animals ####################################
+solver = Solver()
+
+# todo
+# Create Z3 variables which hold the number of animals and the price respectively
+amount_of_animals = Int("amount_of_animals")
+total_price = Int("total_price")
+target_price = 10000
+target_amount = 100
+
+# todo
+# Create Z3 variables which hold the amount of the different animals our farmes is going to buy
+cows = Int("cows")
+mice = Int("mice")
+chicken = Int("chicken")
+
+# todo
+# Add constraints which model our real life requirements
+solver.add(cows + chicken + mice == amount_of_animals)
+solver.add(cows * 1000 + chicken * 300 + mice * 25 == total_price)
+solver.add(total_price == target_price)
+solver.add(amount_of_animals == target_amount)
+
+# Done?
+
+# Check for satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+################################################################################
+# print the model
+#  get the model
+m = solver.model()
+#  print all Z3 variables which have an assignment in the model
+for d in m.decls():
+    print("%s = %s" % (d.name(), m[d]))
+################################################################################
diff --git a/farm_animals/version2.py b/farm_animals/version2.py
new file mode 100644
index 0000000..93ccf66
--- /dev/null
+++ b/farm_animals/version2.py
@@ -0,0 +1,48 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# No need to parse anything for this example
+
+#################################### Farm Animals ####################################
+solver = Solver()
+
+# todo
+# Create Z3 variables which hold the number of animals and the price respectively
+amount_of_animals = Int("amount_of_animals")
+total_price = Int("total_price")
+target_price = 10000
+target_amount = 100
+
+# todo
+# Create Z3 variables which hold the amount of the different animals our farmes is going to buy
+cows = Int("cows")
+mice = Int("mice")
+chicken = Int("chicken")
+
+# todo
+# Add constraints which model our real life requirements
+solver.add(cows + chicken + mice == amount_of_animals)
+solver.add(cows * 1000 + chicken * 300 + mice * 25 == total_price)
+solver.add(total_price == target_price)
+solver.add(amount_of_animals == target_amount)
+# Done?
+
+solver.add(cows > 1)
+solver.add(chicken > 1)
+solver.add(mice > 1)
+
+# Check for satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+################################################################################
+# print the model
+#  get the model
+m = solver.model()
+#  print all Z3 variables which have an assignment in the model
+for d in m.decls():
+    print("%s = %s" % (d.name(), m[d]))
+################################################################################
diff --git a/password_cracking/password_cracker.py b/password_cracking/password_cracker.py
new file mode 100644
index 0000000..47d060f
--- /dev/null
+++ b/password_cracking/password_cracker.py
@@ -0,0 +1,46 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+
+# 'hashed' password we have from the 'binary'
+hashed_password=168372036536695091
+
+# we are going to try different lengths of passwords
+for password_length in range(5,15):
+    # init solver, this will wipe any residual constraints in each loop
+    solver = Solver()
+
+    # initialize constraints for each character of the password
+    # we are only going to allow ascii values from 'a' to 'z'
+    chars = [Int(c) for c in range(password_length)]
+
+    # initialization value
+    n = 7
+    # the 'hashing' algorithm we have extracted from the binary
+    for c in chars:
+        # this essentially extends the symbolic constraints associated with each 'c'
+        n = n * 27 + c * 5
+
+    # the solver should return sat iff
+    # the hashed input is equal the hashed_password
+    solver.add(n == hashed_password)
+
+    for c in chars:
+        # each 'c' should be a lowercase ascii character
+        solver.add(And(c >= ord('a'),
+                       c <= ord('z')))
+
+
+    res = solver.check()
+    if res != sat:
+        print("No possible password found...")
+        continue
+
+    # print the model/password found
+    m = solver.model()
+    for d in m.decls():
+        print("%s = %s -> %c" % (d.name(), m[d], chr(m[d].as_long())))
+    password = ''.join(chr(m[c].as_long()) for c in chars)
+    print("Trying '" + password + "' as password")
+    os.system("./password_storage.sh {}".format(password))
diff --git a/password_cracking/password_storage.sh b/password_cracking/password_storage.sh
new file mode 100755
index 0000000..64c335c
--- /dev/null
+++ b/password_cracking/password_storage.sh
@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+
+
+# return password to password storage shell
+get_password() {
+  printf 'secret'
+}
+
+# initialization value
+n=7
+# 'hashed' password
+hashed_password=168372036536695091
+
+# read password as parameter ...
+password=$1
+# ... or ask for password
+[ -z $1 ] && printf "Enter password:\n" && read -s password
+
+# 'hash' the password with some random multiplications
+for (( i=0; i<${#password}; i++ )); do
+  charval=$(printf "%d\n" \'${password:$i:1}) # ascii value of the current character
+  n=$(echo "$n * 27 + $charval * 5" | bc) # do some computations and assign to intermediate result
+done
+
+# check if hash of entered password is equal to 'hashed' password
+if [[ $n -eq $hashed_password ]]; then
+  # if yes then grant access to prompt
+  while true; do
+    printf "\n$(whoami)'s password storage> "
+    read pass
+    get_password
+  done
+  exit 0
+else
+  # else exit with error code
+  printf "\nWrong password."
+  exit 1
+fi