CWI dicht bug in programmeertaal Java

Onderzoekers van het Centrum Wiskunde & informatica (CWI) hebben in februari 2015 een bug verholpen 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.
CWI dicht bug in programmeertaal JavaOnderzoeker Stijn de Gouw van de CWI-onderzoeksgroep Formal Methods wilde de correctheid van TimSort bewijzen en stuitte hierbij op de fout. Deze kan een gevaar 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 is populair

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. Functies om data te sorteren kunnen uit de library support worden gehaald en hoeven dus niet zelf te worden verzonnen.
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. Eerder was al wel een fix voor de bug voorgesteld, maar De Gouw ontdekte dat deze niet goed was. Hierdoor kunnen programma’s crashen zodra een grote invoer op een bepaalde manier is gesorteerd.

KeY

Om de mechanische correctheid van TimSort te bewijzen heeft Stijn de Gouw KeY ingezet. 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 hier te vinden.

Geef een reactie

Het e-mailadres wordt niet gepubliceerd. Vereiste velden zijn gemarkeerd met *