Sicherung der Codequalität Statische Analyse ergänzt

In sicherheits-, missions- und geschäftskritischen Umgebungen sowie im Bereich von Embedded Systemen müssen sich Softwareingenieure aktiv um Codequalität kümmern. Dabei müssen sie Kodierungsstandards einhalten, um Fehler zu vermeiden. Allerdings findet die etablierte statische Analyse nicht alle Defekte, wert- und zustandssensitive Programmfehler bleiben beispielsweise unerkannt. Daher sollte die statische Analyse um die Datenflussanalyse ergänzt werden.

Die statische Analyse umfasst eine Reihe von Technologien und Techniken, die ihre diagnostischen Vorteile aus einer statischen Überprüfung des Codes ohne dessen Ausführung beziehen. Ein bewährtes Konzept konzentriert sich vor allem auf die Sprachanalyse für die Programmiersprachen C und C++. Dieses leistet eine umfassende Diagnose, mit der Softwareentwickler ein breites Spektrum von Kodierungsproblemen ermitteln und korrigieren beziehungsweise von vornherein vermeiden können.

Dieses Konzept beruht auf detailliertem Wissen zu grundlegenden Sprachproblemen und bietet damit Glaubwürdigkeit für den Einsatz von Kodierungsstandards sowie bei der Vermeidung von Qualitätsproblemen beim Code. Bei der statischen Analyse geht es meist um eine detaillierte Überprüfung der Sprachsemantik, wobei man sich vor allem auf eine genaue Untersuchung von Typen, Ausdrücken, Präprozessor- und Template-Einstellungen sowie andere komplexe Aspekte der Darstellung und Transformation vom Quellcode in einen kompilierten Code konzentriert.

Um dieses Konzept zur Sicherung der Code-qualität zu vervollständigen, ist auch eine wert- und zustandssensitive Fehlererkennung notwendig. Die so genannte Datenflussanalyse nutzt eine Reihe von Techniken für eine statische Analyse des Quellcodes, die auch das Laufzeitverhalten von Programmen untersucht. Mit einer Überprüfung der Steuerungsabläufe sowie einer Überwachung von Objektzuständen und -werten an jedem Punkt im Programm lassen sich potenzielle Probleme ermitteln, etwa undefiniertes Verhalten, logische Anomalien oder andere interessierende Aspekte.

Mit einer so erweiterten statischen Analyse lassen sich bekannte Schwachstellen von C/C++ aufdecken. Dazu zählen fehlerhafte Zeiger-Dereferenzierung (Pointer-Dereferencing), Verletzungen von Array-Grenzen, Teilung durch Null sowie Speicher- und Ressourcen-Missmanagement, die Verwendung undefinierter Datenwerte und andere, ähnliche Probleme. Sowohl die Sprach- als auch die Datenflussanalyse sind wichtige Aspekte einer robusten statischen Analyselösung.

Spezielle Solver im Einsatz

In der neuesten Version von »QA·C« hat PRQA die Funktionen zur Datenflussanalyse überarbeitet. Sie umfassen Geschwindigkeits- und Performanceverbesserungen in Bereichen, die man früher von Theorem-Solver-Engines aus der Forschung kannte. Das Konzept nutzt einen speziellen Bit-Vektor-Solver aus der Familie der »Satisfiable Modulo Theories«-Solver (SMT).

Mit ihnen lässt sich der Zustand von Variablen während der Programmausführung modellieren. Code-Statements, die Einschränkungen für den Wert von Variablen definieren, werden dabei in eine Reihe von Assertionen übersetzt, die man dann an den Solver übergibt. Dieser erhält eine Reihe von Suchanfragen, um die zu meldenden Bedingungen zu identifizieren.

Dank der Nutzung eines Bit-Vektor-Modells, bei dem alle Bits eines skalaren oder zusammengesetzten Typs einzeln und korrekt verarbeitet werden, eignet sich diese Lösung besonders für Embedded-Umgebungen. Bei solchen Umgebungen sind aufgrund eines begrenzten Platzangebots und vieler Hardware-Schnittstellen oft Manipulationen auf Bit-Ebene und damit verbundene Kodierungsstile erforderlich.

Ein detaillierter Kontrollflussgraph (Control Flow Graph, CFG) für die jeweilige Funktion bildet den Kern dieser Datenfluss-Technik. Beim Aufbau dieses CFG im Zusammenspiel mit der Nutzung des SMT-Solvers sind invariante Verzweigungen zu eliminieren; das sind Logikbedingungen, die jeweils immer falsch oder immer richtig sind. Für eine genaue Modellierung des Verhaltens von Schleifenkonstrukten sind weitere Informationen bereitzustellen.

Ein solches Modell verfolgt den Zustand von Variablen durch jedes Statement des Programms. Dabei beeinflussen »Ereignisse« wie Initialisierungen, Zuweisungen, logische Vergleiche, Funktionsaufrufe und Schleifenkonstrukte den Zustand einer Variablen. Eine Analyse und Erkennung wird für jede sprachliche Schwachstelle oder jedes interessierende Logikfragment im Code durchgeführt.

