Loading...
Σειρά: Τυπική επαλήθευση · Μέρος 3 από 3 Κοινό: νέοι χρήστες. Τα μέρη 1 και 2 εισήγαγαν την τυπική επαλήθευση και το bug του Orchard· αυτό το φινάλε δείχνει τις δύο ιδέες να συναντώνται σε ένα πραγματικό σύστημα. Θα θυμηθούμε όσα χρειάζεσαι στην πορεία. Με τι θα φύγεις: μια ακριβή κατανόηση του τι ακριβώς απέδειξε το Zcash για το νέο του pool «Ironwood», πώς δομείται η απόδειξη, τι καλύπτει και τι δεν καλύπτει, πώς το παλιό pool αποσύρθηκε με ασφάλεια και γιατί αυτό δείχνει ένα νέο πρότυπο για την κατασκευή κρυπτογραφικού χρήματος.
Στο Μέρος 1 μάθαμε τι σημαίνει να αποδεικνύεις ότι ένα σύστημα είναι σωστό. Στο Μέρος 2 είδαμε ένα πραγματικό ελάττωμα που οι δοκιμές δεν εντόπισαν για τέσσερα χρόνια, έναν ανεπαρκώς περιορισμένο πολλαπλασιασμό ελλειπτικής καμπύλης που θα μπορούσε να είχε επιτρέψει απεριόριστη αόρατη παραχάραξη. Αυτό το άρθρο είναι η λύση: πώς το Zcash απάντησε όχι απλώς με ένα patch, αλλά με μια απόδειξη ελεγμένη από μηχανή ότι ολόκληρη αυτή η κατηγορία bug έχει εξαλειφθεί.
Όταν ένα bug απειλεί χρήματα, η συνήθης αντίδραση είναι να γίνει patch και να προχωρήσουμε. Το Zcash έκανε κάτι πιο φιλόδοξο. Μαζί με ένα νέο θωρακισμένο pool που ονομάζεται Ironwood, το οποίο ενεργοποιήθηκε στις 28 Ιουλίου 2026, οι μηχανικοί του δημοσίευσαν μια μαθηματική απόδειξη ελεγμένη από μηχανή, με πάνω από 2.700 θεωρήματα γραμμένα στον βοηθό αποδείξεων Lean, που τεκμηριώνει ότι το νέο pool δεν μπορεί να δημιουργήσει πλαστά νομίσματα υπό τις δηλωμένες παραδοχές του. Η απόδειξη είναι δημόσια, στο αποθετήριο ανοικτού κώδικα ironwood, και χρειάστηκε πολύ περισσότερο από έναν μήνα για να ολοκληρωθεί από τρεις ομάδες ερευνητών και κρυπτογράφων.
Αυτό έχει σημασία πέρα από το Zcash. Είναι μία από τις σαφέστερες επιδείξεις στον πραγματικό κόσμο ότι μπορείς να πάρεις ένα ενεργό χρηματοοικονομικό σύστημα, να ορίσεις με ακρίβεια τι σημαίνει «καμία παραχάραξη» και να το αποδείξεις, αντί να ελπίζεις ότι οι δοκιμές σου ήταν διεξοδικές. Μετατρέπει μια υπόσχεση σε θεώρημα.
Το Μέρος 2 κατέληξε στη διαπίστωση που το έκανε αυτό δυνατό. Θυμήσου την, επειδή πάνω της στηρίζονται όλα εδώ:
Ένα μη ανιχνεύσιμο bug παραχάραξης μπορεί να βρίσκεται μόνο στην προδιαγραφή του πρωτοκόλλου, τη μαθηματική περιγραφή όσων πρέπει να επιβάλλει το κύκλωμα. Οτιδήποτε ανιχνεύσιμο θα εμφανιζόταν στη δημόσια λογιστική. Επομένως, η απόδειξη ότι η προδιαγραφή είναι ορθή εξαλείφει μονομιάς ολόκληρη την κατηγορία κρυφών bug παραχάραξης.
Γιατί «μόνο στην προδιαγραφή»; Επειδή κάθε μπλοκ καταγράφει μόνιμα το πλήρες περιεχόμενο κάθε συναλλαγής, συμπεριλαμβανομένων των αποδείξεών της. Αν το λογισμικό δεχόταν εσφαλμένα μια κακή συναλλαγή, οποιοσδήποτε θα μπορούσε να αναπαράγει το ιστορικό με διορθωμένο λογισμικό και να το δει. Αυτά τα αποδεικτικά στοιχεία είναι μόνιμα και δημόσια. Μόνο ένα ελάττωμα στα υποκείμενα μαθηματικά μπορεί να κρυφτεί για πάντα, επειδή δεν υπάρχει «σωστή έκδοση» με την οποία να το αναπαράγεις. Αυτό είναι το ελάττωμα στο οποίο στοχεύει η τυπική επαλήθευση.
Οι δοκιμές ελέγχουν συμπεριφορά σε δειγματοληπτικές εισόδους, και το bug του Orchard κρυβόταν ακριβώς επειδή καμία δειγματοληπτική είσοδος δεν το ενεργοποίησε. Μια απόδειξη για την προδιαγραφή καλύπτει όλες τις εισόδους ταυτόχρονα, συμπεριλαμβανομένων των οριακών περιπτώσεων που κανείς δεν θα σκεφτόταν να δοκιμάσει. Αυτό είναι το μόνο είδος εγγύησης αρκετά ισχυρό ώστε να αποσύρει με βεβαιότητα ένα αόρατο ελάττωμα τεσσάρων ετών.
Η απόδειξη θεμελιώνει μία βασική ιδιότητα, χτισμένη πάνω σε μια βαθύτερη ιδιότητα.
Ακεραιότητα υπολοίπου: η κρυφή αξία που αποθηκεύεται στο θωρακισμένο pool δεν υπερβαίνει ποτέ την καθαρή δημόσια αξία που έχει εισρεύσει σε αυτό.
Αυτή είναι η ιδιότητα κατά της παραχάραξης σε απλή μορφή. Χρήματα μπορούν να εισέλθουν στο θωρακισμένο pool (δημόσια ορατά) και να εξέλθουν από αυτό (δημόσια ορατά), αλλά στο εσωτερικό, όπου τα ποσά είναι κρυφά, δεν μπορεί να δημιουργηθεί αξία από το τίποτα. Ας το κάνουμε συγκεκριμένο με ένα μικρό καθολικό (επαληθευμένη αριθμητική):
5 + 3 = 8 παράγουν εκροές αξίας 4 + 4 = 8. Η εισερχόμενη αξία ισούται με την εξερχόμενη αξία. Η ακεραιότητα υπολοίπου ισχύει. ✓8, αλλά εκροές 4 + 4 + 2 = 10. Αυτό θα δημιουργούσε 2 μονάδες από το τίποτα. Η ακεραιότητα υπολοίπου το απαγορεύει: το pool δεν μπορεί ποτέ να καταβάλει περισσότερα από όσα εισήλθαν σε αυτό. ✗Η ακεραιότητα υπολοίπου είναι η μαθηματική δήλωση ότι το δεύτερο σενάριο δεν μπορεί ποτέ να παράγει έγκυρη συναλλαγή.
Για να εγγυηθούν την ακεραιότητα υπολοίπου, οι ερευνητές έπρεπε πρώτα να αποδείξουν μια βαθύτερη και λεπτότερη ιδιότητα για το ίδιο το σύστημα αποδείξεων μηδενικής γνώσης. Η συνήθης ορθότητα (το «μόνο οι αληθείς δηλώσεις έχουν μάρτυρα» του Μέρους 2) αποδεικνύεται ότι δεν αρκεί για ένα θωρακισμένο pool, για έναν συναρπαστικό λόγο: επειδή μια κρυφή συναλλαγή μπορεί να περιέχει οτιδήποτε, σχεδόν κάθε δήλωση τεχνικά έχει κάποιον μάρτυρα. Έτσι, οι ερευνητές απέδειξαν μια ισχυρότερη ιδιότητα:
Ορθότητα γνώσης: όποιος μπορεί να παράγει έγκυρη απόδειξη συναλλαγής πρέπει όντως να κατέχει έναν έγκυρο μάρτυρα, δηλαδή πραγματικά νομίσματα, σωστά παραγμένα, στη σωστή διεύθυνση.
Το τυπικό εργαλείο γι’ αυτό είναι ένας εξαγωγέας: μια διαδικασία που, λαμβάνοντας οποιονδήποτε αποδεικνύοντα μπορεί να πείσει τον επαληθευτή, μπορεί να αντλήσει από αυτόν τον πραγματικό μάρτυρα. Αν ένας μάρτυρας μπορεί πάντα να εξαχθεί, τότε ένας πειστικός αποδεικνύων πρέπει πράγματι να είχε έναν. Στη γλώσσα του Μέρους 2, η ορθότητα γνώσης είναι η τυπική υπόσχεση ότι δεν υπάρχει κενό ορθότητας, κανένας ελλιπής περιορισμός που θα επέτρεπε σε μια ψευδή δήλωση να περάσει. Είναι ακριβώς η ιδιότητα της οποίας η απουσία ήταν το bug του Orchard. Η απόδειξη της παρουσίας της, για όλους τους πιθανούς αποδεικνύοντες, είναι αυτή που κλείνει οριστικά αυτή την πόρτα.
Η επαλήθευση ήταν μια σοβαρή ανθρώπινη προσπάθεια, όχι αποτέλεσμα με το πάτημα ενός κουμπιού:
ironwood.Για να συλλογιστεί γύρω από την ιδιότητα, το μοντέλο Lean περιγράφει ένα ολόκληρο καθολικό ως λίστα συναλλαγών, καθεμία από τις οποίες φέρει τις ενέργειές της, τη δηλωμένη δημόσια αξία της και τις υπογραφές της. Ένα κατηγόρημα που οι ερευνητές ονομάζουν ValidLedger μεταγράφει απευθείας τους κανόνες συναίνεσης του δικτύου: ο μάρτυρας κάθε ενέργειας πρέπει να ικανοποιεί τις απαιτούμενες συνθήκες, κανένας δείκτης δαπάνης (nullifier) δεν μπορεί να εμφανίζεται δύο φορές, κάθε αναφερόμενη κατάσταση δέντρου πρέπει να είναι μια κατάσταση που το σύστημα όντως έφτασε και κάθε υπογραφή πρέπει να επαληθεύεται. Τα θεωρήματα στη συνέχεια ποσοτικοποιούν πάνω από κάθε έγκυρο καθολικό. Αυτή η φράση, «κάθε έγκυρο καθολικό», είναι όλο το νόημα: όχι ένα δείγμα, αλλά όλα, ένα υπερσύνολο οποιουδήποτε καθολικού θα μπορούσε ποτέ να συνθέσει ένας πραγματικός επιτιθέμενος.
Το αποτέλεσμα ακεραιότητας υπολοίπου συναρμολογείται από διάφορα θεωρήματα επιπέδου καθολικού, καθένα από τα οποία αποδεικνύει ότι μία διαδρομή προς την παραχάραξη είναι κλειστή: ότι κάθε δαπάνη αντιστοιχεί σε πραγματική προγενέστερη εκροή, ότι η συνολική αξία διατηρείται, ότι ένα λαμβανόμενο note παραμένει δαπανήσιμο και δεν μπορεί να κλαπεί, και ότι η δαπάνη απαιτεί κατάλληλη εξουσιοδότηση. Ένα ξεχωριστό στοιχείο, η δεσμευτική υπογραφή, συνδέει τις κρυφές αξίες κάθε συναλλαγής με το δημόσιο ποσό που δηλώνει, ώστε η κρυφή και η δημόσια λογιστική να μη διαφωνούν σιωπηλά.
Μια λεπτή και ειλικρινής ερώτηση: η απόδειξη αφορά ένα μαθηματικό μοντέλο, αλλά το δίκτυο εκτελεί κώδικα Rust. Πώς γνωρίζουμε ότι ο κώδικας ταιριάζει με το μοντέλο;
Η ομάδα χάραξε ένα προσεκτικό όριο που αποκαλεί δακτυλικό αποτύπωμα του επαληθευτή. Πάνω από το όριο, οι αποδείξεις Lean συλλογίζονται για τον επαληθευτή ως ένα ακριβές μαθηματικό αντικείμενο. Κάτω από αυτό βρίσκεται η συνηθισμένη υλοποίηση Rust. Το βασικό επιχείρημα είναι το ίδιο με εκείνο του Μέρους 2:
Οποιοσδήποτε τρόπος με τον οποίο το πραγματικό λογισμικό θα μπορούσε να αποκλίνει από το αποδεδειγμένο μοντέλο θα ήταν bug υλοποίησης, και τα bug υλοποίησης μπορούν να παράγουν μόνο ανιχνεύσιμη παραχάραξη, επειδή κάθε αποδεκτή απόδειξη καταγράφεται μόνιμα και μπορεί να αναπαραχθεί με διορθωμένο λογισμικό.
Επομένως, η απόδειξη χειρίζεται τη μη ανιχνεύσιμη κατηγορία (την προδιαγραφή), και το μόνιμο δημόσιο αρχείο χειρίζεται την ανιχνεύσιμη κατηγορία (την υλοποίηση). Μεταξύ τους, δεν υπάρχει χώρος για να κρυφτεί ένα μη ανιχνεύσιμο bug παραχάραξης. Η ομάδα έκανε επίσης διασταύρωση, εκτελώντας τον πραγματικό επαληθευτή και επιβεβαιώνοντας ότι αναπαράγει ακριβώς το δακτυλικό αποτύπωμα στις καταγεγραμμένες περιπτώσεις.
Το Μέρος 1 επέμεινε ότι μια απόδειξη εγγυάται πως το σύστημα πληροί την προδιαγραφή υπό τις δηλωμένες παραδοχές, και ποτέ δεν σημαίνει «κανένα bug ποτέ». Η ομάδα του Zcash ήταν αξιοθαύμαστα ακριβής ακριβώς ως προς αυτό, και η ειλικρινής εκπαιδευτική γραφή πρέπει να είναι επίσης.
Η απόδειξη ανάγει την ασφάλεια του Ironwood σε ένα μικρό σύνολο τυπικών, σαφώς ονομασμένων παραδοχών. Ειδικότερα, η ορθότητά της βασίζεται στη δυσκολία του προβλήματος διακριτού λογαρίθμου στην ελλειπτική καμπύλη που χρησιμοποιεί το Ironwood (μια καλά μελετημένη παραδοχή, όπου η καλύτερη γνωστή επίθεση θα απαιτούσε της τάξης των 2^126 πράξεων, πολύ πέρα από κάθε εφικτό υπολογισμό), μαζί με τυπικές παραδοχές μοντελοποίησης για τη συνάρτηση hash. Αξίζει να δηλωθούν καθαρά δύο όρια:
Αντί να υπονομεύει το επίτευγμα, η ονομασία αυτών των ορίων είναι αυτό που το καθιστά αξιόπιστο. Ο ισχυρισμός είναι ακριβής: υπό τυπικές κρυπτογραφικές παραδοχές, αυτό το pool δεν μπορεί να δημιουργήσει μη ανιχνεύσιμα πλαστά νομίσματα. Αυτό είναι θεώρημα, όχι ελπίδα, και το ακριβές πεδίο του δηλώνεται ανοιχτά.
Η απόδειξη ότι το νέο pool είναι ορθό αφήνει ακόμη ένα ερώτημα: τι γίνεται με το παλιό pool Orchard, όπου το ελάττωμα υπήρχε για τέσσερα χρόνια; Δεν μπορείς να αποκαλύψεις ξανά το παρελθόν του. Μπορείς όμως να περιορίσεις το μέλλον του.
Το Zcash εισήγαγε έναν μηχανισμό που ονομάζεται turnstile. Ο κανόνας είναι απλός και ισχυρός:
Αξία μπορεί να εξέλθει από το παλιό pool μόνο έως το ποσό που αποδεδειγμένα εισήλθε σε αυτό.
Επειδή τα χρήματα που κινούνται προς και από ένα θωρακισμένο pool είναι δημόσια ορατά (μόνο η δραστηριότητα στο εσωτερικό είναι κρυφή), το turnstile επιτρέπει σε όλο το δίκτυο να ελέγχει ότι δεν εξέρχονται περισσότερα από όσα εισήλθαν ποτέ. Αν πλαστά νομίσματα είχαν δημιουργηθεί μέσα στο παλιό pool, θα έφταναν αυτό το όριο και δεν θα μπορούσαν να εξέλθουν. Και καθώς τα ειλικρινή κεφάλαια μεταναστεύουν έξω και δεν εμφανίζεται πλεόνασμα, η κοινότητα αποκτά ισχυρά δημόσια αποδεικτικά στοιχεία ότι το ελάττωμα δεν αξιοποιήθηκε ποτέ. Είναι ό,τι πλησιέστερο σε έλεγχο της προσφοράς ενός ιδιωτικού pool χωρίς να παραβιάζεται η ιδιωτικότητά του, και φέρνει την ακεραιότητα προσφοράς πιο κοντά στο διαφανές μοντέλο μιας αλυσίδας όπως το Bitcoin, διατηρώντας παράλληλα την ιδιωτικότητα του Zcash.
Το ίδιο το Ironwood επαναχρησιμοποιεί το διορθωμένο κύκλωμα αποδείξεων, ξεκινά εκ νέου με ένα κενό pool και προσθέτει προστασίες με προοπτική για το μέλλον (συμπεριλαμβανομένων προβλέψεων ώστε τα κεφάλαια να μπορούν να παραμείνουν ανακτήσιμα αν μελλοντικοί κβαντικοί υπολογιστές απειλήσουν ποτέ τη σημερινή κρυπτογραφία). Η νέα θωρακισμένη δραστηριότητα περνά τώρα μέσω του Ironwood, ενώ το παλιό pool Orchard περιορίζεται σε αναλήψεις.
Το Ironwood είναι μέρος μιας ευρύτερης μεταβολής στον τρόπο με τον οποίο κατασκευάζει το Zcash. Η προσπάθεια κλιμάκωσης επόμενης γενιάς του (μια αρχιτεκτονική που ονομάζεται Tachyon, χτισμένη πάνω σε αναδρομικές αποδείξεις και ένα σύνολο εργαλείων που ονομάζεται Ragu) αναπτύσσεται με βάση μια φιλοσοφία που μερικές φορές αποκαλείται κρυπτογραφία υψηλής διασφάλισης: η τυπική επαλήθευση ελεγμένη από μηχανή αντιμετωπίζεται όχι ως εκ των υστέρων σκέψη, αλλά ως τυπικό μέρος της διάθεσης νέων κρυπτογραφικών συστημάτων.
Η λογική είναι πειστική. Η αιχμή της κρυπτογραφίας είναι ακριβώς εκεί όπου η ανθρώπινη διαίσθηση είναι πιο αδύναμη και όπου μια λεπτή, αδοκίμαστη οριακή περίπτωση μπορεί να κρυφτεί για χρόνια, όπως έδειξε το Orchard. Η απόδειξη της προδιαγραφής είναι η μόνη τεχνική που κλιμακώνεται σε «όλες τις πιθανές εισόδους» και κλείνει αυτά τα κενά εκ κατασκευής. Η ομάδα έχει υποδείξει ότι σκοπεύει να επεκτείνει περαιτέρω αυτόν τον έλεγχο με τον χρόνο, προς την υλοποίηση και πέρα από αυτήν. Περίμενε να δεις αυτό το επίπεδο να υιοθετείται ευρύτερα, εντός και πέρα από το Zcash.
Απλοποιήσαμε για λόγους σαφήνειας. Η πραγματική ανάπτυξη στο Lean είναι πολύ λεπτομερέστερη από το περίγραμμα εδώ, με ακριβείς ορισμούς ενεργειών, δηλώσεων, commitments, nullifiers και υπογραφών· η «ακεραιότητα υπολοίπου» και η «ορθότητα γνώσης» έχουν ακριβείς τυπικούς ορισμούς που παρουσιάσαμε μόνο με λόγια· η αναγωγή στη δυσκολία του διακριτού λογαρίθμου περνά από αρκετά ενδιάμεσα μοντέλα (ένα αλγεβρικό μοντέλο του αποδεικνύοντος και ένα μοντέλο τυχαίου χρησμού του hash) που συμπυκνώσαμε σε «τυπικές παραδοχές»· και περιγράψαμε το δακτυλικό αποτύπωμα και το turnstile σε εννοιολογικό επίπεδο. Τίποτε από αυτά δεν αλλάζει την ουσιώδη ιστορία: μια προδιαγραφή «καμίας παραχάραξης», μια απόδειξη ελεγμένη από μηχανή για όλα τα έγκυρα καθολικά, μια ρητή και ειλικρινής δήλωση πεδίου και παραδοχών, και μια ασφαλής απόσυρση του ελαττωματικού pool. Για την αυθεντική παρουσίαση, συμβουλέψου τις δημοσιευμένες αναλύσεις επαλήθευσης του Project Tachyon και το αποθετήριο αποδείξεων ironwood.
| Όρος | Σημασία σε απλή γλώσσα |
|---|---|
| Ironwood | Το νέο θωρακισμένο pool του Zcash (2026), που αντικαθιστά το ελαττωματικό pool Orchard |
| Balance integrity | Το pool δεν καταβάλλει ποτέ περισσότερη αξία από όση εισήλθε δημόσια σε αυτό |
| Knowledge soundness | Μια έγκυρη απόδειξη απαιτεί ο αποδεικνύων να κατέχει έναν γνήσιο μάρτυρα |
| Extractor | Μια διαδικασία που αντλεί τον μάρτυρα από κάθε πειστικό αποδεικνύοντα |
| Lean | Ο βοηθός αποδείξεων που χρησιμοποιήθηκε για τον μηχανικό έλεγχο της επαλήθευσης |
| ValidLedger | Το τυπικό μοντέλο των κανόνων συναίνεσης πάνω στο οποίο συλλογίζονται τα θεωρήματα |
| Fingerprint | Το όριο μεταξύ των αποδεδειγμένων μαθηματικών και του λογισμικού Rust που εκτελείται |
| Under stated assumptions | Η απόδειξη ισχύει εφόσον ισχύουν οι κατονομασμένες κρυπτογραφικές παραδοχές |
| Turnstile | Ένας κανόνας που περιορίζει τις εξόδους ενός pool στις επαληθεύσιμες καταθέσεις του |
Σημαίνει η απόδειξη ότι το Ironwood δεν έχει bug; Όχι, και δεν το ισχυρίζεται. Αποδεικνύει μία ακριβή ιδιότητα, την ακεραιότητα υπολοίπου, υπό δηλωμένες παραδοχές. Αυτό αποκλείει τη μη ανιχνεύσιμη παραχάραξη, όχι κάθε πιθανό bug.
Εγγυάται η απόδειξη ότι οι συναλλαγές μου είναι ιδιωτικές; Όχι. Η επαλήθευση καλύπτει την ορθότητα της προσφοράς (όχι πλαστό χρήμα), όχι τις ξεχωριστές εγγυήσεις ιδιωτικότητας του pool. Αυτές τεκμηριώνονται διαφορετικά.
Γιατί να εμπιστευτώ μια απόδειξη γραμμένη από ανθρώπους (και AI); Επειδή ελέγχεται από μηχανή. Ο βοηθός αποδείξεων Lean επαληθεύει μηχανικά κάθε βήμα, επομένως η εμπιστοσύνη βασίζεται στην προδιαγραφή και στις κατονομασμένες παραδοχές, όχι στην προσοχή οποιουδήποτε ανθρώπου ή AI σε κάθε βήμα.
Τι συμβαίνει με νομίσματα που παραμένουν στο παλιό pool Orchard; Μπορούν να αναληφθούν, αλλά μόνο έως το ποσό που αποδεδειγμένα εισήλθε, όπως επιβάλλεται από το turnstile. Αυτό προστατεύει τόσο την ακεραιότητα της προσφοράς όσο και βοηθά να αποδειχθεί ότι το παλιό ελάττωμα δεν αξιοποιήθηκε ποτέ.
Είναι αυτό το τέλος της ιστορίας; Είναι ένα ορόσημο, όχι η γραμμή τερματισμού. Η μελλοντική αρχιτεκτονική του Zcash (Tachyon, με το σύνολο εργαλείων Ragu) κατασκευάζεται με την τυπική επαλήθευση ως τυπική πρακτική, επεκτείνοντας περαιτέρω αυτή την προσέγγιση.
Κάποιος ισχυρίζεται: «Εφόσον το Ironwood είναι τυπικά επαληθευμένο, είναι πλέον αδύνατο να πάει ποτέ κάτι στραβά με το Zcash.» Χρησιμοποιώντας ιδέες και από τα τρία μέρη, δώσε δύο διακριτούς λόγους για τους οποίους αυτός ο ισχυρισμός είναι υπερβολικός. (Απάντηση παρακάτω.)
Πρώτον, η απόδειξη καλύπτει μια συγκεκριμένη ιδιότητα (την ακεραιότητα υπολοίπου) υπό δηλωμένες παραδοχές (τη δυσκολία του διακριτού λογαρίθμου και τυπική μοντελοποίηση hash). Αν μια κρυπτογραφική παραδοχή παραβιαζόταν, ή αν προέκυπτε πρόβλημα خارج από όσα προσδιορίστηκαν (για παράδειγμα στην ιδιωτικότητα, στο λογισμικό πορτοφολιού ή σε κάποιο μη αποδεδειγμένο στοιχείο), η απόδειξη δεν λέει τίποτε γι’ αυτό. Δεύτερον, η τυπική επαλήθευση εγγυάται ότι το σύστημα πληροί την προδιαγραφή που γράφτηκε· αν αυτή η προδιαγραφή δεν κατάφερνε να αποτυπώσει κάποια πραγματική απαίτηση, η απόδειξη θα πιστοποιούσε πιστά το λάθος πράγμα. Και τα δύο σημεία επαναδιατυπώνουν την επιφύλαξη του Μέρους 1: μια απόδειξη είναι ακριβής και οριοθετημένη, ισχυρή ακριβώς επειδή το πεδίο της είναι ειλικρινές, όχι μια γενική εγγύηση ότι τίποτε δεν μπορεί ποτέ να πάει στραβά.
Σε τρία μέρη μετακινηθήκαμε από μια γενική ιδέα σε μια ενεργή εφαρμογή: τι σημαίνει να αποδεικνύεις ότι το λογισμικό είναι σωστό αντί να το δοκιμάζεις (Μέρος 1), πώς ένα πραγματικό ανεπαρκώς περιορισμένο κύκλωμα θα μπορούσε να είχε δημιουργήσει αόρατο χρήμα (Μέρος 2), και πώς μια απόδειξη ακεραιότητας υπολοίπου ελεγμένη από μηχανή απέσυρε οριστικά αυτή την κατηγορία bug (Μέρος 3). Το κοινό νήμα είναι μία ειλικρινής υπόσχεση: όχι «κανένα bug ποτέ», αλλά «αυτή η ακριβής ιδιότητα ισχύει σε κάθε περίπτωση, υπό δηλωμένες παραδοχές». Για χρήματα που κρύβουν τα ίδια τους τα ποσά, αυτή είναι ακριβώς η υπόσχεση που αξίζει να αποδειχθεί.
Μέρος της σειράς Τυπική επαλήθευση για ZecHub.
| High-assurance cryptography |
| Κατασκευή κρυπτογραφίας με την τυπική επαλήθευση ως τυπικό βήμα |