Τυπική επαλήθευση των έξυπνων συμβολαίων

Τα έξυπνα συμβόλαια καθιστούν δυνατή τη δημιουργία αποκεντρωμένων, χωρίς ανάγκη εμπιστοσύνης και ανθεκτικών εφαρμογών που εισάγουν νέες περιπτώσεις χρήσης και ξεκλειδώνουν αξία για τους χρήστες. Επειδή τα έξυπνα συμβόλαια χειρίζονται μεγάλες ποσότητες αξίας, η ασφάλεια είναι μια κρίσιμη παράμετρος για τους προγραμματιστές.

Η τυπική επαλήθευση είναι μία από τις προτεινόμενες τεχνικές για τη βελτίωση της ασφάλειας των έξυπνων συμβολαίων. Η τυπική επαλήθευση, η οποία χρησιμοποιεί τυπικές μεθόδους(opens in a new tab) για τον ορισμό προδιαγραφών, τη σχεδίαση και επαλήθευση προγραμμάτων, χρησιμοποιείται εδώ και χρόνια για να διασφαλίσει τη σωστή λειτουργία κρίσιμων συστημάτων υλισμικού και λογισμικού.

Όταν εφαρμόζεται σε έξυπνα συμβόλαια, η τυπική επαλήθευση μπορεί να αποδείξει ότι η επιχειρηματική λογική μιας σύμβασης πληροί μια προκαθορισμένη προδιαγραφή. Σε σύγκριση με άλλες μεθόδους αξιολόγησης της ορθότητας του κώδικα συμβολαίου, όπως οι δοκιμές, η τυπική επαλήθευση παρέχει ισχυρότερες εγγυήσεις ότι ένα έξυπνο συμβόλαιο είναι λειτουργικά σωστό.

Τι είναι η τυπική επαλήθευση;

Η τυπική επαλήθευση αναφέρεται στη διαδικασία αξιολόγησης της ορθότητας ενός συστήματος σε σχέση με μια τυπική προδιαγραφή. Με απλούστερους όρους, η τυπική επαλήθευση μας επιτρέπει να ελέγξουμε εάν η συμπεριφορά ενός συστήματος ικανοποιεί κάποιες απαιτήσεις (δηλαδή, κάνει αυτό που θέλουμε).

Οι αναμενόμενες συμπεριφορές του συστήματος (ένα έξυπνο συμβόλαιο σε αυτήν την περίπτωση) περιγράφονται χρησιμοποιώντας τυπική μοντελοποίηση, ενώ οι γλώσσες προδιαγραφής επιτρέπουν τη δημιουργία τυπικών ιδιοτήτων. Οι τεχνικές τυπικής επαλήθευσης μπορούν στη συνέχεια να επαληθεύσουν ότι η υλοποίηση ενός συμβολαίου συμμορφώνεται με την προδιαγραφή της και να παράγουν μαθηματική απόδειξη της ορθότητας της πρώτης. Όταν ένα συμβόλαιο ικανοποιεί τις προδιαγραφές του, περιγράφεται ως «λειτουργικά σωστό», «σωστό από τον σχεδιασμό» ή «σωστό από την κατασκευή».

Τι είναι τυπικό μοντέλο;

Στην επιστήμη των υπολογιστών, ένα τυπικό μοντέλο(opens in a new tab) είναι μια μαθηματική περιγραφή μιας υπολογιστικής διαδικασίας. Τα προγράμματα συνοψίζονται αφαιρετικά σε μαθηματικές συναρτήσεις (εξισώσεις), με το μοντέλο να περιγράφει πώς υπολογίζονται τα αποτελέσματα των συναρτήσεων με δεδομένο ένα στοιχείο εισόδου.

Τα τυπικά μοντέλα παρέχουν ένα επίπεδο αφαιρετικότητας πάνω από το οποίο μπορεί να αξιολογηθεί η ανάλυση της συμπεριφοράς ενός προγράμματος. Η ύπαρξη τυπικών μοντέλων επιτρέπει τη δημιουργία μιας τυπικής προδιαγραφής, η οποία περιγράφει τις επιθυμητές ιδιότητες του εν λόγω μοντέλου.

Διαφορετικές τεχνικές χρησιμοποιούνται για τη μοντελοποίηση έξυπνων συμβολαίων για τυπική επαλήθευση. Για παράδειγμα, ορισμένα μοντέλα χρησιμοποιούνται για να εξάγουν συμπεράσματα σχετικά με τη συμπεριφορά υψηλού επιπέδου ενός έξυπνου συμβολαίου. Αυτές οι τεχνικές μοντελοποίησης εφαρμόζουν μια προβολή μαύρου κουτιού στα έξυπνα συμβόλαια, θεωρώντας τα ως συστήματα που δέχονται στοιχεία εισόδου και εκτελούν υπολογισμούς με βάση αυτά τα στοιχεία.

Τα μοντέλα υψηλού επιπέδου επικεντρώνονται στη σχέση μεταξύ έξυπνων συμβολαίων και εξωτερικών παραγόντων, όπως εξωτερικά κατεχόμενοι λογαριασμοί (EOA), λογαριασμοί συμβολαίων και το περιβάλλον της αλυσίδας συστοιχιών. Τέτοια μοντέλα είναι χρήσιμα για τον ορισμό ιδιοτήτων που καθορίζουν πώς πρέπει να συμπεριφέρεται ένα συμβόλαιο ως απόκριση σε ορισμένες αλληλεπιδράσεις χρήστη.

Αντίθετα, άλλα επίσημα μοντέλα επικεντρώνονται στη συμπεριφορά χαμηλού επιπέδου ενός έξυπνου συμβολαίου. Ενώ τα μοντέλα υψηλού επιπέδου μπορούν να βοηθήσουν στην εξαγωγή συμπερασμάτων σχετικά με τη λειτουργικότητα ενός συμβολαίου, ενδέχεται να μην καταφέρουν να καταγράψουν λεπτομέρειες σχετικά με τις εσωτερικές καταστάσεις λειτουργίας της υλοποίησης. Τα μοντέλα χαμηλού επιπέδου εφαρμόζουν μια προβολή λευκού κουτιού στην ανάλυση προγράμματος και βασίζονται σε αναπαραστάσεις χαμηλού επιπέδου εφαρμογών έξυπνων συμβολαίων, όπως ίχνη προγράμματος και γραφήματα ροής ελέγχου(opens in a new tab), για να εξάγουν συμπεράσματα για ιδιότητες σχετικές με την εκτέλεση ενός συμβολαίου.

