Στατική ανάλυση
 |
Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. |
Στην πληροφορική, στατική ανάλυση, στατική ανάλυση κώδικα ή στατική ανάλυση προγράμματος (Αγγλ.: static analysis, static code analysis, static program analysis), είναι η ανάλυση ενός προγράμματος που γίνεται χωρίς να εκτελεστεί το πρόγραμμα (η ανάλυση προγράμματος που γίνεται με εκτέλεσή του λέγεται δυναμική ανάλυση). Στις περισσότερες περιπτώσεις η ανάλυση γίνεται σε κάποιο επίπεδο πηγαίου κώδικα και πολλές φορές σε αντικειμενικό κώδικα. Ο όρος συνήθως αναφέρεται στην ανάλυση που γίνεται με κάποιο αυτόματο εργαλείο, ενώ η ανάλυση προγράμματος από άνθρωπο λέγεται κατανόηση προγράμματος.
Η ανάλυση που μπορεί να γίνει από αυτόματα εργαλεία ποικίλλει από αυτά που εξετάζουν τη συμπεριφορά μόνο συγκεκριμένων εκφράσεων ή δηλώσεων στο πρόγραμμα, έως αυτά που συμπεριλαμβάνουν ολόκληρο τον πηγαίο κώδικα ενός προγράμματος στην ανάλυση. Οι χρήσεις των πληροφοριών που πηγάζουν από την ανάλυση συμπεριλαμβάνουν από τον εντοπισμό πιθανών λαθών στο πρόγραμμα (π.χ. το εργαλείο lint), έως τυπικές μεθόδους που αποδεικνύουν μαθηματικά ιδιότητες για κάποιο δεδομένο πρόγραμμα (π.χ. ότι η συμπεριφορά του όντως ακολουθεί την τεχνική του περιγραφή).
Η μέτρηση μιας οποιασδήποτε ιδιότητας του προγράμματος, όπως και ο αντίστροφος σχεδιασμός (reverse engineering) θεωρούνται επίσης είδη στατικής ανάλυσης.
Μια αυξανόμενη εμπορική χρήση της στατικής ανάλυσης είναι η επαλήθευση ιδιοτήτων του λογισμικού που χρησιμοποιείται σε υπολογιστικά συστήματα όπου η ασφάλεια είναι κρίσιμη, για την αυτόματη ανακάλυψη πιθανών τρωτών σημείων στον κώδικα.
Τυπικές μέθοδοι
[Επεξεργασία | επεξεργασία κώδικα]Ο όρος τυπικές μέθοδοι χρησιμοποιείται στην ανάλυση λογισμικού και υλικού, και η οποία λειτουργεί αμιγώς με τη χρήση αυστηρών μαθηματικών μεθόδων. Οι μαθηματικές τεχνικές που χρησιμοποιούνται περιλαμβάνουν δηλωτική, λειτουργική ή αξιωματική σημασιολογία, και αφηρημένη διερμηνεία.
Αν υποθέσουμε ότι ο χώρος καταστάσεων των προγραμμάτων δεν είναι πεπερασμένος και μικρός, τότε αποδεικνύεται πως η εύρεση όλων των δυνατών λαθών χρόνου εκτέλεσης ή γενικότερα οποιουδήποτε είδους παραβίαση των προδιαγραφών στο τελικό αποτέλεσμα ενός προγράμματος, είναι αδύνατη: δεν υπάρχει καμία αυτόματη μηχανική μέθοδος που να μπορεί πάντα να βρίσκει με ακρίβεια αν ένα πρόγραμμα έχει λάθη εκτέλεσης ή όχι. Το αποτέλεσμα αυτό προκύπτει από τις εργασίες των Αλόνζο Τσερτς, Κουρτ Γκέντελ και Άλαν Τούρινγκ στη δεκαετία του 1930 (βλ. πρόβλημα τερματισμού και θεώρημα Ράις). Όπως συμβαίνει με τα περισσότερα άλυτα προβλήματα απόφασης, μπορεί κανείς να προσπαθήσει να δώσει χρήσιμες προσεγγιστικές λύσεις.
Κάποιες από τις τεχνικές υλοποίησης της τυπικής στατικής ανάλυσης είναι:
- Ο έλεγχος μοντέλων (model checking) εξετάζει συστήματα που έχουν πεπερασμένη κατάσταση, ή μπορούν να αναχθούν σε πεπερασμένη κατάσταση με αφαίρεση
- Η ανάλυση ροής δεδομένων (data-flow analysis) βασίζεται σε δομές συνδέσμων (lattices) για τη συλλογή πληροφοριών για το πιθανό σύνολο τιμών
- Η αφηρημένη διερμηνεία (abstract interpretation) μοντελοποιεί το αποτέλεσμα κάθε εντολής στην κατάσταση μιας αφηρημένης μηχανής (δηλαδή 'εκτελεί' το πρόγραμμα βασιζόμενη στις μαθηματικές ιδιότητες κάθε εντολής). Η αφηρημένη αυτή μηχανή προσεγγίζει όλες τις δυνατές συμπεριφορές του συστήματος. Έτσι, το αφηρημένο σύστημα είναι ευκολότερο να αναλυθεί μαθηματικά, με κόστος την μη πληρότητα της ανάλυσης (δεν ισχύει πάντα κάθε ιδιότητα του πραγματικού και για το αφηρημένο). Αν γίνει σωστά, παρ' όλα αυτά, η αφηρημένη διερμηνεία είναι συνεπής (κάθε ιδιότητα του αφηρημένου ισχύει και για το πραγματικό).
- Η χρήση ισχυρισμών στον κώδικα ενός προγράμματος όπως προτάθηκε αρχικά στη λογική Χόαρ. Υπάρχουν εργαλεία που την υποστηρίζουν για κάποιες γλώσσες προγραμματισμού, όπως η SPARK, ένα υποσύνολο της Ada και η JML (με χρήση του ESC/Java και του ESC/Java2).
Σχετικά άρθρα
[Επεξεργασία | επεξεργασία κώδικα]- Ανάλυση προγράμματος (πληροφορική)
- Δυναμική ανάλυση προγράμματος
- Ανάλυση σχήματος
- Έλεγχος μοντέλων
- Τυπική σημασιολογία των γλωσσών προγραμματισμού
- Τυπική επαλήθευση
- Δοκιμή λογισμικού
- Γεννήτρια τεκμηρίωσης
- Συμβολική ανάλυση προγράμματος
Εξωτερικοί σύνδεσμοι
[Επεξεργασία | επεξεργασία κώδικα]- The SAMATE Project, πηγή για εργαλεία Αυτόματης Στατικής Ανάλυσης
- Code Quality Improvement - Coding standards conformance checking (DDJ)
- Episode 59: Static Code Analysis Interview (Podcast) at Software Engineering Radio
- Implementing Automated Governance for Coding Standards Εξηγεί γιατί και πώς εισήχθη η στατική ανάλυση στη διαδικασία ανάπτυξης προγραμμάτων
Βιβλιογραφία
[Επεξεργασία | επεξεργασία κώδικα]- International Static Analysis Symposium proceedings Αρχειοθετήθηκε 2009-04-21 στο Wayback Machine., Springer-Verlag 1994-.
- Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 “Static Techniques for Security,” Stanford doctoral thesis, 2006.
- Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, “Using Static Analysis to Find Bugs Αρχειοθετήθηκε 2009-07-26 στο Wayback Machine.,” IEEE Software, vol. 25, no. 5, pp. 22–29, Sep./Oct. 2008, doi:10.1109/MS.2008.130
- Adam Kolawa, Why, When, How: Code Analysis[νεκρός σύνδεσμος] white paper