👨🏾‍🤝‍👨🏼 🐛 🐲 खरोंच से एक औपचारिक सत्यापन प्रणाली का निर्माण। भाग 1: PHP और पायथन में चरित्र आभासी मशीन 👐🏻 🎖️ 👩🏻‍🍳

औपचारिक सत्यापन एक कार्यक्रम या एल्गोरिथ्म का सत्यापन है जो दूसरे का उपयोग करता है।

यह सबसे शक्तिशाली तरीकों में से एक है जो आपको कार्यक्रम में सभी कमजोरियों को खोजने या यह साबित करने की अनुमति देता है कि वे वहां नहीं हैं।

औपचारिक सत्यापन का अधिक विस्तृत विवरण मेरे पिछले लेख में वुल्फ, बकरी और गोभी की समस्या को हल करने के उदाहरण पर देखा जा सकता है।

इस लेख में, मैं कार्यक्रमों के कार्यों के औपचारिक सत्यापन से गुजरूंगा, और मैं वर्णन करूंगा
स्वचालित रूप से उन्हें औपचारिक नियम प्रणालियों में कैसे परिवर्तित किया जाए।

इसके लिए, मैंने प्रतीकात्मक सिद्धांतों पर, एक आभासी मशीन का अपना एनालॉग लिखा।

वह प्रोग्राम कोड को पार्स करती है और इसे समीकरणों (एसएमटी) की एक प्रणाली में तब्दील करती है, जिसे पहले से प्रोग्रामेटिक रूप से हल किया जा सकता है।

चूंकि प्रतीकात्मक गणनाओं की जानकारी इंटरनेट पर प्रस्तुत की जाती है, बल्कि
मैं संक्षेप में बताऊंगा कि यह क्या है।

चरित्र गणना डेटा की एक विस्तृत श्रृंखला पर एक साथ एक कार्यक्रम को निष्पादित करने का एक तरीका है और कार्यक्रमों के औपचारिक सत्यापन के लिए मुख्य उपकरण है।

उदाहरण के लिए, हम इनपुट स्थितियां निर्धारित कर सकते हैं जहां पहला तर्क किसी भी सकारात्मक मान, दूसरा नकारात्मक, तीसरा - शून्य और आउटपुट तर्क ले सकता है, उदाहरण के लिए, 42।

एक रन में प्रतीकात्मक गणना हमें जवाब देगी, क्या हमारे लिए वांछित परिणाम और ऐसे इनपुट मापदंडों के सेट का एक उदाहरण प्राप्त करना संभव है। या सबूत है कि ऐसे कोई पैरामीटर नहीं हैं।

इसके अलावा, हम सामान्य रूप से इनपुट तर्कों को सेट कर सकते हैं, और केवल आउटपुट का चयन कर सकते हैं, उदाहरण के लिए, व्यवस्थापक पासवर्ड।

इस मामले में, हमें प्रोग्राम की सभी कमजोरियां मिलेंगी या हमें यह प्रमाण मिलेगा कि एडमिन पासवर्ड सुरक्षित है।

आप देख सकते हैं कि विशिष्ट इनपुट डेटा के साथ एक कार्यक्रम का शास्त्रीय निष्पादन एक प्रतीकात्मक का एक विशेष मामला है।

इसलिए, मेरा चरित्र VM एक मानक वर्चुअल मशीन के अनुकरण मोड में भी काम कर सकता है।

पिछले लेख की टिप्पणियों में, आप इसकी कमजोरियों की चर्चा के साथ औपचारिक सत्यापन की उचित आलोचना पा सकते हैं।

मुख्य समस्याएं इस प्रकार हैं:

संयुक्त विस्फोट, चूंकि औपचारिक सत्यापन अंततः पी = एनपी पर टिकी हुई है
फ़ाइल सिस्टम, नेटवर्क और अन्य बाहरी संग्रहण पर कॉलों को संभालना सत्यापित करना अधिक कठिन है
विनिर्देश में कीड़े, जब ग्राहक या प्रोग्रामर ने एक चीज की कल्पना की, लेकिन ToR में इसका सही वर्णन नहीं किया।