Τα μοντέλα χαμηλού επιπέδου θεωρούνται ιδανικά καθώς αντιπροσωπεύουν την πραγματική εκτέλεση ενός έξυπνου συμβολαίου στο περιβάλλον εκτέλεσης του Ethereum (δηλαδή, το EVM). Οι τεχνικές μοντελοποίησης χαμηλού επιπέδου είναι ιδιαίτερα χρήσιμες στον καθορισμό κρίσιμων ιδιοτήτων ασφαλείας σε έξυπνα συμβόλαια και στον εντοπισμό πιθανών ευπαθειών.

Τι είναι μια τυπική προδιαγραφή;

Μια προδιαγραφή είναι απλώς μια τεχνική απαίτηση την οποία πρέπει να ικανοποιεί ένα συγκεκριμένο σύστημα. Στον προγραμματισμό, οι προδιαγραφές αντιπροσωπεύουν γενικές ιδέες σχετικά με την εκτέλεση ενός προγράμματος (δηλαδή, τι πρέπει να κάνει το πρόγραμμα).

Στο πλαίσιο των έξυπνων συμβολαίων, οι τυπικές προδιαγραφές αναφέρονται σε ιδιότητες, τυπικές περιγραφές των απαιτήσεων που πρέπει να ικανοποιεί ένα συμβόλαιο. Τέτοιες ιδιότητες περιγράφονται ως «αμετάβλητες» και αντιπροσωπεύουν λογικές δηλώσεις σχετικά με την εκτέλεση μιας σύμβασης που πρέπει να παραμένουν αληθείς υπό κάθε πιθανή περίσταση, χωρίς εξαιρέσεις.

Έτσι, μπορούμε να σκεφτούμε μια τυπική προδιαγραφή ως μια συλλογή δηλώσεων γραμμένων σε τυπική γλώσσα που περιγράφουν την προβλεπόμενη εκτέλεση μιας έξυπνης σύμβασης. Οι προδιαγραφές καλύπτουν τις ιδιότητες μιας σύμβασης και ορίζουν πώς θα πρέπει να συμπεριφέρεται η σύμβαση σε διαφορετικές συνθήκες. Ο σκοπός της τυπικής επαλήθευσης είναι να προσδιορίσει εάν ένα έξυπνο συμβόλαιο διαθέτει αυτές τις ιδιότητες (αμετάβλητες) και ότι αυτές οι ιδιότητες δεν παραβιάζονται κατά την εκτέλεση.

Οι τυπικές προδιαγραφές είναι κρίσιμες για την ανάπτυξη ασφαλών υλοποιήσεων έξυπνων συμβολαίων. Τα συμβόλαια που δεν καταφέρνουν να εφαρμόζουν τις αμετάβλητες ιδιότητες ή των οποίων οι ιδιότητες παραβιάζονται κατά την εκτέλεση τους, είναι επιρρεπή σε ευπάθειες που μπορούν να βλάψουν τη λειτουργικότητα ή να προκαλέσουν κακόβουλες εκμεταλλεύσεις.

Τύποι τυπικών προδιαγραφών για έξυπνα συμβόλαια

Οι τυπικές προδιαγραφές επιτρέπουν τον μαθηματικό συλλογισμό σχετικά με τη σωστή εκτέλεση του προγράμματος. Όπως συμβαίνει στα τυπικά μοντέλα, οι τυπικές προδιαγραφές μπορούν να καταγράψουν είτε ιδιότητες υψηλού επιπέδου, είτε τη συμπεριφορά χαμηλού επιπέδου μιας υλοποίησης συμβολαίου.

Οι τυπικές προδιαγραφές προκύπτουν χρησιμοποιώντας στοιχεία της λογικής προγραμματισμού(opens in a new tab), τα οποία επιτρέπουν τον τυπικό συλλογισμό σχετικά με τις ιδιότητες ενός προγράμματος. Μια λογική προγραμματισμού έχει τυπικούς κανόνες που εκφράζουν (σε μαθηματική γλώσσα) την αναμενόμενη συμπεριφορά ενός προγράμματος. Διάφορες λογικές προγραμματισμού χρησιμοποιούνται στη δημιουργία τυπικών προδιαγραφών, συμπεριλαμβανομένων της λογικής προσβασιμότητας(opens in a new tab), της χρονικής λογικής(opens in a new tab) και της λογικής Hoare(opens in a new tab).

Οι τυπικές προδιαγραφές για έξυπνα συμβόλαια μπορούν να ταξινομηθούν σε γενικές γραμμές είτε ως προδιαγραφές υψηλού επιπέδου είτε ως προδιαγραφές χαμηλού επιπέδου. Ανεξάρτητα από την κατηγορία στην οποία ανήκει μια προδιαγραφή, πρέπει να περιγράφει επαρκώς και χωρίς υπεκφυγές την ιδιότητα του συστήματος που αναλύεται.

Προδιαγραφές υψηλού επιπέδου

Όπως υποδηλώνει το όνομα, μια προδιαγραφή υψηλού επιπέδου (που ονομάζεται επίσης «προδιαγραφή προσανατολισμένη στο μοντέλο») περιγράφει τη συμπεριφορά υψηλού επιπέδου ενός προγράμματος. Οι προδιαγραφές υψηλού επιπέδου μοντελοποιούν ένα έξυπνο συμβόλαιο ως μια πεπερασμένη κατάσταση μηχανής(opens in a new tab) (FSM), η οποία μπορεί να μεταβεί μεταξύ καταστάσεων εκτελώντας λειτουργίες, με τη χρονική λογική να χρησιμοποιείται για τον ορισμό τυπικών ιδιοτήτων για το μοντέλο FSM.

Οι χρονικές λογικές(opens in a new tab) είναι «κανόνες για τον συλλογισμό σχετικά με προτάσεις που προσδιορίζονται ως προς το χρόνο (π.χ. «Πάντα πεινάω» ή «Τελικά θα πεινάσω»).» Όταν εφαρμόζονται στην τυπική επαλήθευση, οι χρονικές λογικές χρησιμοποιούνται για να δηλώσουν ισχυρισμούς σχετικά με τη σωστή συμπεριφορά συστημάτων που μοντελοποιούνται ως μηχανές κατάστασης. Ειδικότερα, μια χρονική λογική περιγράφει τις μελλοντικές καταστάσεις στις οποίες μπορεί να βρίσκεται ένα έξυπνο συμβόλαιο και πώς μεταβαίνει μεταξύ των καταστάσεων.

