Οι επιστήμονες των υπολογιστών είναι πολύ κοντά στην ανάπτυξη ενός κώδικα υπολογιστή που δεν θα παραβιάζετε από Hacker
Με σκοπό την προστασία των συσκευών από επιθέσεις, οι μηχανικοί από την Defense Advanced Research Projects (DARPA) έχουν εργαστεί σε ένα νέου είδους μηχανισμό ασφαλείας – ένα λογισμικό σύστημα που δεν θα μπορεί να παραβιαστεί.
Για τσεκάρει το μηχανισμό ασφαλείας, η DARPA έδωσε στους Hacker της “Red Team” έξι εβδομάδες για να προσπαθήσουν να πάρουν τον έλεγχο ενός μη επανδρωμένου στρατιωτικού ελικοπτέρου, που κατασκευάστηκε από μία εταιρεία γνωστή ως “Little Birds». Ακόμα έδωσαν στην ομάδα πρόσθετες πληροφορίες για το δίκτυο υπολογιστών της. Ωστόσο, δεν κατάφεραν να σπάσουν τον κωδικό της άμυνας του Little Bird.
«Δεν ήταν σε θέση να εισβάλουν και να διαταράξουν τη λειτουργία με κανένα τρόπο», δήλωσε η Kathleen Fisher, καθηγήτρια της επιστήμης των υπολογιστών στο Πανεπιστήμιο Tufts και διευθυντής του προγράμματος High-Assurance Cyber Military Systems (HACMS). «Αυτό το αποτέλεσμα έκανε όλους στη DARPA να πουν: ω Θεέ μου, μπορούμε να χρησιμοποιήσουμε πραγματικά αυτή την τεχνολογία σε συστήματα που μας ενδιαφέρουν.»
Ο κωδικός υπολογιστή που υποστηρίζει το hardware ήταν ουσιαστικά απαραβίαστος με την τρέχουσα τεχνολογία, αναφέρει η WIRED. Η έκθεση σημειώνει ότι ο κωδικός είναι “τόσο αξιόπιστος όσο μια μαθηματική απόδειξη.” Η προσέγγιση του προγραμματισμού είναι γνωστή ως τυπική επαλήθευση και αξιολογείται κυρίως σχετικά με το εάν λειτουργεί. Κάθε δήλωση ακολουθεί λογικά την επόμενη. Ένα σύνολο του προγράμματος μπορεί να ελεγχθεί με την ίδια εμπιστοσύνη που οι μαθηματικοί μπορούν να αποδείξουν τα θεωρήματά του.
«Γράφετε έναν μαθηματικό τύπο που περιγράφει τη συμπεριφορά του προγράμματος και χρησιμοποιεί κάποιο είδος ελεγκτή που πρόκειται να ελέγξει την ορθότητα της εν λόγω δήλωσης» είπε ο Bryan Parno, που κάνει την έρευνα για τον επίσημη έλεγχο και την ασφάλεια στη Microsoft Research.
Δεδομένου ότι οι περισσότερες από τις επιθέσεις γίνονται με την αξιοποίηση σφαλμάτων και λάθη στον κώδικα, καθίσταται απαραίτητο να υπάρχει επίσημη επιβεβαίωση ότι είναι απαραβίαστο. Με την προσέγγιση αυτή, οι κωδικοί που έχουν υποστεί αυτή τη διαδικασία υποτίθεται ότι είναι απρόσιτη. Από τη στιγμή που ο κωδικός λειτουργεί δεν αφήνει κενά για να τα εκμεταλλευτούν οι Hacker.
Ο κώδικας είναι ακόμα στα αρχικά στάδια και απαιτεί πολλή δουλειά και δοκιμές για να ολοκληρωθεί.
