Bug in Java gefixt met formele methoden CWI
Amsterdam, 20150225 -- 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 hoeven developers bijvoorbeeld niet zelf een functie te verzinnen om data te sorteren; die kunnen ze 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 Centrum Wiskunde & Informatica (CWI) in Amsterdam, waar het onderzoek is uitgevoerd.
De volledige analyse is te vinden op http://www.envisage-project.eu/timsort-specification-and-verification/.
Op 24 februari werd door CWI-onderzoeker Stijn de Gouw een blogpost gepubliceerd op de site van EU-project Envisage, dat de eerste dag al tienduizenden keren is bekeken: http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
Over het Centrum Wiskunde & Informatica
Het Centrum Wiskunde & Informatica (CWI) is sinds 1946 het nationale onderzoeksinstituut voor wiskunde en informatica. Het is gevestigd op het Amsterdam Science Park en is deel van de Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO). Het instituut heeft een sterke internationale positie. Ruim 150 wetenschappers doen er grensverleggend onderzoek en dragen de verkregen kennis over aan de maatschappij. Meer dan 30 van de onderzoekers zijn hoogleraar aan een universiteit. Het instituut heeft 22 spin-off bedrijven voortgebracht.
Centrum Wiskunde & Informatica