Statisk programanalys - Static program analysis

Mjukvaruutveckling
Kärnverksamhet
Paradigmer och modeller
Metoder och ramar
Stödja discipliner
Övningar
Verktyg
Standarder och kunskapsorgan
Ordlistor
Konturer

Statisk programanalys är analysen av datorprogramvara som utförs utan att faktiskt köra program, till skillnad från dynamisk analys , som är analys som utförs på program medan de körs. I de flesta fall utförs analysen på någon version av källkoden , och i de andra fallen, någon form av objektkoden .

Termen används vanligtvis på analysen som utförs av ett automatiserat verktyg , där mänsklig analys kallas programförståelse, programförståelse eller kodgranskning . Programvaruinspektioner och genomgångar av programvara används också i det senare fallet.

Logisk grund

Den sofistikerade analysen som utförs med verktyg varierar från de som bara tar hänsyn till beteendet hos enskilda uttalanden och deklarationer, till de som inkluderar ett källkod för ett program i sin analys. Användningen av den information som erhålls från analysen varierar från att markera möjliga kodningsfel (t.ex. luddverktyget ) till formella metoder som matematiskt bevisar egenskaper för ett givet program (t.ex. dess beteende matchar det i dess specifikation).

Programvarumätningar och omvänd teknik kan beskrivas som former av statisk analys. Härledande mjukvarumätningar och statisk analys används alltmer tillsammans, särskilt när det gäller att skapa inbyggda system, genom att definiera så kallade mjukvarukvalitetsmål .

En växande kommersiell användning av statisk analys är i verifieringen av egenskaperna hos programvara som används i säkerhetskritiska datorsystem och lokalisering av potentiellt sårbar kod. Till exempel har följande branscher identifierat användningen av statisk kodanalys som ett sätt att förbättra kvaliteten på allt mer sofistikerad och komplex programvara:

  1. Medicinsk programvara : US Food and Drug Administration (FDA) har identifierat användningen av statisk analys för medicintekniska produkter.
  2. Kärnämnesprogramvara: I Storbritannien rekommenderar Office for Nuclear Regulation (ONR) användning av statisk analys av reaktorskyddssystem .
  3. Luftfartsprogramvara (i kombination med dynamisk analys )
  4. Fordon och maskiner (funktionella säkerhetsfunktioner utgör en integrerad del av varje produktutvecklingsfas för bilar, ISO 26262 , avsnitt 8.)

En studie 2012 av VDC Research rapporterade att 28,7% av de undersökta inbyggda programvaruingenjörerna för närvarande använder statiska analysverktyg och 39,7% förväntar sig att använda dem inom 2 år. En studie från 2010 visade att 60% av de intervjuade utvecklarna i europeiska forskningsprojekt åtminstone använde sina grundläggande IDE inbyggda statiska analysatorer. Men bara cirka 10% använde ytterligare ett (och kanske mer avancerat) analysverktyg.

I applikationssäkerhetsindustrin används också namnet Static application security testing (SAST). SAST är en viktig del av Security Development Lifecycles (SDL) som SDL definierat av Microsoft och en vanlig praxis i programvaruföretag.

Verktygstyper

OMG ( Object Management Group ) publicerade en studie om vilka typer av mjukvaroanalyser som krävs för mätning och bedömning av mjukvarukvalitet . Detta dokument om "Hur man levererar motståndskraftiga, säkra, effektiva och enkelt ändrade IT -system i linje med CISQ -rekommendationer" beskriver tre nivåer av mjukvaroanalys.

Enhetsnivå
Analys som sker inom ett specifikt program eller underprogram utan att ansluta till programmets sammanhang.
Tekniknivå
Analys som tar hänsyn till interaktioner mellan enhetsprogram för att få en mer holistisk och semantisk syn på det övergripande programmet för att hitta problem och undvika uppenbara falska positiva. Till exempel är det möjligt att statiskt analysera Android -teknikstacken för att hitta behörighetsfel.
Systemnivå
Analys som tar hänsyn till interaktionerna mellan enhetsprogram, men utan att vara begränsad till en specifik teknik eller programmeringsspråk.