Οι προδιαγραφές υψηλού επιπέδου γενικά καταγράφουν δύο κρίσιμες χρονικές ιδιότητες για τα έξυπνα συμβόλαια: ασφάλεια και ζωντάνια. Οι ιδιότητες ασφάλειας αντιπροσωπεύουν την ιδέα ότι «τίποτα κακό δε συμβαίνει ποτέ» και συνήθως εκφράζουν αμετάβλητες καταστάσεις. Μια ιδιότητα ασφάλειας μπορεί να ορίζει γενικές απαιτήσεις λογισμικού, όπως την αποφυγή αδιεξόδου(opens in a new tab) ή να εκφράζει συγκεκριμένες ιδιότητες για συμβόλαια (π.χ. αμετάβλητα στοιχεία για τον έλεγχο πρόσβασης σε συναρτήσεις, επιτρεπτές τιμές μεταβλητών κατάστασης ή συνθήκες για μεταφορές κρυπτοπαραστατικών).

Πάρτε για παράδειγμα αυτή την απαίτηση ασφάλειας που καλύπτει τις συνθήκες για τη χρήση των transfer() ή transferFrom() σε συμβάσεις κρυπτοπαραστατικών ERC-20: «Το υπόλοιπο ενός αποστολέα δεν είναι ποτέ χαμηλότερο από το ζητούμενο ποσό κρυπτοπαραστατικών που πρόκειται να σταλεί». Αυτή η περιγραφή φυσικής γλώσσας ενός αμετάβλητου στοιχείου συμβολαίου μπορεί να μεταφραστεί σε μια επίσημη (μαθηματική) προδιαγραφή, η εγκυρότητα της οποίας μπορεί στη συνέχεια να ελεγχθεί αυστηρά.

Οι ιδιότητες ζωντάνιας διαβεβαιώνουν ότι «συμβαίνει κάτι που τελικά είναι καλό» και αφορούν την ικανότητα ενός συμβολαίου να σημειώνει πρόοδο μέσα από διαφορετικές καταστάσεις. Ένα παράδειγμα μιας ιδιότητας ζωντάνιας είναι η «ρευστότητα», που αναφέρεται στην ικανότητα ενός συμβολαίου να μεταφέρει τα υπόλοιπά του στους χρήστες κατόπιν αιτήματος. Εάν αυτή η ιδιότητα παραβιαστεί, οι χρήστες δε θα μπορούν να αποσύρουν περιουσιακά στοιχεία που αποθηκεύονται στο συμβόλαιο, όπως συνέβη με το περιστατικό του πορτοφολιού Parity(opens in a new tab).

Προδιαγραφές χαμηλού επιπέδου

Οι προδιαγραφές υψηλού επιπέδου λαμβάνουν ως σημείο εκκίνησης ένα μοντέλο πεπερασμένης κατάστασης ενός συμβολαίου και ορίζουν τις επιθυμητές ιδιότητες αυτού του μοντέλου. Αντίθετα, οι προδιαγραφές χαμηλού επιπέδου (που ονομάζονται επίσης «προδιαγραφές προσανατολισμένες στις ιδιότητες») συχνά μοντελοποιούν προγράμματα (έξυπνα συμβόλαια) ως συστήματα που αποτελούνται από μια συλλογή μαθηματικών συναρτήσεων και περιγράφουν τη σωστή συμπεριφορά τέτοιων συστημάτων.

Με απλούστερους όρους, οι προδιαγραφές χαμηλού επιπέδου αναλύουν ίχνη προγράμματος και προσπαθούν να ορίσουν ιδιότητες ενός έξυπνου συμβολαίου πάνω σε αυτά τα ίχνη. Τα ίχνη αναφέρονται σε ακολουθίες εκτελέσεων συναρτήσεων που αλλάζουν την κατάσταση ενός έξυπνου συμβολαίου. Συνεπώς, οι προδιαγραφές χαμηλού επιπέδου βοηθούν στον καθορισμό απαιτήσεων για την εσωτερική εκτέλεση ενός συμβολαίου.

Οι επίσημες προδιαγραφές χαμηλού επιπέδου μπορούν να δοθούν είτε ως ιδιότητες τύπου Hoare είτε ως αμετάβλητα στοιχεία σε διαδρομές εκτέλεσης.

Ιδιότητες τύπου Hoare

Η λογική Hoare(opens in a new tab) παρέχει ένα σύνολο τυπικών κανόνων για τον συλλογισμό σχετικά με τη σωστή λειτουργία των προγραμμάτων, συμπεριλαμβανομένων των έξυπνων συμβολαίων. Μια ιδιότητα τύπου Hoare αντιπροσωπεύεται από ένα τριπλό Hoare {P}c{Q}, όπου το c είναι ένα πρόγραμμα και τα P και Q είναι προτάσεις για την κατάσταση του c (δηλαδή, του προγράμματος), που περιγράφονται επίσημα ως προϋποθέσεις και μετα-συνθήκες, αντίστοιχα.

Μια προϋπόθεση είναι μια πρόταση που περιγράφει τις συνθήκες που απαιτούνται για τη σωστή εκτέλεση μιας συνάρτησης. Οι χρήστες που καλούν το συμβόλαιο πρέπει να ικανοποιούν αυτήν την απαίτηση. Μια μετα-συνθήκη είναι μια πρόταση που περιγράφει την κατάσταση που καθορίζει μια συνάρτηση εάν εκτελεστεί σωστά. Οι χρήστες μπορούν να αναμένουν ότι αυτή η συνθήκη θα είναι αληθής μετά την κλήση της συνάρτησης. Ένα αμετάβλητο στοιχείο στη λογική Hoare είναι μια πρόταση που διατηρείται με εκτέλεση συνάρτησης (δηλαδή, δεν αλλάζει).

Οι προδιαγραφές τύπου Hoare μπορούν να εγγυηθούν είτε μερική ορθότητα είτε ολική ορθότητα. Η υλοποίηση μιας συνάρτησης συμβολαίου είναι «μερικώς σωστή» εάν η προϋπόθεση ισχύει πριν εκτελεστεί η συνάρτηση και εάν η εκτέλεση τερματιστεί, η μετα-συνθήκη είναι επίσης αληθής. Η απόδειξη της ολικής ορθότητας αποκτάται εάν μια προϋπόθεση είναι αληθής πριν εκτελεστεί η συνάρτηση, η εκτέλεση εγγυημένα τερματίζεται και, όταν το κάνει, η μετα-συνθήκη ισχύει.

Η απόκτηση απόδειξης ολικής ορθότητας είναι δύσκολη καθώς ορισμένες εκτελέσεις ενδέχεται να καθυστερήσουν πριν τερματίσουν ή δεν διακόπτονται ποτέ. Ωστόσο, το ερώτημα εάν η εκτέλεση διακόπτεται είναι πιθανώς άκυρο, καθώς ο μηχανισμός κρατήσεων gas του Ethereum εμποδίζει τους άπειρους βρόχους προγράμματος (η εκτέλεση τερματίζει είτε με επιτυχία είτε τελειώνει λόγω σφάλματος «out-of-gas»).

