Onderzoekers van het Centrum Wiskunde & informatica (CWI) hebben in februari 2015 een bug gefixt in de veelgebruikte objectgerichte programmeertaal Java. Het gaat om een fout in een veel toegepast sorteeralgoritme, TimSort, waardoor programma’s konden crashen. De fout was al in 2013 bekend maar nog nooit goed opgelost. Toen onderzoeker Stijn de Gouw van de CWI-onderzoeksgroep Formal Methods de correctheid van TimSort wilde bewijzen, stuitte hij op de fout, die een gevaar kan zijn voor de security. Hij diende een bug report in met een verbeterde versie. Dat rapport is inmiddels geaccepteerd. Deze versie van TimSort wordt gebruikt door Android.
Java wordt onder meer gebruikt voor serversoftware, internet-gebaseerde bankdiensten en bijvoorbeeld in computerspellen als Minecraft. De programmeertaal wordt zo vaak gebruikt, omdat het veel support biedt in de vorm van libraries. Zo hoef je niet zelf een functie te verzinnen om data te sorteren; die kun je uit de library support halen. Het sorteeralgoritme TimSort is onderdeel van de java.util.Arrays en java.util.Collections libraries. Het is genoemd naar de maker, Tim Peters, die het in 2002 ontwierp voor de programmeertaal Python, waar het nu het standaard sorteeralgoritme is. De sorteerfunctie wordt vaak gebruikt, bijvoorbeeld bij de analyse van data. De Gouw ontdekte dat een eerder voorgestelde fix van de fout niet goed was. Hierdoor kunnen programma’s crashen bij een grote invoer die op een bepaalde manier is gesorteerd.
Voor zijn onderzoek gebruikte Stijn de Gouw KeY , een state-of-the-art open source verificatietool, om de mechanische correctheid te bewijzen van TimSort. Daarna ontwierp hij een correctie, met behoud van performance. Frank de Boer, groepsleider van de Formal Methods groep zegt: “Het was een van de zwaarste bewijzen die tot nu toe zijn uitgevoerd om de correctheid van een bestaande Java-library aan te tonen: het had ruim twee miljoen bewijsregels en duizenden handmatige stappen nodig.” Hij voegt toe: “Bij zo’n belangrijke taal als Java is het cruciaal dat software niet crasht Dit resultaat geeft goed het belang aan van formele methoden voor de maatschappij.” Het onderzoek werd mede-gefinancierd door het EU-project Envisage. Software is een van de speerpunten van het CWI in Amsterdam, waar het onderzoek is uitgevoerd.
De volledige analyse is te vinden op http://www.envisage-project.eu/timsort-specification-and-verification/ .
Meer informatie
- het bug report, 'TimSort fails with ArrayIndexOutOfBoundsException on worst case long arrays'
- het EU-project Envisage
- de CWI Formal Methods groep
- de gebruikte verificatietool KeY van Richard Bubel en Reiner Hähnle
Update
- Een Envisage blogpost over dit onderwerp werd op 24 februari gepubliceerd. De eerste dag waren er meteen 70.000 hits.
- Google programmeertaal Go maakt ook gebruik van TimSort
- toponderzoekers in Formele Methoden en developers wereldwijd refereren aan dit onderzoek, zoals Moshe Vardi en Peter O’Hearn.
