Z3 - Satisfiability Modulo Theories (SMT)
Learn & practice AWS Hacking:HackTricks Training AWS Red Team Expert (ARTE)
Learn & practice GCP Hacking:
HackTricks Training GCP Red Team Expert (GRTE)
Πολύ βασικά, αυτό το εργαλείο θα μας βοηθήσει να βρούμε τιμές για μεταβλητές που πρέπει να ικανοποιούν κάποιες συνθήκες και η υπολογιστική τους χειροκίνητα θα είναι πολύ ενοχλητική. Επομένως, μπορείτε να υποδείξετε στο Z3 τις συνθήκες που πρέπει να ικανοποιούν οι μεταβλητές και θα βρει κάποιες τιμές (αν είναι δυνατόν).
Ορισμένα κείμενα και παραδείγματα προέρχονται από https://ericpony.github.io/z3py-tutorial/guide-examples.htm
Basic Operations
Booleans/And/Or/Not
Ακέραιοι/Απλοποίηση/Πραγματικοί αριθμοί
Εκτύπωση Μοντέλου
Μηχανική Άλγεβρα
Οι σύγχρονοι επεξεργαστές και οι κυριότερες γλώσσες προγραμματισμού χρησιμοποιούν άλγεβρα πάνω σε σταθερού μεγέθους bit-vectors. Η μηχανική άλγεβρα είναι διαθέσιμη στο Z3Py ως Bit-Vectors.
Υπογεγραμμένοι/Μη Υπογεγραμμένοι Αριθμοί
Το Z3 παρέχει ειδικές υπογεγραμμένες εκδόσεις αριθμητικών λειτουργιών όπου έχει σημασία αν το bit-vector αντιμετωπίζεται ως υπογεγραμμένο ή μη υπογεγραμμένο. Στο Z3Py, οι τελεστές <, <=, >, >=, /, % και >> αντιστοιχούν στις υπογεγραμμένες εκδόσεις. Οι αντίστοιχοι μη υπογεγραμμένοι τελεστές είναι ULT, ULE, UGT, UGE, UDiv, URem και LShR.
Functions
Ερμηνευμένες συναρτήσεις όπως η αριθμητική όπου η συνάρτηση + έχει μια σταθερή τυπική ερμηνεία (προσθέτει δύο αριθμούς). Μη ερμηνευμένες συναρτήσεις και σταθερές είναι μέγιστης ευελιξίας; επιτρέπουν οποιαδήποτε ερμηνεία που είναι συνεπής με τους περιορισμούς πάνω στη συνάρτηση ή τη σταθερά.
Παράδειγμα: η f εφαρμοσμένη δύο φορές στο x έχει ως αποτέλεσμα το x ξανά, αλλά η f εφαρμοσμένη μία φορά στο x είναι διαφορετική από το x.
Παραδείγματα
Λύτης Sudoku
Αναφορές
Μάθετε & εξασκηθείτε στο AWS Hacking:HackTricks Training AWS Red Team Expert (ARTE)
Μάθετε & εξασκηθείτε στο GCP Hacking:
HackTricks Training GCP Red Team Expert (GRTE)
Last updated