Οι προδιαγραφές έξυπνων συμβολαίων που δημιουργούνται χρησιμοποιώντας τη λογική Hoare θα έχουν προϋποθέσεις, μετα-συνθήκες και αμετάβλητα στοιχεία που ορίζονται για την εκτέλεση συναρτήσεων και βρόχων σε ένα συμβόλαιο. Οι προϋποθέσεις συχνά περιλαμβάνουν τη δυνατότητα σφαλμάτων εισόδου σε μια συνάρτηση, με μετα-συνθήκες που περιγράφουν την αναμενόμενη απόκριση σε τέτοιες εισόδους (π.χ., εμφάνιση μιας συγκεκριμένης εξαίρεσης). Με αυτόν τον τρόπο, οι ιδιότητες τύπου Hoare είναι αποτελεσματικές για τη διασφάλιση της ορθότητας των υλοποιήσεων συμβολαίων.

Πολλά πλαίσια επίσημης επαλήθευσης χρησιμοποιούν προδιαγραφές τύπου Hoare για την απόδειξη της σημασιολογικής ορθότητας των συναρτήσεων. Είναι επίσης δυνατή η προσθήκη ιδιοτήτων τύπου Hoare (ως ισχυρισμοί) απευθείας στον κώδικα συμβολαίου χρησιμοποιώντας τις συναρτήσεις require και assert στη Solidity.

Οι συναρτήσεις require εκφράζουν μια προϋπόθεση ή ένα αμετάβλητο στοιχείο και χρησιμοποιούνται συχνά για την επικύρωση στοιχείων εισόδου του χρήστη, ενώ το assert καταγράφει μια μετα-συνθήκη απαραίτητη για την ασφάλεια. Για παράδειγμα, ο σωστός έλεγχος πρόσβασης για συναρτήσεις (ένα παράδειγμα ιδιότητας ασφαλείας) μπορεί να επιτευχθεί χρησιμοποιώντας το require ως έλεγχο προϋπόθεσης για την ταυτότητα του λογαριασμού κλήσης. Παρομοίως, ένα αμετάβλητο στοιχείο στις επιτρεπόμενες τιμές των μεταβλητών κατάστασης ενός συμβολαίου (π.χ. συνολικός αριθμός κρυπτοπαραστατικών σε κυκλοφορία) μπορεί να προστατευθεί από παραβίαση χρησιμοποιώντας το assert για να επιβεβαιώσει την κατάσταση του συμβολαίου μετά την εκτέλεση της συνάρτησης.

Προδιαγραφές επιπέδου ιχνών

Οι προδιαγραφές που βασίζονται στα ίχνη περιγράφουν λειτουργίες για τη μετάβαση ενός συμβολαίου μεταξύ διαφορετικών καταστάσεων και τις σχέσεις μεταξύ αυτών των λειτουργιών. Όπως εξηγήθηκε προηγουμένως, τα ίχνη είναι ακολουθίες λειτουργιών που αλλάζουν την κατάσταση ενός συμβολαίου με συγκεκριμένο τρόπο.

Αυτή η προσέγγιση βασίζεται σε ένα μοντέλο έξυπνων συμβολαίων ως συστήματα μετάβασης κατάστασης με ορισμένες προκαθορισμένες καταστάσεις (περιγράφονται από μεταβλητές κατάστασης), μαζί με ένα σύνολο προκαθορισμένων μεταβάσεων (περιγράφονται από συναρτήσεις σύμβασης). Επιπλέον, ένα γράφημα ελέγχου ροής(opens in a new tab) (CFG), το οποίο είναι μια γραφική αναπαράσταση της ροής εκτέλεσης ενός προγράμματος, χρησιμοποιείται συχνά για την περιγραφή της λειτουργικής σημασιολογίας ενός συμβολαίου. Εδώ, κάθε ίχνος αντιπροσωπεύεται ως μια διαδρομή στο γράφημα ελέγχου ροής.

Ως επί το πλείστον, οι προδιαγραφές επιπέδου ιχνών χρησιμοποιούνται για να εξάγουν συμπεράσματα για τα μοτίβα εσωτερικής εκτέλεσης στα έξυπνα συμβόλαια. Δημιουργώντας προδιαγραφές επιπέδου ιχνών, ισχυριζόμαστε τις επιτρεπόμενες διαδρομές εκτέλεσης (δηλαδή, μεταβάσεις κατάστασης) σε ένα έξυπνο συμβόλαιο. Χρησιμοποιώντας τεχνικές, όπως η συμβολική εκτέλεση, μπορούμε να επαληθεύσουμε επίσημα ότι η εκτέλεση δεν ακολουθεί ποτέ μια διαδρομή που δεν έχει οριστεί στο τυπικό μοντέλο.

Ας χρησιμοποιήσουμε ένα παράδειγμα ενός συμβολαίου DAO που έχει ορισμένες δημόσια προσβάσιμες συναρτήσεις για να περιγράψουμε τις ιδιότητες επιπέδου ιχνών. Εδώ, υποθέτουμε ότι η σύμβαση DAO επιτρέπει στους χρήστες να εκτελούν τις ακόλουθες λειτουργίες:

Κατάθεση κεφαλαίων
Ψήφιση πρότασης, μετά την κατάθεση κεφαλαίων
Λήψη επιστροφής χρημάτων εάν δεν ψηφίσουν μια πρόταση

Παραδείγματα ιδιοτήτων σε επίπεδο ιχνών θα μπορούσαν να είναι «οι χρήστες που δεν καταθέτουν κεφάλαια δεν μπορούν να ψηφίσουν μια πρόταση» ή «οι χρήστες που δεν ψηφίζουν μια πρόταση θα πρέπει πάντα να μπορούν να λάβουν επιστροφή χρημάτων». Και οι δύο ιδιότητες επιβεβαιώνουν προτιμώμενες ακολουθίες εκτέλεσης (η ψηφοφορία δεν μπορεί να συμβεί πριν από την κατάθεση κεφαλαίων και η απαίτηση επιστροφής χρημάτων δεν μπορεί να συμβεί μετά την ψηφοφορία σε μια πρόταση).

Τεχνικές για την τυπική επαλήθευση έξυπνων συμβολαίων

Έλεγχος μοντέλου

Ο έλεγχος μοντέλου είναι μια τεχνική τυπικής επαλήθευσης στην οποία ένας αλγόριθμος ελέγχει ένα επίσημο μοντέλο ενός έξυπνου συμβολαίου, έναντι της προδιαγραφής του. Στον έλεγχο μοντέλου τα έξυπνα συμβόλαια αναπαριστώνται συχνά ως συστήματα μεταβάσεων κατάστασης, ενώ οι ιδιότητες σχετικά με επιτρεπτές καταστάσεις συμβολαίων ορίζονται χρησιμοποιώντας χρονική λογική.

