Google award for discovering bug in Java library

Almost all software makes use of a so-called ‘standard library’, which is considered an essential part of a programming language. It contains reusable software components which allow for interoperability between other components produced by many different authors and third-parties. Hiep: “Since standard libraries are used by so many applications, it is of utmost importance that the software does not contain programming errors. Such errors could potentially lead to unwanted behaviour, which is possibly difficult to detect, and may be exploited by malicious parties and escalated to serious security issues.”

One part of Java’s standard library is called the Java Collection Framework (JCF) and contains code used for structuring data in the computer’s working memory. It defines structures for keeping data in lists and tables, and contains algorithms for efficient retrieval of such structured data and operations on them.

Hiep continues: “Earlier, our research group discovered another issue, namely a bug in the sorting algorithm part of the Java Collection Framework. Now, we found another bug in the so-called linked list data structure.” The linked list is a well-known data structure that is often taught in undergraduate, bachelor computer science programs. Hiep: “It was very surprising to us that operations on such a well-known data structure turned out to be programmed incorrectly, even though it is part of a widely-used library and its source code is open source.”

Hiep: “We found the bug while we were trying to prove that the linked list source code had no flaws. However, we were unable to do so because we found this overflow issue.” An overflow issue is a low-level problem on digital computers that store integer numbers in a memory register of a particular bounded size. Hiep: “Compare it with the odometer of an old car. Once you reached, say, 99.999 km it rolled all the way back to 0 km. Something similar happens within a computer when an integer overflow happens. And that overflow may lead to unexpected outcomes.”

Hiep found out that the flawed linked list was used in security-sensitive parts of Java, such as its secure socket implementation. Secure sockets are used in many Internet protocols that guarantee secure communication, such as HTTPS, FTPS and SSH. After the issue was shared with Java developers, the secure socket implementation was updated to no longer use the flawed linked list."

Many years ago, the overflow bug in the Java Collection Framework was not an issue. Hiep: “Back in the days when we had 32-bit machines, the bug could not be triggered because there was simply not enough memory to do so. However, on more recent 64-bit machines it becomes possible to trigger the bug: this is an issue on machines that process big data and thus have a lot of memory available, such as Google’s cloud platform.”

Hiep continues: “It seems that this bug was dormant for quite some time. Even without a change in the source code, the bug slowly became relevant by the uptake of the 64-bit architecture and the increase of available memory: there was nothing spontaneous going on here. We have discovered the issue and have shown how to reproduce, and eliminate, the bug. Otherwise, these kinds of dormant and undiscovered bugs could become the root cause of tomorrow’s zero-day exploits (vulnerabilities earlier known to hackers than to the software makers). In our case, from start to finish, this bug was already present for two decades in the standard library source code!”

Hiep: “We will not stop here. Recently, one of my students also found an overflow issue in yet another part of the Java Collection Framework (BitSet), while he was analyzing its source code also by using formal methods. It now seems to me: no matter where we look, we shall find bugs!”

Many important and societal-relevant applications depend on Java and the correct functioning of the standard library. Hiep: “For example, the Dutch tax authority has a lot of code written in the Java programming language, in software to make sure everyone pays their taxes. Also the Dutch election software, used at the end of an election day for summing votes and computing the final election results, is written in Java. A small programming error can have potentially very significant consequences. Our group wants to continue developing formal reasoning techniques that allow us to precisely analyze the correctness of these important but large pieces of software. Although very challenging, our work is not only purely of theoretical interest, but also produces practical results such as discovering bugs in real software. I am very glad and honoured that Google does recognize the importance of our work.”