Ερευνητές από Κρατικό Ινστιτούτο Έρευνας Πληροφορικής και Αυτοματισμού (INRIA), Η Microsoft Research και το Πανεπιστήμιο Carnegie Mellon παρουσίασαν η πρώτη δοκιμαστική έκδοση του την κρυπτογραφική βιβλιοθήκη EverCrypt αναπτύχθηκε στο πλαίσιο του έργου Everest και χρησιμοποιώντας μαθηματικές μεθόδους επίσημης επαλήθευσης της αξιοπιστίας.
Λόγω των δυνατοτήτων και των επιδόσεων του, Το EverCrypt είναι πολύ κοντά στις υπάρχουσες βιβλιοθήκες κρυπτογράφησης (OpenSSL) που όμως, σε αντίθεση με αυτά, προσφέρει πρόσθετες εγγυήσεις αξιοπιστίας και ασφάλειας.
Π.χ. η διαδικασία επαλήθευσης περιορίζεται στον ορισμό λεπτομερών προδιαγραφών που περιγράφουν όλες τις συμπεριφορές του προγράμματος και η μαθηματική απόδειξη ότι ο γραπτός κώδικας πληροί τις καθορισμένες προδιαγραφές.
Σε αντίθεση με τις μεθόδους ποιοτικού ελέγχου που βασίζονται σε στοιχεία, η επαλήθευση παρέχει αξιόπιστες εγγυήσεις ότι το πρόγραμμα θα εκτελείται μόνο όπως προβλέπεται από τους προγραμματιστές και δεν υπάρχουν συγκεκριμένες κατηγορίες σφαλμάτων.
Για παράδειγμα, συμμόρφωση με τις προδιαγραφές εγγυάται την ασφαλή εργασία με τη μνήμη και την απουσία σφαλμάτων που οδηγούν σε υπερχείλιση buffer, δείκτες παραπομπής, πρόσβαση σε ήδη ελευθερωμένες περιοχές μνήμης ή διπλή απελευθέρωση μπλοκ μνήμης.
Τι είναι το EverCrypt;
EverCrypt παρέχει ισχυρό έλεγχο τύπου και αξίας: Ένα στοιχείο δεν θα μεταβιβάσει ποτέ παραμέτρους στο άλλο στοιχείο που δεν είναι συμβατό και δεν θα αποκτήσει πρόσβαση στις εσωτερικές καταστάσεις των άλλων στοιχείων.
συμπεριφορά εισόδου/εξόδου συμμορφώνεται πλήρως με τις ενέργειες απλών μαθηματικών συναρτήσεων, τα οποία ορίζονται στα κρυπτογραφικά πρότυπα.
Για προστασία από επιθέσεις σε κανάλια τρίτων, συμπεριφορά κατά τους υπολογισμούς (για παράδειγμα, η διάρκεια της εκτέλεσης ή η παρουσία προσβάσεων σε συγκεκριμένη μνήμη) δεν εξαρτάται από τα απόρρητα δεδομένα που υποβάλλονται σε επεξεργασία.
Ο κωδικός του έργου Είναι γραμμένο στη λειτουργική γλώσσα F* (F αστέρι) , που παρέχει ένα σύστημα εξαρτημένων τύπων και βελτιώσεων, που καθιστούν δυνατή τη θέσπιση ακριβών προδιαγραφών (μαθηματικό μοντέλο) για προγράμματα και διασφαλίζουν την ορθότητα και την εφαρμογή χωρίς σφάλματα χρησιμοποιώντας τύπους SMT και βοηθητικά εργαλεία δοκιμών.
Ο κωδικός F* διανέμεται με την άδεια Apache 2.0 και οι τελικές μονάδες C και assembler με την άδεια MIT.
Με βάση τον κωδικό αναφοράς F*, assembler, C, OCaml, JavaScript δημιουργείται και τον κώδικα συναρμολόγησης web.
Μερικά μέρη του κώδικα ετοιμάζεται από το έργο χρησιμοποιούνται ήδη στον Firefox, τον πυρήνα των Windows , η αλυσίδα των μπλοκ Tezos και VPN Wireguard.
EverCrypt Components
Στην ουσία, Το EverCrypt συνδυάζει δύο προηγουμένως διαφορετικά έργα από το HACL* και το Vale, παρέχοντας ένα ενοποιημένο API που βασίζεται σε αυτά και καθιστώντας τα κατάλληλα για χρήση σε πραγματικά έργα.
Το HACL * είναι γραμμένο σε Low* και προορίζεται να παρέχει κρυπτογραφικά πρωτόγονα για χρήση σε προγράμματα C που χρησιμοποιούν τα API στυλ libsodium και NaCL.
Το έργο Ο Vale ανέπτυξε μια συγκεκριμένη γλώσσα τομέα για τη δημιουργία επιταγών στο assembler.
Συνδυάζονται περίπου 110 χιλιάδες γραμμές κώδικα HACL * σε χαμηλή γλώσσα * και 25 χιλιάδες γραμμές κώδικα για το Vale και ξαναγράφονται σε περίπου 70 χιλιάδες γραμμές κώδικα στην καθολική γλώσσα F *, η οποία επίσης αναπτύσσεται ως μέρος του έργου Everest.
Η πρώτη έκδοση της βιβλιοθήκης EverCrypt διαθέτει επαληθευμένες υλοποιήσεις των παρακάτω κρυπτογραφικών αλγορίθμων που προτείνονται σε εκδόσεις C ή assembler (όταν χρησιμοποιείτε τη βιβλιοθήκη.
Από αυτά, η σελίδα του έργου επισημαίνει:
- Αλγόριθμοι κατακερματισμού: όλες οι παραλλαγές των SHA2, SHA3, SHA1 και MD5
- Κωδικοί ελέγχου ταυτότητας: HMAC μέσω SHA1, SHA2-256, SHA2-384 και SHA2-512 για έλεγχο ταυτότητας πηγής δεδομένων
- Αλγόριθμος δημιουργίας κλειδιού HKDF (συνάρτηση εξαγωγής και επέκτασης κλειδιού βάσει HMAC)
- Κρυπτογράφηση ροής ChaCha20 (διαθέσιμη μη βελτιστοποιημένη έκδοση C)
- Poly1305 Message Authentication Algorithm (MAC) (έκδοση C και assembler)
- Πρωτόκολλο Diffie-Hellman για ελλειπτικές καμπύλες Curve25519 (εκδόσεις C και assembler με βελτιστοποιήσεις που βασίζονται σε οδηγίες BMI2 και ADX)
- Λειτουργία κρυπτογράφησης αποκλεισμού AEAD (επαληθευμένη κρυπτογράφηση) ChachaPoly (μη βελτιστοποιημένη έκδοση C)
- Λειτουργία κρυπτογράφησης μπλοκ AEAD AES-GCM (έκδοση συναρμολογητή με βελτιστοποιήσεις AES-NI).
Κατά την πρώτη έκδοση alpha, η επαλήθευση κωδικού έχει ήδη ολοκληρωθεί σε μεγάλο βαθμό, αλλά υπάρχουν ακόμα κάποιες ακάλυπτες περιοχές.
Επιπλέον, το API δεν έχει ακόμη σταθεροποιηθεί, το οποίο θα επεκταθεί στις ακόλουθες εκδόσεις alpha (Σχεδιάζεται να ενοποιηθούν οι δομές για όλα τα API.
Μεταξύ των ελαττωμάτων, σημειώνεται επίσης η υποστήριξη για την αρχιτεκτονική x86_64 (στο πρώτο στάδιο, ο κύριος στόχος είναι η αξιοπιστία, ενώ η βελτιστοποίηση και οι πλατφόρμες θα εφαρμοστούν στη δεύτερη θέση).
πηγή: https://jonathan.protzenko.fr