Kort nieuws

CWI fikst Java-bug met formele methoden

Nieke Roos
Leestijd: 2 minuten

Onderzoekers van het Centrum Wiskunde & informatica (CWI) in Amsterdam hebben in februari een bug gefikst in Java. Het gaat om een fout in het sorteeralgoritme Timsort, waardoor programma’s konden crashen. De bug was al in 2013 bekend maar nog nooit goed opgelost. Toen onderzoeker Stijn de Gouw van de CWI-groep Formal Methods de correctheid van Timsort wilde bewijzen, stuitte hij op de fout, die een gevaar kan zijn voor de security. De bugrapportage met een verbeterde versie die hij indiende, is inmiddels geaccepteerd. Deze versie wordt gebruikt door Android.

Timsort is onderdeel van de library’s java.util.Arrays en java.util.Collections. Het is genoemd naar de maker, Tim Peters, die het in 2002 ontwierp voor Python, waar het nu het standaard sorteeralgoritme is. De functie 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.

Om de mechanische correctheid van Timsort te bewijzen, gebruikte De Gouw Key, een state-of-the-art open-source verificatietool. Daarna ontwierp hij een correctie, met behoud van performance. ‘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’, aldus Frank de Boer, leider van de Formal Methods-groep.

This article is exclusively available to premium members of Bits&Chips. Already a premium member? Please log in. Not yet a premium member? Become one and enjoy all the benefits.

Login

Related content