GAMBA

GAMBA मिश्रित बूलियन-अंकगणितीय व्यंजकों (MBAs) के सरलीकरण के लिए एक उपकरण है। GAMBA, General Advanced Mixed Boolean Arithmetic simplifier का संक्षिप्त रूप है। यह रैखिक बीजगणितीय सरलीकरणकर्ता SiMBA का उपयोग करके, संभावित अरैखिक इनपुट MBA के रैखिक उप-व्यंजकों को पुनरावृत्त रूप से सरल बनाता है। कुल मिलाकर, इसके मुख्य घटक निम्नलिखित हैं:

• अमूर्त सिंटैक्स ट्री (ASTs) का उपयोग
• (तुच्छ और अधिक परिष्कृत) रूपांतरणों को लागू करके रैखिक उप-व्यंजकों का अलगाव
• सरलीकरण योग्य रैखिक उप-व्यंजकों के निर्माण की संभावना बढ़ाने के लिए रीफैक्टरिंग
• SiMBA का उपयोग करके रैखिक उप-व्यंजकों का सरलीकरण
• बिटवाइज़ संक्रियाओं के भीतर गैर-तुच्छ स्थिरांकों और अंकगणितीय संक्रियाओं से अस्थायी रूप से छुटकारा पाने के लिए प्रतिस्थापन तर्क

GAMBA निम्नलिखित पेपर पर आधारित है, प्रस्तुति के लिए उपयोग की गई स्लाइड्स भी देखें:

