რა არის სმარტ კონტრაქტების ფორმალური ვერიფიკაცია?

ეს სტატია გახლავთ ხალხის მიერ წარმოდგენილი. ავტორი გახლავთ დავით ტარტიდი, CertiK-ის, Web3-ის სმარტ კონტრაქტის აუდიტის ფირმის ვიცე-პრეზიდენტი ინჟინერიის სფეროში.
TL;DR

სმარტ კონტრაქტების ფორმალური ვერიფიკაცია უზრუნველყოფს მათ გათავისუფლებას ბაგებისგან, დაუცველობისგან და სხვა გაუთვალისწინებელი შემთხვევებისგან. ის მოიცავს ადამიან ექსპერტს, რომელიც წარმოადგენს სმარტ კონტრაქტში ჩადებულ ლოგიკას მათემატიკური ფორმულირების სახით, შემდეგ ამუშავებს მათ ავტომატიზებული პროცესის სახით, რომელიც ამოწმებს კონტრაქტის შესაძლო შედეგის მოდელებთან მიმართებაში რეალური ლოგიკის მოქმედებას. ფორმალური ვერიფიკაციისა და მექანიკური აუდიტის კომბინაცია შედეგად გვაძლევს სმარტ კონტრაქტის უსაფრთხოების დონის საფუძვლიან შეფასებას.
შესავალისმარტ კონტრაქტები გახლავთ ბლოკჩეინზე განთავსებული კომპიუტერული პროგრამები, რომლებიც ავტომატურად აქტიურდება კონკრეტული პირობების დაკმაყოფილების შემთხვევაში. ისინი შეიძლება იყოს როგორც მარტივი, ისე უკიდურესად რთული და მოიცავდეს მილიონობით, ან თუნდაც მილიარდობით დოლარის ღირებულების აქტივებს.  
სმარტ კონტრაქტების დაუცველობას უსაფრთხოების საკითხებთან დაკავშირებით შესაძლოა გამანადგურებელი შედეგები მოჰყვეს, რაც შესაძლოა მოიცავდეს სმარტ კონტრაქტზე არსებული ყველა აქტივის მოპარვას. 2021 წელს, ბაზრის ავტომატურმა maker-მა (AMM) Uranium Finance-მა, სმარტ კონტრაქტში არსებული მართლწერის მხოლოდ ერთი შეცდომის გამო $50 მილიონი დაკარგა.
ასევე 2021 წელს, Compound Finance-მა $80 მილიონის ოდენობის გაუცემელი ჯილდო დაკარგა მხოლოდ ერთი არასწორი სიმბოლოს გამო. 2022 წელს, $320 მილიონი მოპარეს Wormhole Bridge-ს, მის ერთ-ერთ სმარტ კონტრაქტში ბაგის არსებობის გამო.
მნიშვნელოვანია სმარტ კონტრაქტის სწორი პროგრამის პირველივე ჯერზე მიღება. სმარტ კონტრაქტები ღია კოდი პროგრამებია, რაც იმას ნიშნავს, რომ კოდი საჯარო ხდება კონტრაქტის ამოქმედების შემდეგ. თუ ჰაკერი ბაგს აღმოაჩენს, მას იმწამსვე შეუძლია ამით სარგებლობა. გარდა ამისა, არ არის შესაძლებელი უსაფრთხოების საკითხებთან დაკავშირებული დაუცველობის დროთა განმავლობაში გამოსწორება, რადგან, როგორც წესი, სმარტ კონტრაქტის კოდის შეცვლა შეუძლებელია მისი ამოქმედების შემდეგ.
როგორ მუშაობს სმარტ კონტრაქტის ვერიფიკაცია?  სმარტ კონტრაქტების ფორმალური ვერიფიკაცია მოქმედებს სმარტ კონტრაქტების ლოგიკისა და სასურველი მოქმედების მათემატიკური ფორმულირებით წარმოდგენის გზით. ამის შემდეგ, აუდიტორები იყენებენ ავტომატურ საშუალებებს, ამ ფორმულირების სისწორის შესამოწმებლად.
ეს პროცესი მოიცავს:
კონტრაქტის სპეციფიკაციებისა და სასურველი თვისებების განსაზღვრას ფორმალურ ენაზე.
კონტრაქტის კოდის გადაწერას ფორმალური გამოსახულების სახით, როგორიცაა მათემატიკური მოდელები, ან ლოგიკა.
თეორემის ავტომატური დამადასტურებლების ან მოდელის შემმოწმებლების გამოყენება კონტრაქტის სპეციფიკაციებისა და თვისებების დასადასტურებლად.
ვერიფიკაციის პროცესის გამეორება ნებისმიერი შეცდომის და სასურველი თვისებებიდან გადახრის საპოვნელად და გამოსასწორებლად.
რატომ არის მნიშვნელოვანი სმარტ კონტრაქტის ვერიფიკაციამათემატიკური მსჯელობის გამოყენება გვეხმარება იმის უზრუნველსაყოფად, რომ ფორმალურად ვერიფიცირებული სმარტ კონტრაქტები თავისუფალია ბაგებისგან, დაუცველობისგან და სხვა გაუთვალისწინებელი ქცევისგან. ეს ასევე ხელს უწყობს კონტრაქტისადმი ნდობის გაზრდას, რადგან მისი თვისებების სისწორე სრულადაა დადასტურებული. 
ქვემოთ მოცემულია რამდენიმე მაგალითი იმისა, თუ როგორ დაეხმარა სმარტ კონტრაქტის ვერიფიკაცია მნიშვნელოვანი ფინანსური ზარალისა და სხვა დამღუპველი შედეგების თავიდან აცილებაში.  
UniswapUniswap არის ფართოდ ცნობილი AMM. Uniswap V1 სმარტ კონტრაქტის შემუშავების შემდეგ, განხორციელდა მისი ფორმალური ვერიფიკაცია. მის გამოშვებამდე, ამ ფორმალურმა ვერიფიკაციამ აღმოაჩინა და გამოასწორა დამრგვალებასთან დაკავშირებული შეცდომები, რასაც შეიძლება გამოეწვია თანხების გატანა Uniswap V1-დან. 
BalancerBalancer V2 ასევე არის AMM, რომელმაც გაიარა ფორმალური ვერიფიკაცია. ფორმალურმა ვერიფიკაციამ აღმოაჩინა და გამოასწორა საკომისიოს არასწორი გაანგარიშების შეცდომა, რომელიც ეხებოდა flash სესხის ფუნქციონალს სმარტ კონტრაქტში, რასაც შესაძლოა გამოეწვია ბირჟის დაუცველობა ქურდობის მიმართ.
SafeMoonSafeMoon V1 შეიცავდა რთულად გამოსავლენ ბაგს, რომელიც ნაპოვნი იქნა ფორმალური ვერიფიკაციის შედეგად, მისი გაშვების შემდეგ. მესაკუთრეს შეეძლო უარი ეთქვა კონტრაქტის ფლობაზე და შემდეგ ხელახლა მიეღო იგი, იმ შემთხვევაში თუ საკუთრებაზე უარის თქმამდე შესრულდებოდა გარკვეული ოპერაციები.
ეს ბაგი არ იყო გამოვლენილი SafeMoon V1 fork-ების მექანიკური აუდიტების უმეტესობაში, რადგან მისი აღმოჩენა მოითხოვდა პროგრამის ცვლადის მნიშვნელობების კონკრეტული კომბინაციების ანალიზს. ეს შეიძლება მარტივად გამორჩეს ადამიანს, ხოლო აპარატურა კი პირიქით, მას მარტივად აღმოაჩენს.
როგორ მუშაობს ერთად ფორმალური ვერიფიკაცია და მექანიკური აუდიტიფორმალური ვერიფიკაცია უზრუნველყოფს სისტემატიურ და ავტომატიზირებულ გზას კონტრაქტის ლოგიკისა და ქცევის შესამოწმებლად მისი სასურველი თვისებების მიხედვით. ეს აადვილებს პოტენციური შეცდომის ან ბაგების იდენტიფიცირებას და გამოსწორებას. ის განსაკუთრებით სასარგებლოა რთული და შეუმჩნეველი საკითხების მოსაძებნად, რომლებიც შეიძლება რთულად დასადგენი აღმოჩნდეს მექანიკური შემოწმების გზით.
მექანიკური აუდიტი მოიცავს კონტრაქტის კოდის, დიზაინისა და განლაგების ექსპერტულ განხილვას. აუდიტორი იყენებს საკუთარ გამოცდილებას და ექსპერტულ ცოდნას უსაფრთხოების რისკების იდენტიფიცირებისთვის და კონტრაქტის უსაფრთხოების ზოგადი მდგომარეობის შესაფასებლად. მათ ასევე შეუძლიათ დაადასტურონ, რომ ფორმალური ვერიფიკაციის პროცესი შესრულდა სწორედ და შეამოწმონ ნებისმიერი პრობლემა, რომელიც შეიძლება არ იყოს გამოვლენილი ავტომატური ხელსაწყოებით. 
ფორმალური ვერიფიკაციისა და მექანიკური აუდიტის კომბინაცია შედეგად გვაძლევს სმარტ კონტრაქტის უსაფრთხოების დონის საფუძვლიან და სრულ შეფასებას. ეს ზრდის ნებისმიერი დაუცველობის აღმოჩენისა და გამოსწორების შანსებს. ამის შედეგია უსაფრთხოებისადმი სიღრმისეული მიდგომა, რომელიც იყენებს როგორც ადამიანების, ასევე მანქანების უნიკალურ შესაძლებლობებს. 
შეჯამებასმარტ კონტრაქტების უსაფრთხოების უზრუნველსაყოფად, აუცილებელია გამოიყენოთ როგორც ფორმალური ვერიფიკაცია, ასევე მექანიკური აუდიტი, რათა ვუზრუნველვყოთ სმარტ კონტრაქტის უსაფრთხოების მდგომარეობის საფუძვლიანი და სრული შეფასება.
მიუხედავად იმისა, რომ ფორმალურ ვერიფიკაციას შეიძლება დასჭირდეს დიდი რესურსი, ეს არის ღირებული ინვესტიცია მაღალი ღირებულების ან მაღალი რისკის ფაქტორების მქონე კონტრაქტებისთვის. საბოლოო ჯამში, სასიცოცხლოდ მნიშვნელოვანია უსაფრთხოებისთვის პრიორიტეტის მინიჭება და სმარტ კონტრაქტების გაწმენდა შეცდომებისგან, დაუცველობისა და არასასურველი ქცევისგან.
დამატებითი საკითხავირა არის სმარტ-კონტრაქტები?
რა არის სმარტ-კონტრაქტის უსაფრთხოების აუდიტი?
უარი პასუხისმგებლობაზე და გაფრთხილება რისკის შესახებ: ეს კონტენტი თქვენთვის წარმოდგენილია „არსებული სახით“ და განკუთვნილია მხოლოდ საინფორმაციო და საგანმანათლებლო მიზნებისთვის, რაიმე სახის რეპრეზენტაციისა თუ გარანტიის გარეშე. იგი არ უნდა იქნას აღქმული, როგორც ფინანსური რჩევა და არ არის განკუთვნილი იმისთვის, რომ რეკომენდაცია გაუწიოს რაიმე სახის კონკრეტული პროდუქტის, ან სერვისის შეძენას. ციფრული აქტივების ფასები შეიძლება იყოს არასტაბილური. თქვენი ინვესტიციის ღირებულებამ შეიძლება დაიკლოს ან მოიმატოს და შესაძლოა ვერ შეძლოთ ინვესტირებული თანხის დაბრუნება. თქვენ ერთპიროვნულად ხართ პასუხისმგებელი თქვენს საინვესტიციო გადაწყვეტილებებზე და Binance Academy-ი არ არის პასუხისმგებელი თქვენ მიერ განცდილ არანაირ ზარალზე. ეს მასალა არ უნდა იქნას აღქმული, როგორც ფინანსური რჩევაა.