[PWC-MEDIA] Persbericht CWI: Bug in Java gefixt met formele methoden CWI

  • From: Annette Kik <Annette.Kik@xxxxxx>
  • To: Stijn de Gouw <Stijn.de.Gouw@xxxxxx>, "Frank S.de Boer" <f.s.de.boer@xxxxxx>
  • Date: Mon, 23 Feb 2015 13:58:26 +0100 (CET)

Persbericht Centrum Wiskunde & Informatica (CWI)

Amsterdam, 23 februari 2015


Bug in Java gefixt met formele methoden CWI 

Onderzoekers van het Centrum Wiskunde & informatica (CWI) in Amsterdam 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), waar het onderzoek is 
uitgevoerd.

De volledige analyse is te vinden op 
http://www.envisage-project.eu/timsort-specification-and-verification/.

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.

---
Noot voor de pers (niet voor publicatie):
Meer informatie: onderzoeker Stijn de Gouw (CWI),e-mail  cdegouw@xxxxxx en 
prof. dr. Frank de Boer (CWI en UL), groepsleider van de CWI Formal Methods 
groep, e-mail F.S.de.Boer@xxxxxx. Het bug report: 
https://bugs.openjdk.java.net/browse/JDK-8072909; het EU-project Envisage: 
http://envisage-project.eu/; de CWI Formal Methods groep: 
https://www.cwi.nl/research-groups/Formal-Methods; de gebruikte verificatietool 
KeY: http://www.key-project.org. 

- Behandeld door: Annette Kik, Centrum Wiskunde & Informatica, 
Annette.Kik@xxxxxx, tel. 06-51574891 (ma, wo-och, vr-mi) of bgg 020-5924181. 
Centrum Wiskunde & Informatica, Science Park 123, 1098 XG Amsterdam, 
http://www.cwi.nl.


Other related posts:

  • » [PWC-MEDIA] Persbericht CWI: Bug in Java gefixt met formele methoden CWI - Annette Kik