Für jeden aufgefundenen Fall wird dem SMT-Solver ein Satz aller relevanten Zusicherungen oder Assertionen übergeben, zusammen mit einer Anfrage, welche die Wahrscheinlichkeit für das Auftreten einer derartigen, spezifischen Schwachstelle untersucht. Dabei ist zu beobachten, dass es für eine normal dimensionierte Funktion viele derartige Anfragen gibt und dass die Anzahl der Assertionen für jede Anfrage proportional zum Umfang und der Komplexität der Funktion zunimmt.

Allerdings werden dank eines Designs mit einer »verzögerten Architektur« nur die relevanten Assertionen zusammen mit jeder Anfrage übergeben. Skalierungs- und Performanceprobleme sind daher hauptsächlich mit der Komplexität des Variableneinsatzes in der Funktion verbunden.

Fallbeispiele

Der Code aus Beispiel 1 (siehe Kasten »Beispiel 1: Überprüfung auf Variablen-Interdependenz«) zeigt die Verwendung der lokalen Variablen i, die am Ende der Funktion inkrementiert wird. Allerdings wird i an diesem Punkt undefiniert sein, wenn keine Beziehung zwischen cmd und rtn besteht, sodass rtn immer gleich Null ist, wenn cmd einen Wert von 2 besitzt.

Die Datenflussanalyse kann ermitteln, dass diese Funktion auf dieser angenommenen Beziehung beruht. Die Schleifenmodellierung ist ein wichtiger Teil der Semantik-Eingabedaten für eine Datenfluss-analyse. Anfangs- und Endwerte der Schleifensteuerungsvariablen werden verfolgt. Gleichzeitig wird ermittelt, ob Probleme nur bei Zwischenwerten auftreten.

Beispiel 2 (siehe Kasten »Beispiel 2: Überprüfung der Schleifenbedingungen«) zeigt diese Logik im Einsatz. In der Schleife werden zwei Probleme erkannt. In der zweiten Iteration tritt eine Teilung durch Null auf, und in der letzten Iteration wird ein ungültiger Array-Index berechnet. Beide Fehler stammen aus Codeabschnitten, bei denen es um die Schleifensteuerungsvariable geht.

Invariante Logik profitiert

Auch invariante Logik profitiert von einer genaueren Modellierung der Bestandteile eines bedingten Ausdrucks. In Beispiel 3 (siehe Kasten »Beispiel 3: Komplexer invarianter und nicht erreichbarer Code«) bestimmt die Variablenmodellierung in der ersten bedingten Verzweigung einen eingeschränkten Satz von Werten für Variable a.

Unter Berücksichtigung dieses Werte-Subsets ergibt die Untersuchung einen Satz von invarianten Codeverzweigungen. Diese enthalten einen Zweig, in dem der Wert immer wahr ist, und einen anderen Zweig mit nicht erreichbarem Code. In der Datenflussanalyse werden Zeiger (Pointer) genauso wie andere Variablen modelliert. Dabei navigiert man durch den CFG einer Funktion, um wichtige Details über ihren Status zu erhalten.

Ein zusätzlicher Satz von Modellattributen für Zeiger berücksichtigt den Typ und die Grenzen des Objekts, auf das er bezogen ist, sowie den aktuellen Offset innerhalb dieses Objektes. Anhand dieser Attribute lässt sich ermitteln, ob zwei Zeiger auf das gleiche Objekt bezogen sind, wenn die Pointer-Arithmetik einen ungültigen Zeiger erzeugt hat oder wenn ein Versuch gemacht wurde, eine Adresse außerhalb der Grenzen eines Objekts/Arrays zu dereferenzieren.

Das Beispiel 4 (siehe Kasten »Beispiel 4: Ungültige Zeiger-Dereferenzierung«)  zeigt einen Pointer, der von einem zugewiesenen Block zurückgeliefert wird, der irrtümlich über das Ende des Blocks hinaus dereferenziert wurde. Diese leistungsfähige Dataflow-Analyselösung bietet noch viele weitere Fähigkeiten. Verschach-telte Schleifen und Schleifen mit nicht zusammenhängenden Inkrementierungswerten lassen sich ebenfalls verarbeiten.

Die einzelnen Bits in einem skalaren oder zusammengesetzten Typ lassen sich nachverfolgen, was ein »intelligentes« Vorgehen bei Unionen und Bitfeld-Operationen ermöglicht. Die Modellierungsumgebung nutzt ein bidirektionales Konzept, indem zum Beispiel nachfolgende, bedingte Tests einen vorhergehenden, fraglichen Variableneinsatz nachweisen können.

Über den Autor:

Fergus Bolger ist Chief Technology Officer bei PRQA Programming Research.