नतीजतन, कार्यक्रम को सत्यापित किया जाएगा और विनिर्देशों को पूरा किया जाएगा, लेकिन यह बिल्कुल नहीं करेगा कि रचनाकारों को इससे क्या उम्मीद है।

चूंकि इस लेख में मैं मुख्य रूप से व्यवहार में औपचारिक सत्यापन के आवेदन पर विचार करता हूं, मैं अभी तक दीवार के खिलाफ अपने माथे को नहीं हराऊंगा, और मैं एक ऐसी प्रणाली चुनूंगा जहां एल्गोरिथम जटिलता और बाहरी कॉल की संख्या न्यूनतम है।

चूंकि स्मार्ट कॉन्ट्रैक्ट्स इन आवश्यकताओं को सबसे अच्छे तरीके से सूट करते हैं, इसलिए पसंद वेव्स प्लेटफॉर्म से RIDE अनुबंधों पर गिर गई: वे ट्यूरिंग-पूर्ण नहीं हैं, और उनकी अधिकतम जटिलता कृत्रिम रूप से सीमित है।

लेकिन हम उन्हें पूरी तरह से तकनीकी पक्ष से विचार करेंगे।

सभी के अलावा, किसी भी अनुबंध के लिए, औपचारिक सत्यापन विशेष रूप से मांग में होगा: एक नियम के रूप में, इसके लॉन्च के बाद एक अनुबंध त्रुटि को ठीक करना असंभव है।
और ऐसी त्रुटियों की कीमत बहुत अधिक हो सकती है, क्योंकि बड़ी मात्रा में धन अक्सर स्मार्ट अनुबंधों पर संग्रहीत होते हैं।

मेरा चरित्र वर्चुअल मशीन PHP और पायथन में लिखा गया है, और परिणामी SMT सूत्रों को हल करने के लिए Microsoft रिसर्च के Z3Prover का उपयोग करता है।

इसके मूल में एक शक्तिशाली बहु-लेन-देन खोज है, जो
आपको समाधान या कमजोरियां खोजने की अनुमति देता है, भले ही इसके लिए बहुत अधिक लेनदेन की आवश्यकता हो।
यहां तक कि इथेरियम कमजोरियों की खोज के लिए सबसे शक्तिशाली प्रतीकात्मक रूपरेखाओं में से एक, माइथ्रिल ने कुछ महीने पहले ही इस सुविधा को जोड़ा था।

लेकिन यह ध्यान देने योग्य है कि ईथर के अनुबंध अधिक जटिल हैं और ट्यूरिंग पूर्णता है।

PHP RIDE स्मार्ट कॉन्ट्रैक्ट के स्रोत कोड को एक पाइथन स्क्रिप्ट में अनुवादित करता है जिसमें प्रोग्राम को Z3 SMT के साथ संगत उनके बदलावों के लिए अनुबंध की शर्तों और शर्तों की एक प्रणाली के रूप में प्रस्तुत किया जाता है:

अब मैं वर्णन करूंगा कि अंदर क्या हो रहा है, अधिक विस्तार से।

लेकिन पहले, स्मार्ट अनुबंध RIDE की भाषा के बारे में कुछ शब्द।

यह एक कार्यात्मक और अभिव्यक्ति-आधारित प्रोग्रामिंग भाषा है जो कि इच्छानुसार आलसी है।
RIDE को ब्लॉकचेन के भीतर अलगाव में किया जाता है, और उपयोगकर्ता के बटुए से जुड़े भंडारण से जानकारी निकाल और लिख सकता है।

आप प्रत्येक वॉलेट में RIDE अनुबंध संलग्न कर सकते हैं, और निष्पादन का परिणाम केवल TRUE या FALSE होगा।

TRUE का अर्थ है कि स्मार्ट अनुबंध लेन-देन की अनुमति देता है, और FALSE कि यह इसे मना करता है।
एक सरल उदाहरण: एक स्क्रिप्ट एक हस्तांतरण को रोक सकती है यदि बटुआ संतुलन 100 से कम है।

एक उदाहरण के रूप में, मैं सभी एक ही वुल्फ, बकरी और गोभी ले जाऊंगा, लेकिन पहले से ही एक स्मार्ट अनुबंध के रूप में प्रस्तुत किया गया है।