Ο έλεγχος μοντέλου απαιτεί τη δημιουργία μιας αφηρημένης μαθηματικής αναπαράστασης ενός συστήματος (δηλαδή, ενός συμβολαίου) και την έκφραση ιδιοτήτων αυτού του συστήματος χρησιμοποιώντας τύπους που προέρχονται από την προτασιακή λογική(opens in a new tab). Αυτό απλοποιεί την εργασία του αλγορίθμου ελέγχου μοντέλου, δηλαδή να αποδείξει ότι ένα μαθηματικό μοντέλο ικανοποιεί έναν δεδομένο λογικό τύπο.

Ο έλεγχος μοντέλου στην τυπική επαλήθευση χρησιμοποιείται κυρίως για την αξιολόγηση χρονικών ιδιοτήτων που περιγράφουν τη συμπεριφορά ενός συμβολαίου με την πάροδο του χρόνου. Οι χρονικές ιδιότητες για έξυπνα συμβόλαια περιλαμβάνουν την ασφάλεια και τη ζωντάνια, τις οποίες εξηγήσαμε προηγουμένως.

Για παράδειγμα, μια ιδιότητα ασφάλειας που σχετίζεται με τον έλεγχο πρόσβασης (π.χ., μόνο ο ιδιοκτήτης του συμβολαίου μπορεί να καλέσει selfdestruct) μπορεί να γραφτεί σε τυπική λογική. Στη συνέχεια, ο αλγόριθμος ελέγχου μοντέλου μπορεί να επαληθεύσει εάν το συμβόλαιο ικανοποιεί αυτή την τυπική προδιαγραφή.

Ο έλεγχος μοντέλου χρησιμοποιεί εξερεύνηση χώρου καταστάσεων, η οποία περιλαμβάνει τη δημιουργία όλων των πιθανών καταστάσεων ενός έξυπνου συμβολαίου και την προσπάθεια εύρεσης προσβάσιμων καταστάσεων που οδηγούν σε παραβιάσεις ιδιοτήτων. Ωστόσο, αυτό μπορεί να οδηγήσει σε έναν άπειρο αριθμό καταστάσεων (γνωστό ως «πρόβλημα έκρηξης κατάστασης»), επομένως οι ελεγκτές μοντέλων βασίζονται σε τεχνικές αφαίρεσης για να πραγματοποιήσουν την αποτελεσματική ανάλυση των έξυπνων συμβολαίων.

Απόδειξη θεωρημάτων

Η απόδειξη θεωρημάτων είναι μια μέθοδος μαθηματικού συλλογισμού σχετικά με την ορθότητα των προγραμμάτων, συμπεριλαμβανομένων των έξυπνων συμβολαίων. Αυτό περιλαμβάνει τη μετατροπή του μοντέλου του συστήματος ενός συμβολαίου και των προδιαγραφών του σε μαθηματικούς τύπους (λογικές δηλώσεις).

Ο στόχος της απόδειξης θεωρημάτων είναι να επαληθεύσει τη λογική ισοδυναμία μεταξύ αυτών των δηλώσεων. Η «λογική ισοδυναμία» (που ονομάζεται επίσης «λογική διπλή υποδοχή») είναι ένας τύπος σχέσης μεταξύ δύο δηλώσεων, έτσι ώστε η πρώτη δήλωση είναι αληθής εάν και μόνο εάν η δεύτερη δήλωση είναι αληθής.

Η απαιτούμενη σχέση (λογική ισοδυναμία) μεταξύ δηλώσεων σχετικά με το μοντέλο ενός συμβολαίου και την ιδιότητά του διατυπώνεται ως μια αποδείξιμη δήλωση (που ονομάζεται θεώρημα). Χρησιμοποιώντας ένα επίσημο σύστημα συλλογισμού, ο αυτόματος μηχανισμός απόδειξης θεωρημάτων μπορεί να επαληθεύσει το θεώρημα. Με άλλα λόγια, αυτός που αποδεικνύει ένα θεώρημα μπορεί να αποδείξει οριστικά ότι το μοντέλο ενός έξυπνου συμβολαίου ταιριάζει ακριβώς με τις προδιαγραφές του.

Ενώ ο έλεγχος μοντέλων μοντελοποιεί τα συμβόλαια ως συστήματα μετάβασης με πεπερασμένες καταστάσεις, η απόδειξη θεωρημάτων μπορεί να χειριστεί την ανάλυση συστημάτων άπειρης κατάστασης. Ωστόσο, αυτό σημαίνει ότι ένας αυτόματος τρόπος απόδειξης θεωρημάτων δεν μπορεί πάντα να γνωρίζει εάν ένα λογικό πρόβλημα μπορεί να «λάβει απόφαση» ή όχι.

Συνεπώς, απαιτείται συχνά ανθρώπινη βοήθεια για να καθοδηγήσει αυτόν που θα αποδείξει το θεώρημα στην απόδειξη της ορθότητας. Η χρήση ανθρώπινης προσπάθειας στην απόδειξη θεωρημάτων καθιστά πιο δαπανηρή τη χρήση της από τον έλεγχο μοντέλου, ο οποίος είναι πλήρως αυτοματοποιημένος.

Συμβολική εκτέλεση

Η συμβολική εκτέλεση είναι μια μέθοδος ανάλυσης ενός έξυπνου συμβολαίου με την εκτέλεση συναρτήσεων χρησιμοποιώντας συμβολικές τιμές (π.χ., x > 5) αντί για συγκεκριμένες τιμές (π.χ., x == 5). Ως τεχνική τυπικής επαλήθευσης, η συμβολική εκτέλεση χρησιμοποιείται για να εξαγάγει επίσημα συμπεράσματα σχετικά με ιδιότητες επιπέδου ιχνών, στον κώδικα ενός συμβολαίου.

Η συμβολική εκτέλεση αντιπροσωπεύει ένα ίχνος εκτέλεσης ως μαθηματικό τύπο πάνω σε συμβολικές τιμές εισόδου και ονομάζεται κατηγόρημα διαδρομής. Ένας λύτης SMT(opens in a new tab) χρησιμοποιείται για να ελέγξει εάν ένα κατηγόρημα διαδρομής είναι «ικανοποιήσιμο» (δηλαδή, υπάρχει μια τιμή που μπορεί να ικανοποιήσει τον τύπο). Εάν μια ευάλωτη διαδρομή είναι ικανοποιήσιμη, ο λύτης SMT θα δημιουργήσει μια συγκεκριμένη τιμή που ενεργοποιεί την εκτέλεση προς αυτήν τη διαδρομή.

