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 er veel ondersteuning is 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/ .
– 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
'Kritieke grondstoffen' in grote hoeveelheden nodig hebben in Europa - maar we halen ze uit…
Helen Kardan is TNO's nieuwe Director Science & Technology voor de High Tech Industry unit.…
Control Techniques en KB Electronics vormen sinds 1 mei 2024 Nidec Drives. Control Techniques en…
Hitma Groep heeft KS Perslucht overgenomen. Het in Haarlem gevestigde bedrijf sluit met zijn productassortiment en…
De Duitse fabrikant van houten windturbinebladen Voodin Blade Technology heeft 's werelds eerste prototype-installatie aangekondigd…
FME en Orgalim (de Europese koepel van de technologische industrie) pleiten voor het centraal stellen…