उपयोगकर्ता उस बटुए से पैसे नहीं निकाल पाएगा जिस पर अनुबंध को तैनात किया गया है जब तक कि वह हर किसी को दूसरी तरफ नहीं भेजता।

#      let contract = tx.sender let human= extract(getInteger(contract,"human")) let wolf= extract(getInteger(contract,"wolf")) let goat= extract(getInteger(contract,"goat")) let cabbage= extract(getInteger(contract,"cabbage")) #   -,      4 . #           . match tx { case t:DataTransaction => #       let newHuman= extract(getInteger(t.data,"human")) let newWolf= extract(getInteger(t.data,"wolf")) let newGoat= extract(getInteger(t.data,"goat")) let newCabbage= extract(getInteger(t.data,"cabbage")) #0 ,     ,  1    let humanSide= human == 0 || human == 1 let wolfSide= wolf == 0 || wolf == 1 let goatSide= goat == 0 || goat == 1 let cabbageSide= cabbage == 0 || cabbage == 1 let side= humanSide && wolfSide && goatSide && cabbageSide #    ,        . let safeAlone= newGoat != newWolf && newGoat != newCabbage let safe= safeAlone || newGoat == newHuman let humanTravel= human != newHuman #     ,  -   . let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1 let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1 let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7 #        . #     1  0,    #  ,        #  -    side && safe && humanTravel && objectTravel case s:TransferTransaction => #             human == 1 && wolf == 1 && goat == 1 && cabbage == 1 #     case _ => false }

PHP सबसे पहले स्मार्ट कॉन्ट्रैक्ट से निकाले गए सभी वेरिएबल्स को उनकी चाबियों के रूप में और लॉजिकल एक्सप्रेशन के संगत वेरिएबल के रूप में निकालता है।

 cabbage: extract ( getInteger ( contract , "cabbage" ) ) goat: extract ( getInteger ( contract , "goat" ) ) human: extract ( getInteger ( contract , "human" ) ) wolf: extract ( getInteger ( contract , "wolf" ) ) fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1 fState: wolf: goat: cabbage: cabbageSide: cabbage== 0 || cabbage== 1 human: extract ( getInteger ( contract , "human" ) ) newGoat: extract ( getInteger ( t.data , "goat" ) ) newHuman: extract ( getInteger ( t.data , "human" ) ) goatSide: goat== 0 || goat== 1 humanSide: human== 0 || human== 1 t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1 t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1 t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage safeAlone: newGoat != newWolf && newGoat != newCabbage wolfSide: wolf== 0 || wolf== 1 humanTravel: human != newHuman side: humanSide && wolfSide && goatSide && cabbageSide safe: safeAlone || newGoat== newHuman objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7

तब PHP उन्हें Z3Prover SMT के लिए एक संगत पायथन सिस्टम विवरण में परिवर्तित करता है।
डेटा को एक चक्र में लपेटा जाता है, जहां स्टोरेज वेरिएबल्स को इंडेक्स i, ट्रांजेक्शन वेरिएबल्स इंडेक्स i + 1 मिलता है, और एक्सप्रेशंस वाले वेरिएबल पिछले राज्य से अगले में ट्रांस्फ़ॉर्म के लिए नियम निर्धारित करते हैं।

यह हमारे आभासी मशीन का बहुत ही दिल है, जो एक बहु-लेनदेन खोज इंजन प्रदान करता है।

 fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 ) final: fState[Steps] fState: wolf: goat: cabbage: cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 ) goatSide: Or( goat[i] == 0 , goat[i] == 1 ) humanSide: Or( human[i] == 0 , human[i] == 1 ) t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 ) t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 ) t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] ) t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] ) t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] ) safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage ) wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 ) humanTravel: human[i] != human[i+1] side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) safe: Or( safeAlone[i] , goat[i+1] == human[i+1] ) objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )

शर्तों को क्रमबद्ध किया जाता है और एक स्क्रिप्ट टेम्पलेट में डाला जाता है जिसे अजगर में एसएमटी प्रणाली का वर्णन करने के लिए डिज़ाइन किया गया है।