Ας υποθέσουμε ότι μια συνάρτηση ενός έξυπνου συμβολαίου λαμβάνει ως στοιχείο εισόδου μια τιμή uint (x) και αναστρέφεται όταν το x είναι μεγαλύτερο από 5 και επίσης μικρότερο από 10. Η εύρεση μιας τιμής για το x που προκαλεί το σφάλμα χρησιμοποιώντας μια κανονική διαδικασία δοκιμής, θα απαιτούσε την εκτέλεση δεκάδων περιπτώσεων δοκιμής (ή περισσότερων) χωρίς την εγγύηση ότι θα βρεθεί πραγματικά ένα στοιχείο εισόδου που προκαλεί σφάλμα.

Αντίθετα, ένα εργαλείο συμβολικής εκτέλεσης θα εκτελέσει τη συνάρτηση με τη συμβολική τιμή: X > 5 ∧ X < 10 (δηλαδή, το x είναι μεγαλύτερο από 5 ΚΑΙ το x είναι μικρότερο από 10). Η συσχετισμένη προϋπόθεση διαδρομής x = X > 5 ∧ X < 10 θα δοθεί στη συνέχεια σε έναν λύτη SMT για επίλυση. Εάν μια συγκεκριμένη τιμή ικανοποιεί τον τύπο x = X > 5 ∧ X < 10, ο λύτης SMT θα την υπολογίσει, για παράδειγμα, ο λύτης μπορεί να παράγει το 7 ως μια τιμή για το x.

Επειδή η συμβολική εκτέλεση βασίζεται σε εισόδους σε ένα πρόγραμμα και το σύνολο των στοιχείων εισόδου για την εξερεύνηση όλων των προσβάσιμων καταστάσεων είναι δυνητικά άπειρο αλλά είναι ακόμα μια μορφή δοκιμής. Ωστόσο, όπως φαίνεται στο παράδειγμα, η συμβολική εκτέλεση είναι πιο αποτελεσματική από την κανονική δοκιμή για την εύρεση στοιχείων εισόδου που προκαλούν παραβιάσεις ιδιοτήτων.

Επιπλέον, η συμβολική εκτέλεση παράγει λιγότερα ψευδώς θετικά από άλλες τεχνικές βασισμένες σε ιδιότητες (π.χ., fuzzing) που δημιουργούν τυχαία στοιχεία εισόδου σε μια συνάρτηση. Εάν μια κατάσταση σφάλματος προκληθεί κατά τη διάρκεια της συμβολικής εκτέλεσης, τότε είναι δυνατό να δημιουργηθεί μια συγκεκριμένη τιμή που προκαλεί το σφάλμα και να αναπαραχθεί το ζήτημα.

Η συμβολική εκτέλεση μπορεί επίσης να παρέχει κάποιο βαθμό μαθηματικής απόδειξης ορθότητας. Εξετάστε το ακόλουθο παράδειγμα μιας συνάρτησης συμβολαίου με προστασία από υπέρβαση:

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;

Μια ιχνηλασία εκτέλεσης που οδηγεί σε υπέρβαση του ακέραιου, θα πρέπει να ικανοποιεί τον τύπο: z = x + y ΚΑΙ (z >= x) ΚΑΙ (z >= y) ΚΑΙ (z < x Ή z < y). Ένας τέτοιος τύπος είναι απίθανο να λυθεί, επομένως χρησιμεύει ως μαθηματική απόδειξη ότι στη συνάρτηση safe_add δε γίνεται ποτέ υπέρβαση.

Γιατί να χρησιμοποιήσουμε τυπική επαλήθευση στα έξυπνα συμβόλαια;

Η ανάγκη για αξιοπιστία

Η τυπική επαλήθευση χρησιμοποιείται για να αξιολογήσει τη σωστή λειτουργία κρίσιμων συστημάτων, των οποίων η αποτυχία μπορεί να έχει καταστροφικές συνέπειες, όπως θάνατο, τραυματισμό ή οικονομική καταστροφή. Τα έξυπνα συμβόλαια είναι εφαρμογές υψηλής αξίας που ελέγχουν τεράστιες ποσότητες αξίας και απλά λάθη στον σχεδιασμό μπορούν να οδηγήσουν σε μη αναστρέψιμες απώλειες για τους χρήστες(opens in a new tab). Η τυπική επαλήθευση ενός συμβολαίου πριν τη δημοσίευση, ωστόσο, μπορεί να αυξήσει τις εγγυήσεις ότι θα λειτουργήσει όπως αναμένεται όταν εκτελείται στην αλυσίδα συστοιχιών.

Η αξιοπιστία είναι μια ιδιαίτερα επιθυμητή ποιότητα σε οποιοδήποτε έξυπνο συμβόλαιο, ειδικά επειδή ο κώδικας που αναπτύσσεται στο εικονικό μηχάνημα του Ethereum (EVM) είναι συνήθως αμετάβλητος. Με τις αναβαθμίσεις μετά την κυκλοφορία να μην είναι εύκολα προσβάσιμες, η ανάγκη εγγύησης της αξιοπιστίας των συμβολαίων καθιστά απαραίτητη την τυπική επαλήθευση. Η τυπική επαλήθευση είναι σε θέση να εντοπίσει δύσκολα προβλήματα, όπως υποχείλιση και υπερχείλιση ακεραίων, επανεισδοχή και κακές βελτιστοποιήσεις gas, οι οποίες μπορεί να ξεφύγουν από ελεγκτές και δοκιμαστές.

Απόδειξη λειτουργικής ορθότητας

Η δοκιμή προγράμματος είναι η πιο κοινή μέθοδος απόδειξης ότι ένα έξυπνο συμβόλαιο ικανοποιεί κάποιες απαιτήσεις. Αυτό περιλαμβάνει την εκτέλεση ενός συμβολαίου με ένα δείγμα των δεδομένων που αναμένεται να χειριστεί και την ανάλυση της συμπεριφοράς του. Εάν το συμβόλαιο επιστρέφει τα αναμενόμενα αποτελέσματα για τα δεδομένα του δείγματος, τότε οι προγραμματιστές έχουν αντικειμενική απόδειξη της ορθότητάς του.

Ωστόσο, αυτή η προσέγγιση δεν μπορεί να αποδείξει τη σωστή εκτέλεση για τις τιμές εισόδου που δεν αποτελούν μέρος του δείγματος. Επομένως, η δοκιμή ενός συμβολαίου μπορεί να βοηθήσει στην ανίχνευση σφαλμάτων (δηλαδή εάν ορισμένες διαδρομές κώδικα αποτυγχάνουν να επιστρέψουν τα επιθυμητά αποτελέσματα κατά την εκτέλεση), αλλά δεν μπορεί να αποδείξει οριστικά την απουσία σφαλμάτων.

