Splint liest C-Quellcode und findet typische Programmierfehler, das klappt ohne Änderung am Code. Mit etwas Zusatzaufwand ist aber noch mehr drin: In speziellen Kommentaren beschreibt der Entwickler sein Programm, damit ihn Splint besser versteht und noch mehr schmutzige Codestellen entdeckt.
Ohne Änderungen am Programmcode und ohne Flags beeindruckt der statische Semantikprüfer Splint[1] mit seinem detektivischen Spürsinn beim Finden von Fehlern. Ein Artikel in der letzten Ausgabe[2] beschrieb bereits, was Splint aus dem Stand beherrscht. Programmierer können das Tool aber noch wirksamer einsetzen, wenn sie ihr Programm mit speziellen Code-Kommentaren ergänzen. Die Kommentare erlauben es Splint, den Sourcecode besser zu verstehen. Der Prüfer ist dann in der Lage, noch eine ganze Reihe weiterer Probleme zu analysieren. Dazu gehören unter anderem:
Vor einfachen Problemen warnt bereits der C-Compiler. Je komplexer die Fallen sind, in die der Programmierer tappt, desto mehr Aufwand müssen Tools treiben, um die Fehler zu entdecken. Abbildung 1 stellt Ertrag und Nutzen dieser Werkzeuge gegenüber: Werkzeuge zur formalen Verifikation finden zwar die meisten Fehler, dazu ist jedoch ein beträchtlicher Aufwand nötig. Mit Splint bleibt der Aufwand gering, das Tool findet dennoch sehr viele Bugs.
Das Splint-Kommando kennt eine Reihe von Optionen und Parametern. Die Syntax lautet:
splint Flags -f Dateiname Programm
Dabei ist » Flags« eine Liste von Schaltern, die mehrere Arten der Überprüfung aktivieren oder deaktivieren.
Anders als bei den meisten Unix-Programmen deaktiviert ein Minuszeichen »-« die jeweilige Option, ein Pluszeichen »+« aktiviert sie. Zusätzlich gibt es Abkürzungen sowie Prüfstufen, die eine ganze Reihe von Flags gleichzeitig betreffen. Splint unterscheidet vier Stufen, auf denen es immer strengere Prüfkriterien anwendet: »-weak«, »-standard« (Default), »-checks« und »-strict« (siehe Kasten "Splint-Prüfstufen").
Falls die Datei »~/.splintrc« existiert und lesbar ist, übernimmt Splint die Standardeinstellungen der Flags aus diesem File. Mit »-f Dateiname« kann man auch eine andere Datei verwenden. Folgender Aufruf überprüft das Programm »Beispiel1.c« aus Listing 1:
splint -checks +boundswrite -exportheader Beispiel1.c
Mit diesen Parametern benutzt Splint die Prüfstufe »checks«, und zwar ohne die Prüfung »exportheader«, aber mit aktiviertem »boundswrite«.
Splint bezieht sein Wissen über den Sinn einzelner Codestellen nur aus dem vorliegenden Quellcode. Bei auffälligen Details kann Splint daher nicht wissen, was der Programmierer damit beabsichtigt oder ob es schlicht ein Fehler ist. Dies Hintergrundwissen kann der Programmautor in spezielle Kommentare packen und damit an Splint weitergeben.
Listing 1 enthält solche Kommentare: Die Main-Funktion in Zeile 3 nimmt eine Liste von Argumenten entgegen, die sie aber nie benutzt. Der Code-Kommentar »/*@unused@*/« verhindert, dass Splint eine Fehlermeldung ausgibt: Dem Programmautor ist bewusst, dass er die Variablen nicht verwendet, er setzt sie aber absichtlich ein. Solche Code-Kommentare beginnen immer mit »/*@« und enden mit »@*/«. Folgendes Kommando gibt eine Liste der möglichen Kommentare aus:
splint -help annotations
Ein verbreitetes Problem beim Entwickeln von Software sind ungültige Zeiger. Sie verursachen die Hälfte aller Fehler. Auch bei Bugs dieser Art hilft Splint. In Listing 1 hat sich ein kleiner, aber sehr unangenehmer Fehler eingeschlichen: Zeile 9 gibt Speicher frei, der einen String enthält. Zeile 10 versucht, genau diesen String auszugeben.
Im vorliegenden Beispiel ist das unkritisch und leicht zu bemerken, in realen Programmen können zwischen dem Freigeben des Speicherbereichs und dem verbotenen Zugriff aber Hunderte von Programmzeilen liegen. Während diese bearbeitet werden, könnte der Speicher beliebige andere Daten erhalten haben oder außerhalb des gültigen Adressbereichs liegen. Splint reagiert mit der folgenden Warnung:
Beispiel1.c:10:26: Variable dpointer used after being released
Schwieriger wird die Sache, wenn Speicheranforderung und -freigabe nicht im Hauptprogramm, sondern in Funktionen erfolgen. Das Programm in Listing 2 fordert in der Routine »allocmem()« Speicher an. Es erwartet in »get_data()« vom Benutzer eine String-Eingabe und kehrt diesen Text in »reverse_data()« um. Dann gibt es den String aus und den Speicher in »deallocmem()« wieder frei. In der vorliegenden Form führt das Programm unter anderem zu folgender Splint-Fehlermeldung:
linttest.c:70:8: Implicitly temp storage char_p passed as only param: free (char_p)
Splint meint, dass angeforderter Speicher nicht freigegeben wurde. Die Fehlermeldung verschwindet, wenn man den Code-Kommentar »/*@only@*/« direkt vor »char*« in Zeile 11 einfügt. Der Semantikprüfer weiß jetzt, dass es sich um eine exklusive Referenz handelt. Das bedeutet: Dieser Zeiger ist verpflichtet, den Speicherplatz, auf den er zeigt, wieder freizugeben. Die Verpflichtung kann er auf drei Arten an andere Zeiger übertragen:
Nachdem er seine Verpflichtung auf einen anderen Zeiger übertragen hat, gilt der ursprüngliche Pointer als toter Zeiger, der nicht mehr verwendet werden darf. Dadurch kann Splint gewährleisten, dass das Programm einmal angeforderten Speicher wieder freigibt, und zwar genau ein Mal. Damit das alles richtig funktioniert, muss die Verpflichtung zur Speicherfreigabe einmal entstehen. Das passiert in den Routinen, die Speicher reservieren, etwa »malloc()« oder »calloc()«.
Splint bringt eigene Versionen der Header für Standardbibliotheken mit. Diese enthalten bereits Code-Kommentare, die Splint beim Überprüfen eines Programms automatisch verwendet. Die »malloc()«-Funktion sieht dort so aus:
/*@only@*/ /*@null@*/ void *malloc(size_t size);
Der Rückgabewert ist ein Zeiger, der auf einen Speicherbereich zeigt, den der Aufrufer wieder freigeben muss (»only«). Der Zeiger kann eventuell null sein. Durch einen Blick in die mit Splint gelieferten Header »standard.h« und »posix .h« kann man eine Menge über die Code-Kommentare lernen.
| Splint-Prüfstufen |
|---|
| Weak: Schwache Prüfung für typische, unkommentierte Programme. In dieser Stufe entdeckt Splint keine Modifies (Seiteneffekte durch verborgene Wertänderungen) und prüft keine Makros. Der Aufrufer einer Funktion darf deren Rückgabewert ignorieren. Die Typen »bool«, »int«, »char« und benutzerdefinierte »enum«-Typen sind gleichwertig. Standard: In dieser Prüfstufe untersucht Splint zusätzlich zu den Prüfungen der Weak-Stufe, ob das Programm bereits freigegebenen Speicher nutzt, Null-Zeiger dereferenziert, unerreichbaren Code oder Endlosschleifen enthält und die Rückgabewerte von Funktionen auswertet. Zudem kontrolliert diese Stufe, ob die Makros in Ordnung sind und die Funktionen alle Parameter verwenden. Für Splint sind die Typen »bool«, »int« und »char« unterschiedlich, sie dürfen nicht (ohne explizite Typumwandlung) gemischt werden. Checks: Diese schärfere Prüfung stellt zusätzlich sicher, dass sich alle Funktionen an ihre genaue Schnittstellenbeschreibung halten. In dieser Stufe gelten auch »enum« und »int« als unterschiedliche Typen. Strict: Die schärfste Prüfstufe ist für reale Programme nur bedingt zu empfehlen. Die Manpage verspricht daher dem Ersten, der ein reales Programm schreibt, das diese Stufe ohne Warnungen meistert, eine Belohnung. |
|
Listing 1: |
|---|
01 #include <stdlib.h>
02
03 int main(/*@unused@*/ int argc, /*@unused@*/ char **argv)
04 {
05 char* dpointer=NULL;
06 dpointer = (char*)calloc((size_t)20, (size_t)1);
07 if (dpointer==NULL) return 1;
08 strcpy (dpointer, "Hello World");
09 free (dpointer);
10 printf("Ausgabe: %sn", dpointer); /* dpointer zeigt ins Nirwana */
11 return 0;
12 }
|
Alle Rezensionen aus dem Linux-Magazin
Im Insecurity Bulletin widmet sich Mark Vogelsberger aktuellen Sicherheitslücken sowie Hintergründen und Security-Grundlagen. mehr...