खाली खाका

 import json from z3 import * s = Solver() Steps=7 Num= Steps+1 $code$ #template, only start rest s.add(data + start) #template s.add(final) ind = 0 f = open("/var/www/html/all/bin/python/log.txt", "a") while s.check() == sat: ind = ind +1 print ind m = s.model() print m print "traversing model..." #for d in m.decls(): #print "%s = %s" % (d.name(), m[d]) f.write(str(m)) f.write("\n\n") exit() #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model print "Total solution number: " print ind f.close()

संपूर्ण श्रृंखला से अंतिम स्थिति के लिए, हस्तांतरण लेनदेन अनुभाग में निर्दिष्ट नियम लागू होते हैं।

तो, Z3Prover बस शर्तों के ऐसे सेट की तलाश करेगा जो अंततः आपको अनुबंध से धन निकालने की अनुमति देगा।

नतीजतन, हम स्वचालित रूप से हमारे अनुबंध के पूरी तरह से काम कर रहे एसएमटी मॉडल प्राप्त करते हैं।
आप देख सकते हैं कि यह मेरे पिछले लेख से मॉडल के समान है, जिसे मैंने मैन्युअल रूप से लिखा था।

पूरा टेम्प्लेट

 import json from z3 import * s = Solver() Steps=7 Num= Steps+1 human = [ Int('human_%i' % (i + 1)) for i in range(Num) ] wolf = [ Int('wolf_%i' % (i + 1)) for i in range(Num) ] goat = [ Int('goat_%i' % (i + 1)) for i in range(Num) ] cabbage = [ Int('cabbage_%i' % (i + 1)) for i in range(Num) ] nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ] start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ] safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ] safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ] humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ] cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ] goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ] humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ] t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ] t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ] t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ] wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ] side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ] objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ] data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ] fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 ) final= fState #template, only start rest s.add(data + start) #template s.add(final) ind = 0 f = open("/var/www/html/all/bin/python/log.txt", "a") while s.check() == sat: ind = ind +1 print ind m = s.model() print m print "traversing model..." #for d in m.decls(): #print "%s = %s" % (d.name(), m[d]) f.write(str(m)) f.write("\n\n") exit() #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model print "Total solution number: " print ind f.close()

लॉन्च के बाद, Z3Prover एक स्मार्ट अनुबंध को हल करता है और हमारे लिए एक लेनदेन श्रृंखला प्रदर्शित करता है, जो हमें धन निकालने की अनुमति देगा:

 Winning transaction chain found: Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0 Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1 Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1 Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1 Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1 Transfer transaction

अग्रेषण अनुबंध के अलावा, आप अपने स्वयं के अनुबंधों के साथ प्रयोग कर सकते हैं या इस सरल उदाहरण की कोशिश कर सकते हैं, जो 2 लेनदेन में हल किया गया है।

 let contract = tx.sender let a= extract(getInteger(contract,"a")) let b= extract(getInteger(contract,"b")) let c= extract(getInteger(contract,"c")) let d= extract(getInteger(contract,"d")) match tx { case t:DataTransaction => let na= extract(getInteger(t.data,"a")) let nb= extract(getInteger(t.data,"b")) let nc= extract(getInteger(t.data,"c")) let nd= extract(getInteger(t.data,"d")) nd == 0 || a == 100 - 5 case s:TransferTransaction => ( a + b - c ) * d == 12 case _ => true }

चूंकि यह बहुत पहला संस्करण है, वाक्यविन्यास बहुत सीमित है और बग्स हो सकते हैं।
निम्नलिखित लेखों में, मैं वीएम के आगे के विकास को उजागर करने की योजना बना रहा हूं, और दिखाऊंगा कि इसकी मदद से औपचारिक रूप से सत्यापित स्मार्ट अनुबंध बनाना कैसे संभव है, और न केवल उन्हें हल करना।

एक प्रतीकात्मक आभासी मशीन http://2.59.42.98/hyperbox/ पर उपलब्ध है
स्रोत github पर उपलब्ध हैं: http://github.com/scp1001/hyperbox
सभी वीएम लॉजिक 2 फाइलों, हाइपरबॉक्स.फपी और हाइपरबॉक्स 2.php में समाहित है

खरोंच से एक औपचारिक सत्यापन प्रणाली का निर्माण। भाग 1: PHP और पायथन में चरित्र आभासी मशीन

More articles: