Fehler in Standardsortieralgorithmus mit formalen Methoden aufgedeckt
Android, Java und Groovy nutzen alle den TimSort-Algorithmus. Informatiker eines Verbundprojekts konnten mit Hilfe eines von ihnen entwickelten Tools nun einen Fehler in der Implementierung feststellen und beheben.
- Julia Schmidt
Die Mitglieder eines EU-Verbundprojekts sind beim Testen ihrer Verifikationssoftware KeY auf einen für beseitigt gehaltenen Fehler im Sortieralgorithmus TimSort gestoßen. Letzterer kommt unter anderem als Standardmechanismus für Sortieraufgaben im Android SDK, in Suns JDK und OpenJDK zum Einsatz. Die nun behobene Schwachstelle ließ sich wohl theoretisch für Denial-of-Service-Angriffe nutzen, auch wenn die Projektmitarbeiter die akute Bedrohung für gering halten.
Der 2002 von Tim Peters entwickelte Sortieralgorithmus TimSort vereint Ideen aus den Verfahren Merge Sort und Insertion Sort. Er geht den eingegebenen Array von links nach rechts durch und sortiert ihn, indem er aufeinander folgende, disjunkte bereits sortierte Abschnitte aufzufinden versucht, absteigend sortierte Abschnitte umdreht und die Längen der Abschnitte mit einer minimalen Abschnittslänge vergleicht und bei Bedarf auffüllt (nähere Informationen zur Funktionsweise finden sich in der Beschreibung der ersten Implementierung für Python). Die Längen der Abschnitte addiert der Algorithmus und schreibt sie in einen Array runLen.
Nach jedem dieser Schreibvorgänge wird eine Methode mergeCollapse gestartet, die Abschnitte zusammenführt, bis die letzten drei Elemente in runLen zwei festgelegte Bedingungen erfüllen. Diese Bedingungen geben zusammen eine Invariante. Die Informatiker des Envisage-Projekts konnten nun mit formalen Methoden feststellen, dass die mergeCollapse-Methode in bestimmten Fällen gegen die Invariante verstößt und haben eine Korrektur eingereicht, die für das OpenJDK angenommen wurde. Eine genaue Beschreibung der Schwachstelle und der formalen Spezifikation der Gegenmaßnahme sind in einem ausfürhlichen Blogbeitrag beschrieben.
Die zur Verifikation benutzte KeY-Software des Verbundprojekts, an dem unter anderem das Karlsruhe Institut für Technologie und die Technische Universität Darmstadt beteiligt sind, steht interessierten Entwicklern auf der Projektseite zum Download zur Verfügung. Sie können es unter anderem dazu nutzen, um eigene Programme auf Fehler im Aufbau zu untersuchen. (jul)
