mirror of
https://github.com/carlospolop/hacktricks
synced 2024-12-25 04:23:33 +00:00
200 lines
10 KiB
Markdown
200 lines
10 KiB
Markdown
<details>
|
|
|
|
<summary><strong>जानें AWS हैकिंग को शून्य से हीरो तक</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong> के साथ!</strong></summary>
|
|
|
|
HackTricks का समर्थन करने के अन्य तरीके:
|
|
|
|
* यदि आप अपनी **कंपनी का विज्ञापन HackTricks में देखना चाहते हैं** या **HackTricks को PDF में डाउनलोड करना चाहते हैं** तो [**सब्सक्रिप्शन प्लान**](https://github.com/sponsors/carlospolop) देखें!
|
|
* [**आधिकारिक PEASS & HackTricks स्वैग**](https://peass.creator-spring.com) प्राप्त करें
|
|
* हमारे विशेष [**NFTs**](https://opensea.io/collection/the-peass-family) कलेक्शन, [**The PEASS Family**](https://opensea.io/collection/the-peass-family) खोजें
|
|
* **शामिल हों** 💬 [**डिस्कॉर्ड समूह**](https://discord.gg/hRep4RUj7f) या [**टेलीग्राम समूह**](https://t.me/peass) और हमें **ट्विटर** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live) पर **फॉलो** करें।
|
|
* **अपने हैकिंग ट्रिक्स साझा करें, HackTricks** के लिए PRs सबमिट करके [**HackTricks**](https://github.com/carlospolop/hacktricks) और [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github repos में।
|
|
|
|
</details>
|
|
|
|
|
|
बहुत ही बुनियादी रूप से, यह टूल हमें उन मानों को खोजने में मदद करेगा जो कुछ स्थितियों को पूरा करने की आवश्यकता है और उन्हें हाथ से गणना बहुत परेशानीजनक होगा। इसलिए, आप Z3 को इंडिकेट कर सकते हैं कि मानों को कौन सी स्थितियों को पूरा करने की आवश्यकता है और यह कुछ मान (यदि संभव है) खोजेगा।
|
|
|
|
**कुछ पाठ और उदाहरण [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm) से निकाले गए हैं**
|
|
|
|
# मूल ऑपरेशन
|
|
|
|
## बूलियन/और/या/नहीं
|
|
```python
|
|
#pip3 install z3-solver
|
|
from z3 import *
|
|
s = Solver() #The solver will be given the conditions
|
|
|
|
x = Bool("x") #Declare the symbos x, y and z
|
|
y = Bool("y")
|
|
z = Bool("z")
|
|
|
|
# (x or y or !z) and y
|
|
s.add(And(Or(x,y,Not(z)),y))
|
|
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
|
|
print(s.model()) #Print valid values to satisfy the model
|
|
```
|
|
## पूर्णांक/सरल/वास्तविक
|
|
```python
|
|
from z3 import *
|
|
|
|
x = Int('x')
|
|
y = Int('y')
|
|
#Simplify a "complex" ecuation
|
|
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
|
|
#And(x >= 2, 2*x**2 + y**2 >= 3)
|
|
|
|
#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
|
|
#so you can get the decimals you need from the solution
|
|
r1 = Real('r1')
|
|
r2 = Real('r2')
|
|
#Solve the ecuation
|
|
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
|
|
#Solve the ecuation with 30 decimals
|
|
set_option(precision=30)
|
|
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
|
|
```
|
|
## मॉडल प्रिंट करना
|
|
```python
|
|
from z3 import *
|
|
|
|
x, y, z = Reals('x y z')
|
|
s = Solver()
|
|
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
|
|
s.check()
|
|
|
|
m = s.model()
|
|
print ("x = %s" % m[x])
|
|
for d in m.decls():
|
|
print("%s = %s" % (d.name(), m[d]))
|
|
```
|
|
# मशीन अंकगणित
|
|
|
|
आधुनिक सीपीयू और मुख्य प्रवाहित प्रोग्रामिंग भाषाएं **निर्धारित-आकार बिट-वेक्टर** पर अंकगणित का उपयोग करती हैं। मशीन अंकगणित Z3Py में **बिट-वेक्टर** के रूप में उपलब्ध है।
|
|
```python
|
|
from z3 import *
|
|
|
|
x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
|
|
y = BitVec('y', 16)
|
|
|
|
e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
|
|
a = BitVecVal(-1, 16)
|
|
b = BitVecVal(65535, 16)
|
|
print(simplify(a == b)) #This is True!
|
|
a = BitVecVal(-1, 32)
|
|
b = BitVecVal(65535, 32)
|
|
print(simplify(a == b)) #This is False
|
|
```
|
|
## साइन किए गए/असाइन किए गए संख्याएं
|
|
|
|
Z3 विशेष साइन रूपों के अंकगणितीय कार्यों प्रदान करता है जहाँ यह मायने रखता है कि **बिट-वेक्टर को साइन या असाइन के रूप में कैसे देखा जाए**। Z3Py में, ऑपरेटर **<, <=, >, >=, /, % और >>** साइन रूपों के संस्करणों को दर्शाते हैं। संबंधित **असाइन** ऑपरेटर हैं **ULT, ULE, UGT, UGE, UDiv, URem और LShR**।
|
|
```python
|
|
from z3 import *
|
|
|
|
# Create to bit-vectors of size 32
|
|
x, y = BitVecs('x y', 32)
|
|
solve(x + y == 2, x > 0, y > 0)
|
|
|
|
# Bit-wise operators
|
|
# & bit-wise and
|
|
# | bit-wise or
|
|
# ~ bit-wise not
|
|
solve(x & y == ~y)
|
|
solve(x < 0)
|
|
|
|
# using unsigned version of <
|
|
solve(ULT(x, 0))
|
|
```
|
|
## कार्य
|
|
|
|
**व्याख्यात कार्य** जैसे अंकगणित जहाँ **कार्य +** का **निश्चित मानक व्याख्या** होता है (यह दो नंबर जोड़ता है)। **अव्याख्यात कार्य** और स्थिर संदर्भ हैं; वे **किसी भी व्याख्या** को अनुमति देते हैं जो **कार्य या स्थिर संदर्भ** के अधीन संबंधित है।
|
|
|
|
उदाहरण: x पर दो बार f लागू करने पर पुनः x परिणाम होता है, लेकिन x पर एक बार f लागू करने पर x से भिन्न है।
|
|
```python
|
|
from z3 import *
|
|
|
|
x = Int('x')
|
|
y = Int('y')
|
|
f = Function('f', IntSort(), IntSort())
|
|
s = Solver()
|
|
s.add(f(f(x)) == x, f(x) == y, x != y)
|
|
s.check()
|
|
m = s.model()
|
|
print("f(f(x)) =", m.evaluate(f(f(x))))
|
|
print("f(x) =", m.evaluate(f(x)))
|
|
|
|
print(m.evaluate(f(2)))
|
|
s.add(f(x) == 4) #Find the value that generates 4 as response
|
|
s.check()
|
|
print(m.model())
|
|
```
|
|
# उदाहरण
|
|
|
|
## सुडोकू सॉल्वर
|
|
```python
|
|
# 9x9 matrix of integer variables
|
|
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
|
|
for i in range(9) ]
|
|
|
|
# each cell contains a value in {1, ..., 9}
|
|
cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
|
|
for i in range(9) for j in range(9) ]
|
|
|
|
# each row contains a digit at most once
|
|
rows_c = [ Distinct(X[i]) for i in range(9) ]
|
|
|
|
# each column contains a digit at most once
|
|
cols_c = [ Distinct([ X[i][j] for i in range(9) ])
|
|
for j in range(9) ]
|
|
|
|
# each 3x3 square contains a digit at most once
|
|
sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]
|
|
for i in range(3) for j in range(3) ])
|
|
for i0 in range(3) for j0 in range(3) ]
|
|
|
|
sudoku_c = cells_c + rows_c + cols_c + sq_c
|
|
|
|
# sudoku instance, we use '0' for empty cells
|
|
instance = ((0,0,0,0,9,4,0,3,0),
|
|
(0,0,0,5,1,0,0,0,7),
|
|
(0,8,9,0,0,0,0,4,0),
|
|
(0,0,0,0,0,0,2,0,8),
|
|
(0,6,0,2,0,1,0,5,0),
|
|
(1,0,2,0,0,0,0,0,0),
|
|
(0,7,0,0,0,0,5,2,0),
|
|
(9,0,0,0,6,5,0,0,0),
|
|
(0,4,0,9,7,0,0,0,0))
|
|
|
|
instance_c = [ If(instance[i][j] == 0,
|
|
True,
|
|
X[i][j] == instance[i][j])
|
|
for i in range(9) for j in range(9) ]
|
|
|
|
s = Solver()
|
|
s.add(sudoku_c + instance_c)
|
|
if s.check() == sat:
|
|
m = s.model()
|
|
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
|
|
for i in range(9) ]
|
|
print_matrix(r)
|
|
else:
|
|
print "failed to solve"
|
|
```
|
|
## संदर्भ
|
|
|
|
* [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)
|
|
|
|
|
|
<details>
|
|
|
|
<summary><strong>जीरो से हीरो तक AWS हैकिंग सीखें</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>
|
|
|
|
HackTricks का समर्थन करने के अन्य तरीके:
|
|
|
|
* अगर आप अपनी **कंपनी का विज्ञापन HackTricks में देखना चाहते हैं** या **HackTricks को PDF में डाउनलोड करना चाहते हैं** तो [**सब्सक्रिप्शन प्लान्स**](https://github.com/sponsors/carlospolop) देखें!
|
|
* [**आधिकारिक PEASS & HackTricks स्वैग**](https://peass.creator-spring.com) प्राप्त करें
|
|
* हमारे विशेष [**NFTs**](https://opensea.io/collection/the-peass-family) कलेक्शन, [**The PEASS Family**](https://opensea.io/collection/the-peass-family) खोजें
|
|
* **शामिल हों** 💬 [**डिस्कॉर्ड समूह**](https://discord.gg/hRep4RUj7f) या [**टेलीग्राम समूह**](https://t.me/peass) और हमें **ट्विटर** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)** पर **फॉलो** करें।
|
|
* **हैकिंग ट्रिक्स साझा करें** द्वारा **पीआर** सबमिट करके [**HackTricks**](https://github.com/carlospolop/hacktricks) और [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github रेपो में।
|
|
|
|
</details>
|