Statyczna analiza programu - Static program analysis
Rozwój oprogramowania |
---|
Analiza statyczna programu to analiza oprogramowania komputerowego wykonywana bez faktycznego wykonywania programów, w przeciwieństwie do analizy dynamicznej , która jest analizą wykonywaną na programach podczas ich wykonywania. W większości przypadków analiza jest wykonywana na jakiejś wersji kodu źródłowego , aw innych przypadkach na jakiejś postaci kodu wynikowego .
Termin ten jest zwykle stosowany do analizy wykonywanej przez zautomatyzowane narzędzie , przy czym analiza wykonywana przez człowieka jest nazywana zrozumieniem programu, zrozumieniem programu lub przeglądem kodu . Inspekcje oprogramowania i instruktaże oprogramowania są również wykorzystywane w tym drugim przypadku.
Racjonalne uzasadnienie
Zaawansowanie analizy wykonywanej przez narzędzia różni się od tych, które uwzględniają tylko zachowanie poszczególnych instrukcji i deklaracji, po takie, które uwzględniają w swojej analizie pełny kod źródłowy programu. Zastosowania informacji uzyskanych z analizy są różne, od wskazywania możliwych błędów kodowania (np. narzędzie lint ) po metody formalne, które matematycznie udowadniają właściwości danego programu (np. jego zachowanie jest zgodne z jego specyfikacją).
Metryki oprogramowania i inżynierię odwrotną można opisać jako formy analizy statycznej. Wyprowadzanie metryk oprogramowania i analiza statyczna są coraz częściej stosowane razem, zwłaszcza przy tworzeniu systemów wbudowanych, poprzez definiowanie tzw. celów jakości oprogramowania .
Rosnące komercyjne wykorzystanie analizy statycznej polega na weryfikacji właściwości oprogramowania używanego w systemach komputerowych o krytycznym znaczeniu dla bezpieczeństwa oraz lokalizowaniu potencjalnie podatnego kodu. Na przykład następujące branże zidentyfikowały wykorzystanie statycznej analizy kodu jako sposobu na poprawę jakości coraz bardziej wyrafinowanego i złożonego oprogramowania:
- Oprogramowanie medyczne : Amerykańska Agencja ds. Żywności i Leków (FDA) zidentyfikowała zastosowanie analizy statycznej w urządzeniach medycznych.
- Oprogramowanie jądrowe: W Wielkiej Brytanii Urząd Regulacji Jądrowych (ONR) zaleca stosowanie analizy statycznej w systemach ochrony reaktorów .
- Oprogramowanie lotnicze (w połączeniu z analizą dynamiczną )
- Motoryzacja i maszyny (funkcjonalne funkcje bezpieczeństwa stanowią integralną część każdej fazy rozwoju produktu motoryzacyjnego, ISO 26262 , rozdział 8.)
Badanie przeprowadzone w 2012 r. przez VDC Research wykazało, że 28,7% ankietowanych inżynierów oprogramowania wbudowanego używa obecnie narzędzi do analizy statycznej, a 39,7% spodziewa się, że użyje ich w ciągu 2 lat. Badanie z 2010 r. wykazało, że 60% ankietowanych programistów biorących udział w europejskich projektach badawczych korzystało przynajmniej z podstawowych wbudowanych w IDE analizatorów statycznych. Jednak tylko około 10% korzystało z dodatkowego innego (i być może bardziej zaawansowanego) narzędzia analitycznego.
W branży bezpieczeństwa aplikacji używana jest również nazwa Static application security testing (SAST). SAST jest ważną częścią cykli rozwoju zabezpieczeń (SDL), takich jak SDL zdefiniowany przez Microsoft i powszechną praktyką w firmach programistycznych.
Rodzaje narzędzi
OMG ( Object Management Group ) opublikowało badanie dotyczące rodzajów analizy oprogramowania wymaganej do pomiaru i oceny jakości oprogramowania . Ten dokument „Jak dostarczyć odporne, bezpieczne, wydajne i łatwo modyfikowalne systemy IT zgodnie z zaleceniami CISQ” opisuje trzy poziomy analizy oprogramowania.
- Poziom jednostki
- Analiza, która odbywa się w ramach określonego programu lub podprogramu, bez łączenia się z kontekstem tego programu.
- Poziom technologii
- Analiza uwzględniająca interakcje między programami jednostkowymi, aby uzyskać bardziej holistyczny i semantyczny obraz całego programu w celu znalezienia problemów i uniknięcia oczywistych fałszywych alarmów. Na przykład można statycznie przeanalizować stos technologii Androida, aby znaleźć błędy uprawnień.
- Poziom systemu
- Analiza uwzględniająca interakcje między programami jednostkowymi, ale bez ograniczania się do jednej konkretnej technologii lub języka programowania.
Można zdefiniować kolejny poziom analizy oprogramowania.
- Poziom misji/biznesu
- Analiza uwzględniająca warunki, reguły i procesy warstwy biznesowej/misji, które są realizowane w ramach systemu oprogramowania pod kątem jego działania w ramach działań w warstwie przedsiębiorstwa lub programu/misji. Elementy te są implementowane bez ograniczania się do jednej konkretnej technologii lub języka programowania, aw wielu przypadkach są dystrybuowane w wielu językach, ale są statycznie wyodrębniane i analizowane w celu zrozumienia systemu w celu zapewnienia misji.
Metody formalne
Metody formalne to termin stosowany do analizy oprogramowania (i sprzętu komputerowego ), której wyniki uzyskuje się wyłącznie dzięki zastosowaniu rygorystycznych metod matematycznych. Matematyczne techniki stosowane obejmują denotational semantykę , aksjomatyczne semantyki , semantyka operacyjnych i abstrakcyjnej interpretacji .
Poprzez proste sprowadzenie do problemu zatrzymania , możliwe jest udowodnienie tego (dla dowolnego kompletnego języka Turinga ), znalezienie wszystkich możliwych błędów w czasie wykonywania w dowolnym programie (lub ogólniej wszelkiego rodzaju naruszenia specyfikacji końcowego wyniku program) jest nierozstrzygalny : nie ma mechanicznej metody, która może zawsze odpowiedzieć zgodnie z prawdą, czy dowolny program może, czy nie, wykazywać błędy w czasie wykonywania. Wynik ten pochodzi z prac Churcha , Gödla i Turinga z lat 30. (patrz: Problem zatrzymania i twierdzenie Rice'a ). Podobnie jak w przypadku wielu pytań nierozstrzygalnych, nadal można próbować podać przydatne przybliżone rozwiązania.
Niektóre z technik implementacji formalnej analizy statycznej obejmują:
- Interpretacja abstrakcyjna , aby modelować wpływ, jaki każde stwierdzenie wywiera na stan abstrakcyjnej maszyny (tj. „wykonuje” oprogramowanie w oparciu o matematyczne właściwości każdej instrukcji i deklaracji). Ta abstrakcyjna maszyna nadmiernie przybliża zachowania systemu: w ten sposób abstrakcyjny system jest łatwiejszy do analizy kosztem niekompletności (nie każda właściwość prawdziwa oryginalnego systemu jest prawdziwa dla systemu abstrakcyjnego). Jednak prawidłowo wykonana interpretacja abstrakcyjna jest słuszna (każda prawdziwa właściwość systemu abstrakcyjnego może być odwzorowana na prawdziwą właściwość systemu oryginalnego).
- Analiza przepływu danych , oparta na sieciach technika gromadzenia informacji o możliwym zestawie wartości;
- Logika Hoare'a , formalny system z zestawem logicznych reguł do rygorystycznego wnioskowania o poprawności programów komputerowych . Istnieje obsługa narzędzi dla niektórych języków programowania (np. języka programowania SPARK (podzbiór Ada ) i języka modelowania Java —JML — przy użyciu ESC/Java i ESC/Java2 , wtyczki Frama-C WP ( najsłabszy warunek wstępny ) dla C język rozszerzony o ACSL ( ANSI/ISO C Specification Language ) ).
- Sprawdzanie modelu , uwzględnia systemy, które mają skończony stan lub mogą zostać zredukowane do skończonego stanu przez abstrakcję ;
- Wykonanie symboliczne , używane do wyprowadzania wyrażeń matematycznych reprezentujących wartość zmutowanych zmiennych w określonych punktach kodu.
Analiza statyczna oparta na danych
Analiza statyczna oparta na danych wykorzystuje duże ilości kodu do wywnioskowania reguł kodowania. Na przykład, można wykorzystać wszystkie otwarte pakiety Java na GitHubie, aby nauczyć się dobrej strategii analizy. Wnioskowanie o regułach może wykorzystywać techniki uczenia maszynowego. Na przykład wykazano, że jeśli ktoś za bardzo odbiega od sposobu korzystania z API zorientowanego obiektowo, prawdopodobnie jest to błąd. Możliwe jest również uczenie się na podstawie dużej liczby wcześniejszych poprawek i ostrzeżeń.
Zobacz też
- Audyt kodu
- Generator dokumentacji
- Semantyka formalna języków programowania
- Weryfikacja formalna
- Lista narzędzi do statycznej analizy kodu
- Analiza kształtu (oprogramowanie)
- Jakość oprogramowania
- Certyfikat Jakości Oprogramowania
- ISO 26262
- ISO 9126 (obecnie seria ISO 25000)
- Lint (oprogramowanie)
Bibliografia
Dalsza lektura
- Ayewah, Nataniel; Hovemeyera, Dawida; Morgenthaler, J. David; Penixa, Jana; Pugh, William (2008). „Korzystanie z analizy statycznej, aby znaleźć błędy”. Oprogramowanie IEEE . 25 (5): 22–29. CiteSeerX 10.1.1.187.8985 . doi : 10.1109/MS.2008.130 . S2CID 20646690 .
- Brian Chess, Jacob West (Fortify Software) (2007). Bezpieczne programowanie z analizą statyczną . Addisona-Wesleya. Numer ISBN 978-0-321-42477-8.
- Flemminga Nielsona; Hanne R. Nielson; Chris Hankin (2004-12-10). Zasady analizy programu (1999 (poprawione 2004) ed.). Skoczek. Numer ISBN 978-3-540-65410-0.
- „Abstrakcyjna interpretacja i analiza statyczna”, International Winter School on Semantics and Applications 2003, David A. Schmidt
Zewnętrzne linki
- Poprawa jakości kodu - Sprawdzanie zgodności ze standardami kodowania (DDJ)
- Konkurs na weryfikację oprogramowania (SV-COMP)
- Odcinek 59: Wywiad dotyczący analizy kodu statycznego ( Podcast ) w Radiu Inżynierii Oprogramowania
- Implementing Automated Governance for Coding Standards Wyjaśnia, dlaczego i jak zintegrować statyczną analizę kodu z procesem kompilacji
- Zintegruj analizę statyczną z procesem tworzenia oprogramowania
- Projekt SAMATE , źródło narzędzi do automatycznej analizy statycznej
- Praktyczne wprowadzenie do statycznej analizy kodu