En ytterligare nivå av mjukvaroanalys kan definieras.

Mission/affärsnivå
Analys som tar hänsyn till affärs-/uppdragslagers villkor, regler och processer som implementeras inom mjukvarusystemet för dess drift som en del av företags- eller program-/uppdragslageraktiviteter. Dessa element implementeras utan att vara begränsade till en specifik teknik eller programmeringsspråk och distribueras i många fall över flera språk, men extraheras och analyseras statiskt för systemförståelse för uppdragsförsäkring.

Formella metoder

Huvudartikel: Formella metoder

Formella metoder är termen som används för analys av programvara (och datorhårdvara ) vars resultat erhålls enbart genom användning av rigorösa matematiska metoder. De matematiska tekniker som används inkluderar denotationssemantik , axiomatisk semantik , operativ semantik och abstrakt tolkning .

Genom en enkel minskning av stoppproblemet är det möjligt att bevisa att (för alla Turing-fullständiga språk) att hitta alla möjliga körtidsfel i ett godtyckligt program (eller mer allmänt någon form av kränkning av en specifikation om det slutliga resultatet av ett program) kan inte avgöras : det finns ingen mekanisk metod som alltid kan svara sanningsenligt om ett godtyckligt program kan visa körtidsfel eller inte. Detta resultat härstammar från verk av Church , Gödel och Turing på 1930 -talet (se: Halting problem and Rices theorem ). Som med många oavgörbara frågor kan man fortfarande försöka ge användbara ungefärliga lösningar.

Några av implementeringsteknikerna för formell statisk analys inkluderar:

  • Abstrakt tolkning , för att modellera effekten som varje påstående har på tillståndet för en abstrakt maskin (dvs det "kör" programvaran baserat på de matematiska egenskaperna för varje påstående och deklaration). Denna abstrakta maskin över-approximerar systemets beteenden: det abstrakta systemet görs därför enklare att analysera, på bekostnad av ofullständighet (inte alla egendomar som gäller för det ursprungliga systemet är sanna för det abstrakta systemet). Om det görs på rätt sätt är abstrakt tolkning dock sund (varje egenskap som gäller för det abstrakta systemet kan mappas till en verklig egenskap hos det ursprungliga systemet).
  • Dataflödesanalys , en gitterbaserad teknik för att samla information om den möjliga uppsättningen värden;
  • Hoare logic , ett formellt system med en uppsättning logiska regler för att noggrant resonera om att datorprogram är korrekta . Det finns verktygsstöd för vissa programmeringsspråk (t.ex. SPARK-programmeringsspråket (en delmängd av Ada ) och Java-modelleringsspråket —JML — med hjälp av ESC/Java och ESC/Java2 , Frama-C WP ( svagaste förutsättning ) plugin för C språk utökat med ACSL ( ANSI/ISO C Specification Language )).
  • Modellkontroll , betraktar system som har ändligt tillstånd eller kan reduceras till ändliga tillstånd genom abstraktion ;
  • Symbolisk körning , som används för att härleda matematiska uttryck som representerar värdet av muterade variabler vid särskilda punkter i koden.

Datadriven statisk analys

Datadriven statisk analys använder stora mängder kod för att utläsa kodningsregler. Till exempel kan man använda alla Java-paket med öppen källkod på GitHub för att lära sig en bra analysstrategi. Regelens slutsats kan använda maskininlärningstekniker. Till exempel har det visat sig att när man avviker för mycket på sättet man använder ett objektorienterat API, så är det troligtvis ett fel. Det är också möjligt att lära av en stor mängd tidigare korrigeringar och varningar.

Se även

Referenser

Vidare läsning

externa länkar