@inproceedings{gamba2023,
    author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
    title = {Simplification of General Mixed Boolean-Arithmetic Expressions: {GAMBA}},
    address = {Delft, The Netherlands},
    year = {2023},
    month = jul,
    publisher = {IEEE},
    pages = {427--438},
    doi = {10.1109/EuroSPW59978.2023.00053},
    howpublished = {https://arxiv.org/abs/2305.06763},
    booktitle = {Proceedings of the 2nd Workshop on Robust Malware Analysis, WORMA'23, 
                 co-located with the 8th IEEE European Symposium on Security and Privacy}
}

सामग्री

दो मुख्य प्रोग्राम प्रदान किए गए हैं:

• simplify_general.py सामान्य MBAs के सरलीकरण के लिए
• simplify.py रैखिक MBAs के सरलीकरण के लिए

इसके अतिरिक्त, पेपर में बताए गए परिणामों को पुन: प्रस्तुत करने के लिए एक परीक्षण स्क्रिप्ट भी प्रदान की गई है।

उपयोग

एकल सामान्य व्यंजकों को सरल बनाना

एकल व्यंजक expr को सरल बनाने के लिए, उपयोग करें

python3 src/simplify_general.py "expr"

वैकल्पिक रूप से, एक साथ कई व्यंजकों को सरल बनाया जा सकता है, जैसे:

python3 src/simplify_general.py "x+x" "y*y" "a&a"

वास्तव में, प्रत्येक कमांड लाइन तर्क जो कोई विकल्प नहीं है, सरलीकृत किए जाने वाले व्यंजक के रूप में माना जाता है। ध्यान दें कि उद्धरण चिह्नों को छोड़ने से अवांछित व्यवहार हो सकता है। सरलीकरण परिणाम कमांड लाइन पर निम्नानुसार मुद्रित होते हैं:

*** Expression x+x
*** ... simplified to 2*x
*** Expression y*y
*** ... simplified to y**2
*** Expression a
*** ... simplified to a

यदि विकल्प -z का उपयोग किया जाता है, तो सरलीकरण परिणामों को Z3 का उपयोग करके अंततः मूल व्यंजकों के शब्दार्थ रूप से समतुल्य होने की पुष्टि की जाती है। जब तक एल्गोरिथ्म सही ढंग से काम करता है, यह कमांड लाइन आउटपुट को प्रभावित नहीं करता है:

python3 src/simplify_general.py "x+x" -z

यदि एल्गोरिथ्म गलत परिणाम देता है, तो निम्नलिखित त्रुटि उत्पन्न होगी:

*** Expression x+x
Error in simplification! Simplified expression is not equivalent to original one!

इसके अतिरिक्त, एक विशिष्ट बिट गणना तक के सभी संभावित इनपुटों के साथ परिणामों का संख्यात्मक सत्यापन किया जा सकता है। यह विकल्प -v के साथ सक्षम होता है, जिसके बाद उपयोग किए गए इनपुटों की अधिकतम बिट गणना होती है:

python3 src/simplify_general.py "x+x" -v 3

फिर से गलत परिणाम के मामले में, आउटपुट निम्न जैसा हो सकता है:

*** Expression x+x
*** ... verify via evaluation ... [                    ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2

GAMBA के आउटपुट व्यंजकों में पाए जाने वाले स्थिरांक स्पष्ट रूप से स्थिरांकों और चरों दोनों के लिए उपयोग की गई बिटों की संख्या पर निर्भर कर सकते हैं। यह संख्या डिफ़ॉल्ट रूप से $64$ है और इसे विकल्प -b का उपयोग करके सेट किया जा सकता है:

python3 src/simplify_general.py "-x" -b 32

डिफ़ॉल्ट रूप से, आउटपुट में पाए जाने वाले स्थिरांकों को शून्य के जितना संभव हो उतना निकट निरूपण में रिपोर्ट किया जाता है। अर्थात, उपरोक्त मामले में, संख्या -1 वैसी ही रहेगी:

*** Expression -x
*** ... simplified to -x

इस व्यवहार को बदला जा सकता है: विकल्प -m का उपयोग करने से स्थिरांकों की मॉड्यूलो-कमी सक्षम होती है:

python3 src/simplify_general.py "-x" -b 32 -m

फिर, $b$ बिटों की संख्या के लिए, स्थिरांक हमेशा $0$ और $2^b-1$ के बीच होते हैं। अतः उपरोक्त कॉल का परिणाम निम्न आउटपुट होगा:

*** Expression -x
*** ... simplified to 4294967295*x

एकल रैखिक व्यंजकों को सरल बनाना

फ़ाइल src/simplify.py को src/simplify_general.py द्वारा उपयोग किए जाने के लिए बनाया गया है, लेकिन इसे अलग से भी चलाया जा सकता है। उपलब्ध सेटिंग्स देखने के लिए कमांड लाइन विकल्प -h का उपयोग करें।

प्रयोगों की पुनरुत्पत्ति

फ़ाइल experiments/tests.py का उपयोग पेपर में बताए गए प्रयोगों को पुन: प्रस्तुत करने के लिए किया जा सकता है। डिफ़ॉल्ट रूप से यह GAMBA को 6 डेटासेट पर चलाता है:

python3 experiments/tests.py

वैकल्पिक रूप से, इसे विकल्प --linear या -l का उपयोग करके इसके बजाय SiMBA चलाने का निर्देश दिया जा सकता है। उस स्थिति में, SiMBA केवल रैखिक ग्राउंड ट्रुथ वाले MBAs पर चलाया जाता है:

python3 experiments/tests.py --linear

संख्यात्मक जाँच या Z3 का उपयोग करने वाली जाँच को क्रमशः विकल्पों --check (-c) या --z3 (-z) के माध्यम से सक्षम किया जा सकता है।

व्यंजकों को सरलीकरण या सत्यापन की सफलता के आधार पर वर्गीकृत किया गया है:

• ok: वे व्यंजक जो संबंधित ग्राउंड ट्रुथ के बिल्कुल समान परिणाम में सरलीकृत होते हैं
• okz: वे व्यंजक जिनकी ग्राउंड ट्रुथ के साथ समतुल्यता को एल्गोरिथ्म का उपयोग करके सत्यापित किया जा सकता है (व्यंजक में से ग्राउंड ट्रुथ व्यंजक को घटाकर प्राप्त व्यंजक को 0 तक सरलीकृत करके)
• z3: वे व्यंजक जिनकी ग्राउंड ट्रुथ के साथ समतुल्यता को Z3 का उपयोग करके सत्यापित किया जा सकता है
• to: वे व्यंजक जिनके लिए एल्गोरिथ्म टाइमआउट में चला गया
• ng: वे व्यंजक जिनके लिए सरलीकरण और सत्यापन सफल नहीं हुए
• nc: वे व्यंजक जिनके लिए एल्गोरिथ्म, SiMBA का उपयोग किए जाने पर, नहीं चलाया गया क्योंकि ग्राउंड ट्रुथ रैखिक नहीं हैं
• err: वे व्यंजक जिनके लिए कोई त्रुटि हुई

डेटासेट

experiments/tests.py के साथ उपयोग के लिए डेटासेट experiments/datasets/ निर्देशिका में पाए जा सकते हैं।

• neureduce.txt: विकल्प -d 0 का उपयोग करें; https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv से (कुछ सुधारों के साथ)
• mba_obf_linear.txt: विकल्प -d 1 का उपयोग करें; https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt से (1000 रैखिक व्यंजक)
• mba_obf_nonlinear.txt: विकल्प -d 2 का उपयोग करें; https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt और https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt से (प्रत्येक में 500 व्यंजक; गैर-बहुपदीय व्यंजकों के लिए कुछ सुधारों के साथ)
• syntia.txt: विकल्प -d 3 का उपयोग करें; MBA-Flatten, dataset/dataset_syntia.txt से
• mba_flatten.txt: विकल्प -d 4 का उपयोग करें; MBA-Flatten, dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt से पहले 1000 व्यंजक
• qsynth_ea.txt: विकल्प -d 5 का उपयोग करें; https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json से

इसके अतिरिक्त, निम्नलिखित बोनस डेटासेट experiments/datasets/bonus/ निर्देशिका में प्रदान किए गए हैं (प्रकाशन में शामिल नहीं):

• loki_tiny.txt: विकल्प -d 6 का उपयोग करें; https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data से, LOKI पेपर द्वारा सरल ग्राउंड ट्रुथ व्यंजकों ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$) के लिए उत्पन्न 25000 MBAs, गहराई 5 तक

MBAs का प्रारूप

चरों की संख्या सिद्धांत रूप में असीमित है, लेकिन निश्चित रूप से चर गणना के साथ रनटाइम बढ़ता है। चरों के संकेतन पर कोई कठोर प्रतिबंध नहीं है। उन्हें एक अक्षर से शुरू होना चाहिए और उनमें अक्षर, संख्याएँ और अंडरस्कोर हो सकते हैं। उदाहरण के लिए, निम्नलिखित चर नाम सभी मान्य होंगे:

• $a$, $b$, $c$, ..., $x$, $y$, $z$, ...
• $v0$, $v1$, $v2$, ...
• $v_0$, $v_1$, $v_2$, ...
• $X0$, $X1$, $X2$, ...
• $var0$, $var1$, $var2$, ...
• $var1a$, $var1b$, $var1c$, ...
• ...

निम्नलिखित ऑपरेटर समर्थित हैं, Python में उनकी प्राथमिकता के क्रम में:

• $**$: घातांक
• $\mathord{\sim}$, $-$: बिटवाइज़ निषेध और यूनरी माइनस
• $*$: गुणनफल
• $+$, $-$: योग और अंतर
• <<: बायां शिफ्ट
• &: संयोजन
• $\mathbin{^\wedge}$: एक्सक्लूसिव डिस्जंक्शन
• $|$: इनक्लूसिव डिस्जंक्शन

इनपुट व्यंजकों में व्हाइटस्पेस का उपयोग किया जा सकता है। उदाहरण के लिए, व्यंजक "x+y" को वैकल्पिक रूप से "x + y" के रूप में भी लिखा जा सकता है।

कृपया ऑपरेटरों की प्राथमिकता का सम्मान करें और आवश्यक होने पर कोष्ठकों का उपयोग करें! उदाहरण के लिए, व्यंजक $1 + (x|y)$ और $1 + x|y$ समतुल्य नहीं हैं क्योंकि $+$ की प्राथमिकता $|$ से अधिक है। ध्यान दें कि बाद वाला व्यंजक तो रैखिक MBA भी नहीं है।

निर्भरताएँ

Z3

यदि सरलीकृत व्यंजकों का वैकल्पिक सत्यापन उपयोग किया जाता है, तो SMT सॉल्वर Z3, simplify_general.py और simplify.py के लिए आवश्यक है। यदि यह विकल्प उपयोग नहीं किया जाता है, तो Z3 स्थापित न होने पर भी कोई त्रुटि नहीं फेंकी जाती है।

Z3 स्थापित करना:

• Github रिपॉजिटरी से: https://github.com/Z3Prover/z3
• Debian पर: sudo apt-get install python3-z3

NumPy

वैज्ञानिक कंप्यूटिंग पैकेज NumPy आलस्य के कारण आवश्यक है, लेकिन संचालन के लिए वास्तव में आवश्यक नहीं है। नोट: numpy.quantile के लिए कम से कम संस्करण 1.15.0 आवश्यक है।

NumPy स्थापित करना:

• Github रिपॉजिटरी से: https://github.com/numpy/numpy.git
• Debian पर: sudo apt-get install python3-numpy

लाइसेंस

कॉपीराइट (c) 2023 Denuvo GmbH, GPLv3 के अंतर्गत जारी किया गया।

संपर्क

• Benjamin Reichenwallner: benjamin(dot)reichenwallner(at)denuvo(dot)com
• Peter Meerwald-Stadler: peter(dot)meerwald(at)denuvo(dot)com