Loading...
Σειρά: Σειρά τυπικής επαλήθευσης · Μέρος 2 από 3 Κοινό: Νέοι χρήστες. Το Μέρος 1 παρουσίασε την τυπική επαλήθευση· εδώ συναντάμε το πραγματικό σφάλμα που την κατέστησε επείγουσα. Όλα όσα χρειάζεσαι εξηγούνται από την αρχή. Τι θα αποκομίσεις: Μία διαισθητική αλλά ακριβή εικόνα για το πώς ένα κρυπτογραφικό σύστημα αποδείξεων μπορεί να περιέχει ένα κενό ορθότητας, τι ακριβώς ήταν το σφάλμα «Orchard» του Zcash το 2026, γιατί αυτή η κατηγορία σφάλματος μπορεί να παραμένει κρυμμένη επί χρόνια και γιατί έχει συμβεί ξανά στο παρελθόν.
Στο Μέρος 1 είπαμε ότι οι δοκιμές μπορούν να δείξουν την παρουσία σφαλμάτων, αλλά ποτέ την απουσία τους, και ότι τα πιο επικίνδυνα σφάλματα βρίσκονται στην προδιαγραφή ενός συστήματος, στα υποκείμενα μαθηματικά του. Αυτό το άρθρο είναι η μελέτη περίπτωσης. Το 2026 βρέθηκε ένα ελάττωμα στο θωρακισμένο pool Orchard του Zcash, το οποίο θα μπορούσε να είχε επιτρέψει σε έναν επιτιθέμενο να δημιουργήσει αόρατα απεριόριστα πλαστά χρήματα. Είχε επιβιώσει τέσσερα χρόνια και επανειλημμένους ελέγχους. Η κατανόησή του, καθώς και των προδρόμων του, είναι το σαφέστερο δυνατό κίνητρο για την απόδειξη της ορθότητας των συστημάτων.
Το Zcash είναι ένα κρυπτονόμισμα με ιδιωτική λειτουργία. Στο θωρακισμένο pool του, τα ποσά, οι αποστολείς και οι παραλήπτες των συναλλαγών είναι κρυμμένοι. Αυτή η ιδιωτικότητα δημιουργείται με αποδείξεις μηδενικής γνώσης: κρυπτογραφικές αποδείξεις ότι μία συναλλαγή τηρεί όλους τους κανόνες, χωρίς να αποκαλύπτει το περιεχόμενό της.
Αυτός ο σχεδιασμός έχει δύο όψεις. Σε ένα διαφανές καθολικό όπως του Bitcoin, αν κάποιος δημιουργούσε νομίσματα από το τίποτα, οι διογκωμένοι αριθμοί θα ήταν ορατοί σε όλους και το δίκτυο θα μπορούσε να το εντοπίσει και να το αναστρέψει. Σε ένα θωρακισμένο pool, οι αριθμοί είναι κρυμμένοι από τον σχεδιασμό. Επομένως, αν το ίδιο το σύστημα αποδείξεων είχε ένα ελάττωμα που επέτρεπε σε μία μη έγκυρη συναλλαγή να φαίνεται έγκυρη, η παραχάραξη θα ήταν μη ανιχνεύσιμη. Δεν θα μπορούσες να την εντοπίσεις εξετάζοντας το καθολικό, επειδή το καθολικό είναι σκόπιμα αδιαφανές.
Αυτός είναι ακριβώς ο κίνδυνος που υλοποιήθηκε στο Orchard. Για να τον κατανοήσουμε, πρέπει να δούμε τι ελέγχει πραγματικά μία απόδειξη μηδενικής γνώσης.
Φαντάσου έναν συνοριακό υπάλληλο που πρέπει να εγκρίνει ταξιδιώτες χωρίς να βλέπει απευθείας τα έγγραφά τους. Αντί γι’ αυτό, κάθε ταξιδιώτης συμπληρώνει μία λίστα ελέγχου, και ο υπάλληλος εγκρίνει όποιον έχει επισημάνει πλήρως τη λίστα του. Η λίστα έχει σχεδιαστεί έτσι ώστε μόνο ένας νόμιμος ταξιδιώτης να μπορεί να επισημάνει κάθε πεδίο.
Τώρα, ας υποθέσουμε ότι από τη λίστα λείπει ένα κρίσιμο πεδίο, για παράδειγμα «το διαβατήριο δεν έχει λήξει». Σχεδόν όλοι εξακολουθούν να τη συμπληρώνουν ειλικρινά και τίποτα δεν φαίνεται λάθος. Όμως, ένα άτομο με ληγμένο διαβατήριο μπορεί επίσης να επισημάνει κάθε εναπομείναν πεδίο και να περάσει. Το σύστημα φαίνεται εντάξει στην καθημερινή χρήση. Το κενό έχει σημασία μόνο για κάποιον που το αναζητά.
Μία απόδειξη μηδενικής γνώσης λειτουργεί όπως αυτή η λίστα ελέγχου. Δεν αποκαλύπτει τις ιδιωτικές λεπτομέρειες· ελέγχει ότι αυτές ικανοποιούν ένα σταθερό σύνολο συνθηκών. Και αν μία αναγκαία συνθήκη παραλειφθεί κατά λάθος, τότε ορισμένες μη έγκυρες είσοδοι μπορούν επίσης να περάσουν, ενώ όλα συνεχίζουν να φαίνονται φυσιολογικά.
Ας κάνουμε ακριβή τη «λίστα συνθηκών», επειδή ακριβώς εκεί βρισκόταν το σφάλμα.
Στο υπόβαθρο, η δήλωση «αυτή η συναλλαγή είναι έγκυρη» κωδικοποιείται ως ένα κύκλωμα: μία σταθερή συλλογή αριθμητικών συνθηκών, που ονομάζονται περιορισμοί, γραμμένες ως εξισώσεις πάνω σε αριθμούς. Για να δημιουργήσει μία έγκυρη απόδειξη, ο αποδεικνύων πρέπει να παρέχει μυστικές τιμές (τον μάρτυρα) που ικανοποιούν κάθε περιορισμό. Η απόδειξη πείθει έναν επαληθευτή ότι υπάρχει τέτοιος μάρτυρας, χωρίς να τον αποκαλύπτει.
Η ιδιότητα που χρειαζόμαστε από αυτό το σύστημα έχει όνομα:
Ορθότητα: Πρέπει να είναι αδύνατο να παραχθεί έγκυρη απόδειξη για μία ψευδή δήλωση. Μόνο οι αληθείς δηλώσεις πρέπει να έχουν μάρτυρες που ικανοποιούν όλους τους περιορισμούς.
Η ορθότητα είναι η εγγύηση κατά της παραχάραξης. Αν η ορθότητα ισχύει, μία έγκυρη απόδειξη σημαίνει πραγματικά ότι πραγματοποιήθηκε μία αληθινή, συμβατή με τους κανόνες συναλλαγή. Αν η ορθότητα έχει κενό, μία έγκυρη απόδειξη μπορεί να μη σημαίνει απολύτως τίποτα.
Οι περιορισμοί συχνά πρέπει να επιβάλλουν ότι μία τιμή είναι απλή. Ένα συνηθισμένο παράδειγμα: να επιβληθεί ότι η τιμή b είναι ένα μόνο bit, είτε 0 είτε 1. Ο τυπικός τρόπος να γίνει αυτό είναι ένας περιορισμός:
b × (b − 1) = 0
Γιατί λειτουργεί; Ένα γινόμενο είναι μηδέν μόνο όταν ένας από τους παράγοντές του είναι μηδέν. Επομένως, το b × (b − 1) = 0 επιβάλλει b = 0 ή b = 1, και τίποτα άλλο. Ελέγχοντας κάθε τιμή από το 0 έως το 16 (σε αριθμητική που επανέρχεται στο 17), οι μόνες τιμές που το ικανοποιούν είναι ακριβώς οι 0 και 1. ✓
Τώρα φαντάσου ότι αυτή η γραμμή παραλείπεται κατά λάθος από το κύκλωμα. Ξαφνικά το b δεν περιορίζεται. Ένας ανέντιμος αποδεικνύων μπορεί να ορίσει το b σε 5, ή 9, ή οτιδήποτε άλλο, και να εξακολουθεί να ικανοποιεί τους υπόλοιπους περιορισμούς. Αυτή η μία ελλιπής γραμμή είναι ένα κενό ορθότητας: ψευδείς δηλώσεις έχουν πλέον ικανοποιητικούς μάρτυρες.
Αυτό δεν είναι υποθετικό. Ένας ελλιπής λογικός περιορισμός ακριβώς αυτού του είδους βρέθηκε στον πρώτο θωρακισμένο σχεδιασμό του Zcash, το Sprout, κατά την ανάπτυξη και διορθώθηκε πριν από την κυκλοφορία. Η ανεπαρκής επιβολή περιορισμών είναι ένα από τα συνηθέστερα και πιο επικίνδυνα λάθη στην κατασκευή αυτών των κυκλωμάτων.
Αυτή είναι ολόκληρη η μορφή του σφάλματος Orchard, σε μικρή κλίμακα. Τώρα ας δούμε το πραγματικό πρόβλημα.
Οι θωρακισμένες αποδείξεις του Zcash βασίζονται σε ελλειπτικές καμπύλες, μαθηματικά αντικείμενα των οποίων τα σημεία μπορούν να συνδυαστούν και να «πολλαπλασιαστούν» με αριθμούς, λειτουργίες που το κύκλωμα πρέπει να επιβάλλει με περιορισμούς. Το κύκλωμα περιέχει μηχανισμούς που εκτελούν πολλαπλασιασμό ελλειπτικής καμπύλης και ελέγχουν ότι αυτός έγινε σωστά.
Σύμφωνα με τη δημοσιοποίηση από το Shielded Labs και τον ερευνητή Taylor Hornby, το ελάττωμα Orchard ήταν ακριβώς το εξής:
Ένα ανεπαρκώς περιορισμένο στοιχείο του κυκλώματος Orchard κατέστησε δυνατό να εισάγονται αυθαίρετες ψευδείς είσοδοι σε έναν πολλαπλασιασμό ελλειπτικής καμπύλης και ο έλεγχος του πολλαπλασιασμού να εξακολουθεί να περνά.
Με απλά λόγια, από τη λίστα ελέγχου του κυκλώματος έλειπαν τα πεδία που θα έπρεπε να είχαν καθορίσει αυτόν τον πολλαπλασιασμό. Εξαιτίας του κενού, ένας επιτιθέμενος με επαρκή εξειδίκευση θα μπορούσε να κατασκευάσει μία απόδειξη συναλλαγής που το σύστημα θα αποδεχόταν, παρότι η συναλλαγή δημιουργούσε αξία από το τίποτα. Αυτό είναι παραχάραξη, και επειδή τα ποσά στο θωρακισμένο pool είναι κρυμμένα, θα ήταν μη ανιχνεύσιμη από το καθολικό. Η ομάδα του Tachyon περιέγραψε αργότερα το ίδιο ελάττωμα, στο επίπεδο του κώδικα, ως ελλιπείς γραμμές στο κύκλωμα που αλλοίωναν αθόρυβα τις υποκείμενες εξισώσεις.
Οι παραλληλισμοί με την ιστορία της λίστας ελέγχου είναι ακριβείς:
| Ιστορία λίστας ελέγχου | Το σφάλμα Orchard |
|---|---|
| Ένα ελλιπές πεδίο «το διαβατήριο δεν έχει λήξει» | Ένας ελλιπής περιορισμός σε έναν πολλαπλασιασμό ελλειπτικής καμπύλης |
| Ένας ταξιδιώτης με ληγμένο διαβατήριο περνά ούτως ή άλλως | Αυθαίρετες ψευδείς είσοδοι περνούν τον έλεγχο πολλαπλασιασμού |
| Όλοι οι υπόλοιποι δεν επηρεάζονται, οπότε τίποτα δεν φαίνεται λάθος | Οι κανονικές συναλλαγές λειτουργούσαν τέλεια, κρύβοντας το ελάττωμα |
| Μόνο κάποιος που το αναζητά βρίσκει το κενό | Χρειάστηκε ένας ειδικός που διερευνούσε σκόπιμα τα μαθηματικά του κυκλώματος |
Για να είναι σαφές πόσο σοβαρό ήταν αυτό: ο ερευνητής, με βοήθεια AI, έγραψε ένα πλήρες λειτουργικό exploit και επιβεβαίωσε σε ένα τοπικό δοκιμαστικό δίκτυο ότι παρήγαγε απεριόριστα, μη ανιχνεύσιμα πλαστά νομίσματα. Αυτό ήταν ένα πραγματικό και εκμεταλλεύσιμο ελάττωμα, όχι μία θεωρητική ανησυχία.
Το σφάλμα υπήρχε στο Orchard από την ενεργοποίησή του τον Μάιο του 2022 έως την επείγουσα διόρθωση τον Ιούνιο του 2026, περνώντας από επανειλημμένους επαγγελματικούς ελέγχους από μερικούς από τους καλύτερους κρυπτογράφους του κόσμου. Πώς;
Επειδή, όπως προειδοποίησε το Μέρος 1, οι δοκιμές δειγματοληπτούν περιπτώσεις και αυτό το ελάττωμα υπήρχε σε μία περίπτωση που κανείς δεν δειγματοληπτούσε. Οι συνηθισμένες συναλλαγές δεν ενεργοποιούσαν ποτέ τον ελλιπή περιορισμό, οπότε κάθε δοκιμή περνούσε και κάθε ημέρα κανονικής λειτουργίας φαινόταν άψογη. Το ελάττωμα ήταν προσβάσιμο μόνο με τη σκόπιμη κατασκευή ενός ασυνήθιστου μάρτυρα, στοχευμένου ακριβώς στο κενό. Τελικά βρέθηκε όχι με την εκτέλεση δοκιμών, αλλά με συλλογισμό πάνω στα μαθηματικά του κυκλώματος.
Η ίδια η ανακάλυψη είναι ένδειξη για το πού κατευθύνεται η ασφάλεια. Τον Απρίλιο του 2026, το Shielded Labs ανέθεσε στον ερευνητή ασφάλειας Taylor Hornby να αναζητήσει ειδικά ακριβώς αυτό το είδος ελαττώματος. Λίγο μετά την κυκλοφορία ενός νέου frontier μοντέλου AI (του Claude Opus 4.8 της Anthropic) στα τέλη Μαΐου του 2026, ο Hornby το χρησιμοποίησε, μαζί με ένα προσαρμοσμένο περιβάλλον ανάλυσης και παραδοσιακές μεθόδους, σε έναν στοχευμένο έλεγχο του κυκλώματος Orchard. Στις 29 Μαΐου 2026, ο έλεγχος βρήκε την ευπάθεια.
Δύο νηφάλια στοιχεία από τη δημοσιοποίηση αξίζει να αναφερθούν ξεκάθαρα:
Το σφάλμα Orchard ανήκει σε μία επαναλαμβανόμενη οικογένεια, και η κατανόηση αυτής της οικογένειας είναι που κάνει την τυπική επαλήθευση να φαίνεται όχι προαιρετική αλλά αναπόφευκτη. Ένα ελάττωμα παραχάραξης ανάγεται πάντα σε μία από τρεις πηγές (η ταξινόμηση από το Μέρος 1): την προδιαγραφή (τα ίδια τα μαθηματικά), την υλοποίηση (κώδικας που δεν ακολουθεί τα σωστά μαθηματικά), ή μία διαψευσμένη υπόθεση. Και, κρίσιμα:
Ένα σφάλμα παραχάραξης είναι μη ανιχνεύσιμο μόνο αν βρίσκεται στην προδιαγραφή. Τα σφάλματα υλοποίησης αφήνουν μόνιμα δημόσια στοιχεία, επειδή κάθε μπλοκ καταγράφει το πλήρες περιεχόμενο κάθε συναλλαγής, επομένως η επανάληψη του ιστορικού μέσω διορθωμένου λογισμικού θα αποκάλυπτε κάθε συναλλαγή που ο ελαττωματικός κώδικας αποδέχθηκε εσφαλμένα.
Η ιστορία του ίδιου του Zcash δείχνει το μοτίβο:
| Σφάλμα (έτος) | Πηγή | Ανιχνεύσιμο; |
|---|---|---|
| Ελάττωμα commitment Zerocash (2016, πριν από την κυκλοφορία) | Προδιαγραφή (ένα περικομμένο hash παραβίαζε μία ιδιότητα δέσμευσης) | Μη ανιχνεύσιμο |
| Ελάττωμα ορθότητας trusted setup (2018) | Προδιαγραφή (ένα λάθος στο υποκείμενο paper zk-SNARK) | Μη ανιχνεύσιμο |
| Σύγκρουση ερωτήματος συστήματος αποδείξεων (2025) | Προδιαγραφή (ένας ελλιπής έλεγχος στο σύστημα αποδείξεων) | Ανιχνεύσιμο |
| Σφάλμα επαλήθευσης υποομάδας Curve (2016) | Υλοποίηση (ένας ελλιπής έλεγχος υποομάδας) | Ανιχνεύσιμο |
| Ανεπαρκώς περιορισμένος πολλαπλασιασμός Orchard (2026) | Προδιαγραφή (το κύκλωμα) | Μη ανιχνεύσιμο |
Η κοινή γραμμή είναι έντονη: τα ελαττώματα που θα μπορούσαν να παραμείνουν κρυμμένα για πάντα είναι εκείνα στα μαθηματικά. Αυτή είναι ακριβώς η κατηγορία που μία ελεγχόμενη από μηχανή απόδειξη της προδιαγραφής μπορεί να εξαλείψει, για όλες τις περιπτώσεις ταυτόχρονα. Οι δοκιμές και οι έλεγχοι δειγματοληπτούν· μόνο η απόδειξη των μαθηματικών καλύπτει κάθε είσοδο.
Οι προγραμματιστές του Zcash κινήθηκαν γρήγορα και σταδιακά:
Αυτό το δεύτερο βήμα είναι όπου η τυπική επαλήθευση εισέρχεται στην ιστορία και αποτελεί το θέμα του Μέρους 3. Η συνειδητοποίηση πάνω στην οποία ενήργησε η ομάδα αξίζει μία προεπισκόπηση, επειδή συνδέει ολόκληρη αυτή τη σειρά:
Ένα μη ανιχνεύσιμο ελάττωμα παραχάραξης μπορεί να υπάρχει μόνο στην προδιαγραφή του πρωτοκόλλου. Επομένως, αν μπορείς να αποδείξεις ότι η προδιαγραφή αποκλείει την παραχάραξη, εξαλείφεις ολόκληρη την κατηγορία σφάλματος που έμεινε κρυμμένη εδώ επί τέσσερα χρόνια.
Αυτή είναι ακριβώς η ιδέα του πρώτου πυλώνα από το Μέρος 1: επαλήθευσε την προδιαγραφή και κλείνεις το κενό που οι δοκιμές δεν θα μπορούσαν ποτέ να κλείσουν.
Απλοποιήσαμε σκόπιμα. Το πραγματικό κύκλωμα περιλαμβάνει εκατοντάδες περιοχές και πολλές χιλιάδες περιορισμούς, και το πραγματικό ελάττωμα είναι τεχνικά πιο περίπλοκο από έναν μόνο ελλιπή έλεγχο bit· χρησιμοποιήσαμε τον έλεγχο bit επειδή δείχνει ακριβώς τη μορφή ενός ανεπαρκώς περιορισμένου κυκλώματος και επειδή αυτό το ακριβές λάθος είναι πραγματικό στην ιστορία του Zcash. Το ακριβές ελάττωμα Orchard ήταν ένας ανεπαρκώς περιορισμένος πολλαπλασιασμός ελλειπτικής καμπύλης, όπως αναφέρεται στην επίσημη δημοσιοποίηση. Επίσης συμπτύξαμε το χρονοδιάγραμμα δημοσιοποίησης και αποκατάστασης. Για την έγκυρη τεχνική περιγραφή, συμβουλέψου τη δημοσιοποίηση Shielded Labs και τα κείμενα του Project Tachyon.
b(b−1)=0 επιβάλλει στο b να είναι 0 ή 1· αν το αφαιρέσεις, το b μπορεί να είναι οτιδήποτε. Αυτή η ακριβής κατηγορία σφάλματος είναι πραγματική στην ιστορία του Zcash.)| Όρος | Σημασία με απλά λόγια |
|---|---|
| Shielded pool | Η ιδιωτική λειτουργία του Zcash, όπου τα ποσά και τα μέρη είναι κρυμμένα |
| Zero-knowledge proof | Μία απόδειξη ότι μία κρυφή δήλωση είναι έγκυρη, χωρίς να αποκαλύπτει τίποτε άλλο |
| Circuit | Το σταθερό σύνολο αριθμητικών συνθηκών που πρέπει να ικανοποιεί μία έγκυρη συναλλαγή |
| Constraint | Μία συνθήκη (εξίσωση) μέσα στο κύκλωμα |
| Witness | Οι μυστικές τιμές που ικανοποιούν τους περιορισμούς |
| Soundness | Η εγγύηση ότι μόνο αληθείς δηλώσεις μπορούν να παράγουν έγκυρη απόδειξη |
| Soundness gap | Ένας ελλιπής περιορισμός που επιτρέπει να περάσουν ψευδείς δηλώσεις |
| Under-constrained | Ένα κύκλωμα από το οποίο λείπει μία συνθήκη που χρειαζόταν, η ρίζα του σφάλματος Orchard |
| Detectable / undetectable | Το κατά πόσο η εκμετάλλευση θα άφηνε στοιχεία στο δημόσιο καθολικό |
Δημιουργήθηκε πράγματι πλαστό Zcash; Δεν βρέθηκαν στοιχεία εκμετάλλευσης και η ομάδα τη θεωρεί απίθανη. Όμως, επειδή το ελάττωμα θα ήταν μη ανιχνεύσιμο από το καθολικό, το καθολικό μόνο του δεν μπορεί να αποδείξει πλήρως ότι δεν συνέβη ποτέ, γι’ αυτό και η απόκριση ήταν τόσο διεξοδική.
Γιατί η απόκρυψη ποσών κάνει ένα σφάλμα χειρότερο; Σε μία διαφανή αλυσίδα, τα δημιουργημένα νομίσματα είναι ορατά και μπορούν να εντοπιστούν και να αναστραφούν. Όταν τα ποσά κρύβονται για ιδιωτικότητα, ένα σφάλμα παραχάραξης δεν παράγει καμία ορατή ανωμαλία, επομένως μπορεί να παραμένει αθέατο.
Γιατί δεν το εντόπισαν χρόνια ελέγχων; Οι έλεγχοι και οι δοκιμές εξετάζουν σε μεγάλο βαθμό συμπεριφορά σε ρεαλιστικές περιπτώσεις. Αυτό το ελάττωμα εμφανιζόταν μόνο με μία σκόπιμα κατασκευασμένη, ασυνήθιστη είσοδο, στοχευμένη σε μία μαθηματική οριακή περίπτωση, την οποία ο συνήθης έλεγχος δεν ενεργοποιούσε. Βρέθηκε με στοχευμένο συλλογισμό πάνω στο κύκλωμα, όχι με δοκιμές.
Αρκεί πράγματι ένας ελλιπής περιορισμός; Ναι. Ένα σύστημα αποδείξεων είναι τόσο ισχυρό όσο το πλήρες σύνολο περιορισμών του. Η παράλειψη μίας αναγκαίας συνθήκης αρκεί για να επιτρέψει τη διέλευση μη έγκυρων δηλώσεων.
Ποιος ήταν ο ρόλος του AI; Ένας ερευνητής χρησιμοποίησε ένα frontier μοντέλο AI μαζί με ένα προσαρμοσμένο περιβάλλον και παραδοσιακές μεθόδους για να ελέγξει τα μαθηματικά του κυκλώματος και να βρει το ελάττωμα. Το AI χρησιμοποιείται όλο και περισσότερο και στις δύο πλευρές της ασφάλειας, κάτι που αποτελεί μέρος του λόγου για τον οποίο η απόδειξη της ορθότητας των συστημάτων έχει πλέον τόσο μεγάλη σημασία.
Υπόθεσε ότι μία θωρακισμένη συναλλαγή υποτίθεται ότι αποδεικνύει πως «τα χρήματα που εισέρχονται ισούνται με τα χρήματα που εξέρχονται», αλλά το κύκλωμα ξεχνά να περιορίσει μία τιμή εξόδου. Τι θα μπορούσε να κάνει ένας ανέντιμος αποδεικνύων και γιατί το δημόσιο καθολικό θα φαινόταν εντελώς φυσιολογικό; (Απάντηση παρακάτω.)
Με αυτή την έξοδο μη περιορισμένη, ο αποδεικνύων θα μπορούσε να την ορίσει μεγαλύτερη από όση επιτρέπουν οι πραγματικές εισροές, δημιουργώντας αξία από το τίποτα, δηλαδή ένα πλαστό ποσό. Η απόδειξη θα εξακολουθούσε να επαληθεύεται, επειδή ο ελλιπής περιορισμός είναι το μόνο στοιχείο που θα είχε εντοπίσει την ανισορροπία. Και επειδή το θωρακισμένο pool κρύβει τα ποσά, το καθολικό δείχνει μόνο ότι «πραγματοποιήθηκε μία έγκυρη συναλλαγή», χωρίς ορατή ανισορροπία που να προκαλεί συναγερμό. Η πλαστογραφία είναι πραγματική αλλά αόρατη, και αυτός είναι ακριβώς ο λόγος που η ορθότητα του κυκλώματος έχει τόσο μεγάλη σημασία και πρέπει να αποδεικνύεται αντί να ελέγχεται με δοκιμές.
Μέρος 3 · Ironwood: Η διόρθωση δεν ήταν απλώς ένα patch. Οι μηχανικοί του Zcash δημιούργησαν ένα νέο θωρακισμένο pool και το συνόδευσαν με μία ελεγχόμενη από μηχανή μαθηματική απόδειξη, με περισσότερα από 2.700 θεωρήματα γραμμένα στον βοηθό αποδείξεων Lean, ότι δεν μπορεί να δημιουργήσει πλαστά χρήματα υπό τις δηλωμένες υποθέσεις του. Θα δούμε τι σημαίνουν η «ακεραιότητα ισορροπίας» και η «ορθότητα γνώσης», τι ακριβώς καλύπτει και τι δεν καλύπτει η απόδειξη, και πώς το παλιό pool αποσύρθηκε με ασφάλεια.
Μέρος της σειράς Τυπικής επαλήθευσης για ZecHub.