Αντίθετα, η τυπική επαλήθευση μπορεί να αποδείξει επίσημα ότι ένα έξυπνο συμβόλαιο ικανοποιεί τις απαιτήσεις για ένα άπειρο εύρος εκτελέσεων, χωρίς να εκτελέσει καθόλου το συμβόλαιο. Αυτό απαιτεί τη δημιουργία μιας τυπικής προδιαγραφής που περιγράφει με ακρίβεια τις σωστές συμπεριφορές του συμβολαίου και την ανάπτυξη ενός επίσημου (μαθηματικού) μοντέλου του συστήματος του συμβολαίου. Στη συνέχεια, μπορούμε να ακολουθήσουμε μια τυπική διαδικασία απόδειξης για να ελέγξουμε τη συνοχή μεταξύ του μοντέλου του συμβολαίου και της προδιαγραφής του.

Με την τυπική επαλήθευση, το ερώτημα της επαλήθευσης εάν η επιχειρηματική λογική ενός συμβολαίου ικανοποιεί τις απαιτήσεις, είναι μια μαθηματική πρόταση που μπορεί να αποδειχθεί ή να απορριφθεί. Αποδεικνύοντας επίσημα μια πρόταση, μπορούμε να επαληθεύσουμε έναν άπειρο αριθμό περιπτώσεων δοκιμής με ένα συγκεκριμένο αριθμό βημάτων. Με αυτόν τον τρόπο, η τυπική επαλήθευση έχει καλύτερες προοπτικές απόδειξης ότι ένα συμβόλαιο είναι λειτουργικά σωστό σε σχέση με μια προδιαγραφή.

Ιδανικοί στόχοι επαλήθευσης

Ένας στόχος επαλήθευσης περιγράφει το σύστημα που θα επαληθευτεί τυπικά. Η τυπική επαλήθευση χρησιμοποιείται καλύτερα σε «ενσωματωμένα συστήματα» (μικρά, απλά κομμάτια λογισμικού που αποτελούν μέρος ενός μεγαλύτερου συστήματος). Είναι επίσης ιδανικά για εξειδικευμένους τομείς που έχουν λίγους κανόνες, καθώς αυτό διευκολύνει την τροποποίηση εργαλείων για την επαλήθευση ιδιοτήτων συγκεκριμένου τομέα.

Τα έξυπνα συμβόλαια, τουλάχιστον σε κάποιο βαθμό, πληρούν και τις δύο απαιτήσεις. Για παράδειγμα, το μικρό μέγεθος των συμβολαίων στο Ethereum τα καθιστά κατάλληλα για τυπική επαλήθευση. Ομοίως, το EVM ακολουθεί απλούς κανόνες, γεγονός που διευκολύνει τη συγγραφή προδιαγραφών και την επαλήθευση σημασιολογικών ιδιοτήτων για προγράμματα που εκτελούνται στο EVM.

Ταχύτερος κύκλος ανάπτυξης

Οι τεχνικές τυπικής επαλήθευσης, όπως η επαλήθευση μοντέλου και η συμβολική εκτέλεση, είναι γενικά πιο αποτελεσματικές από την κανονική ανάλυση κώδικα έξυπνου συμβολαίου (που εκτελείται κατά τη διάρκεια δοκιμών ή ελέγχου). Αυτό συμβαίνει επειδή η τυπική επαλήθευση βασίζεται σε συμβολικές τιμές για να ελέγξει ισχυρισμούς («τι γίνεται αν ένας χρήστης προσπαθήσει να αποσύρει n ether;») σε αντίθεση με τις δοκιμές που χρησιμοποιούν συγκεκριμένες τιμές («τι γίνεται αν ένας χρήστης προσπαθήσει να αποσύρει 5 ether;»).

Οι συμβολικές μεταβλητές εισόδου μπορούν να καλύψουν πολλές κατηγορίες συγκεκριμένων τιμών, επομένως οι προσεγγίσεις τυπικής επαλήθευσης υπόσχονται μεγαλύτερη κάλυψη κώδικα σε μικρότερο χρονικό διάστημα. Όταν χρησιμοποιείται αποτελεσματικά, η τυπική επαλήθευση μπορεί να επιταχύνει τον κύκλο ανάπτυξης για τους προγραμματιστές.

Η τυπική επαλήθευση βελτιώνει επίσης τη διαδικασία δημιουργίας αποκεντρωμένων εφαρμογών (dapp) μειώνοντας τα δαπανηρά σφάλματα σχεδιασμού. Η αναβάθμιση των συμβολαίων (όπου είναι δυνατόν) για τη διόρθωση ευπαθειών, απαιτεί εκτεταμένη επανεγγραφή βάσεων κώδικα και περισσότερη προσπάθεια ανάπτυξης. Η τυπική επαλήθευση μπορεί να εντοπίσει πολλά σφάλματα στις υλοποιήσεις συμβάσεων που μπορεί να ξεφύγουν από τους δοκιμαστές και τους ελεγκτές και παρέχει άφθονη ευκαιρία για τη διόρθωση αυτών των προβλημάτων πριν από την ανάπτυξη ενός συμβολαίου.

Μειονεκτήματα της τυπικής επαλήθευσης

Κόστος χειρωνακτικής εργασίας

Η τυπική επαλήθευση, ειδικά η ημιαυτόματη επαλήθευση όπου ένας άνθρωπος καθοδηγεί τον επαληθευτή για να παράγει αποδείξεις ορθότητας, απαιτεί σημαντική χειρωνακτική εργασία. Επιπλέον, η δημιουργία τυπικής προδιαγραφής είναι μια σύνθετη δραστηριότητα που απαιτεί υψηλό επίπεδο δεξιοτήτων.

Αυτοί οι παράγοντες (προσπάθεια και δεξιότητα) καθιστούν την τυπική επαλήθευση πιο απαιτητική και δαπανηρή σε σύγκριση με τις συνήθεις μεθόδους αξιολόγησης της ορθότητας στα συμβόλαια, όπως οι δοκιμές και οι έλεγχοι. Ωστόσο, η πληρωμή του κόστους για έναν πλήρη έλεγχο επαλήθευσης είναι πρακτική, δεδομένου του κόστους των σφαλμάτων στις υλοποιήσεις έξυπνων συμβολαίων.

Ψευδώς αρνητικά

Η τυπική επαλήθευση μπορεί να ελέγξει μόνο εάν η εκτέλεση του έξυπνου συμβολαίου ταιριάζει με την τυπική προδιαγραφή. Ως εκ τούτου, είναι σημαντικό να βεβαιωθείτε ότι η προδιαγραφή περιγράφει σωστά τις αναμενόμενες συμπεριφορές ενός έξυπνου συμβολαίου.

