---

“Don't Miss the End: Preventing Unsafe End-of-File Comparisons” by C.Z. Chen and W. Dietl. In NASA Formal Methods, 2018, pp. 87-94.

Abstract

Reading from an InputStream or Reader in Java either returns the read byte/character or -1 if the end-of-file (EOF) has been reached. To support the additional -1 as return value, the read methods return an int. For correct usage, the return value should be compared to -1 before being converted to byte or char. If the conversion was performed before the comparison, it can cause a read-until-EOF-loop to either exit prematurely or be stuck in an infinite loop. The SEI CERT Oracle Coding Standard for Java rule FIO08-J “Distinguish between characters or bytes read from a stream and -1” describes this issue in detail. This paper presents a type system that prevents unsafe EOF value comparisons statically and is implemented for Java using the Checker Framework. In an evaluation of 35 projects (9 million LOC) it detected 3 defects in production software, 8 bad coding practices, and no false positives. The overall annotation effort is very low. Overrides for the read methods needed to be annotated, requiring a total of 44 annotations. Additionally, 3 annotations for fields and method parameters needed to be added. To the best of our knowledge this is the first open source tool to prevent this security issue.

BibTeX entry:

@inproceedings{ChenDietl18,
   author = {C.Z. Chen and W. Dietl},
   title = {Don't Miss the End: Preventing Unsafe End-of-File Comparisons},
   booktitle = {NASA Formal Methods},
}

---

---