Εάν οι προδιαγραφές είναι κακώς γραμμένες, οι παραβιάσεις ιδιοτήτων, οι οποίες υποδεικνύουν ευάλωτες εκτελέσεις, δεν μπορούν να εντοπιστούν από τον έλεγχο τυπικής επαλήθευσης. Σε αυτήν την περίπτωση, ένας προγραμματιστής μπορεί να υποθέσει εσφαλμένα ότι το συμβόλαιο είναι χωρίς σφάλματα.

Ζητήματα απόδοσης

Η τυπική επαλήθευση αντιμετωπίζει μια σειρά από προβλήματα απόδοσης. Για παράδειγμα, τα προβλήματα αύξησης της κατάστασης και διαδρομής που αντιμετωπίζονται κατά τον έλεγχο μοντέλου και τον συμβολικό έλεγχο, αντίστοιχα, μπορούν να επηρεάσουν τις διαδικασίες επαλήθευσης. Επίσης, τα εργαλεία τυπικής επαλήθευσης χρησιμοποιούν συχνά λύτες SMT και άλλους λύτες περιορισμών στο υποκείμενο επίπεδο τους και αυτοί οι λύτες βασίζονται σε υπολογιστικά εντατικές διαδικασίες.

Επίσης, δεν είναι πάντα δυνατό για τους επαληθευτές προγραμμάτων να προσδιορίσουν εάν μια ιδιότητα (που περιγράφεται ως λογικός τύπος) μπορεί να ικανοποιηθεί ή όχι (το πρόβλημα ικανότητας λήψης απόφασης(opens in a new tab)) επειδή ένα πρόγραμμα μπορεί να μην τερματίσει ποτέ. Ως εκ τούτου, μπορεί να είναι αδύνατο να αποδειχθούν ορισμένες ιδιότητες ενός συμβολαίου ακόμα και αν είναι καλά καθορισμένες.

Εργαλεία τυπικής επαλήθευσης για έξυπνα συμβόλαια Ethereum

Γλώσσες προδιαγραφής για τη δημιουργία τυπικών προδιαγραφών

Act: _*Το Act επιτρέπει τη συγγραφή ενημερώσεων αποθήκευσης, προϋποθέσεων/μετα-συνθηκών και αμετάβλητων στοιχείων συμβολαίων. Η σουίτα εργαλείων του διαθέτει επίσης στήριξη αποδείξεων που μπορούν να αποδείξουν πολλές ιδιότητες μέσω του Coq, των λυτών SMT ή του hevm.**

Scribble: _*Το Scribble μετατρέπει τις σημειώσεις κώδικα στη γλώσσα προδιαγραφής Scribble σε συγκεκριμένους ισχυρισμούς που ελέγχουν την προδιαγραφή.**

Τεκμηρίωση(opens in a new tab)

Dafny: _*Το Dafny είναι μια γλώσσα προγραμματισμού έτοιμη για πράξεις επαλήθευσης που βασίζεται σε σημειώσεις υψηλού επιπέδου για να συλλογιστεί και να αποδείξει την ορθότητα του κώδικα**

GitHub(opens in a new tab)

Επαληθευτές προγραμμάτων για έλεγχο σωστής λειτουργίας

Certora Prover: Το Certora Prover είναι ένα αυτόματο εργαλείο τυπικής επαλήθευσης για τον έλεγχο της ορθότητας του κώδικα σε έξυπνα συμβόλαια. Οι προδιαγραφές γράφονται σε CVL (Γλώσσα επαλήθευσης Certora), με εντοπισμό παραβιάσεων των ιδιοτήτων χρησιμοποιώντας ένα συνδυασμό στατικής ανάλυσης και επίλυσης περιορισμών.

Solidity SMTChecker: _*Το Solidity SMTChecker είναι ένας ενσωματωμένος ελεγκτής μοντέλου που βασίζεται στο SMT (Satisfiability Modulo Theories) και την επίλυση Horn. Επιβεβαιώνει εάν ο πηγαίος κώδικας ενός συμβολαίου ταιριάζει με τις προδιαγραφές κατά τη μεταγλώττιση και διενεργεί στατικούς ελέγχους παραβίασης των ιδιοτήτων ασφαλείας.**

GitHub(opens in a new tab)

solc-verify: _*Το solc-verify είναι μια επεκταμένη έκδοση του μεταγλωττιστή Solidity που μπορεί να εκτελέσει αυτόματη τυπική επαλήθευση σε κώδικα Solidity, χρησιμοποιώντας σημειώσεις και μονάδα επαλήθευσης προγράμματος.**

GitHub(opens in a new tab)

KEVM: _*Το KEVM είναι μια επίσημη συντομογραφία του εικονικού μηχανήματος του Ethereum (EVM) γραμμένη στη γλώσσα K. Το KEVM είναι εκτελέσιμο και μπορεί να αποδείξει ορισμένες προτάσεις σχετικές με τις ιδιότητες, χρησιμοποιώντας λογική προσβασιμότητας.**

Λογικά πλαίσια για απόδειξη θεωρημάτων

Isabelle: Το Isabelle/HOL είναι ένας βοηθός απόδειξης που επιτρέπει την εκτέλεση μαθηματικών τύπων σε μια τυπική γλώσσα και παρέχει εργαλεία για την απόδειξη αυτών των τύπων. Η κύρια εφαρμογή είναι η τυποποίηση μαθηματικών αποδείξεων και ειδικότερα η τυπική επαλήθευση, η οποία περιλαμβάνει την απόδειξη της ορθότητας του υλισμικού ή λογισμικού του υπολογιστή και την απόδειξη ιδιοτήτων γλωσσών και πρωτοκόλλων του υπολογιστή.

Coq: Το Coq είναι ένας διαδραστικός τρόπος απόδειξης θεωρημάτων, που σας επιτρέπει να ορίζετε προγράμματα χρησιμοποιώντας θεωρήματα και να δημιουργείτε διαδραστικά μηχανικά ελεγχόμενες αποδείξεις ορθότητας.

Εργαλεία βασισμένα σε συμβολική εκτέλεση για ανίχνευση ευάλωτων προτύπων σε έξυπνα συμβόλαια

Manticore: _Ένα εργαλείο για ανάλυση κώδικα bytecode EVM που βασίζεται σε συμβολική εκτέλεση.*

hevm: _*Το hevm είναι μια μηχανή συμβολικής εκτέλεσης και ελεγκτής ισοδυναμίας για κώδικα bytecode EVM.**

GitHub(opens in a new tab)

Mythril: Ένα εργαλείο συμβολικής εκτέλεσης για ανίχνευση ευπαθειών σε έξυπνα συμβόλαια Ethereum.