Checker Framework: Vulnerability Debugging

This project focused on identifying and mitigating a logic based vulnerability involving negative time values in Java (via Checker Framework). The issue explored was that a value’s syntax could be valid and unit correct, while actually being logically unsafe. For example, a value such as -5 seconds may satisfy a unit annotation, but in real deployments it could produce incorrect business logic.

The project used Java, Gradle and the Checker Framework, with development carried out in Visual Studio Code on Windows. I investigated how the Checker Framework Units Checker validates unit correctness, then extended the application logic to detect invalid negative time values. The final implementation lead me to create GoodTime.java to enforce validation and BadTime.java to demonstrate invalid behaviour, showing the difference between technical unit correctness and meaningful secure input handling.

The vulnerability is relevant in sectors such as banking or finance. If a system calculates interest, transaction timings, refunds or audit records using a negative time value, it could create inaccurate calculations and unreliable records. My mitigation prevented this invalid value from being silently accepted.

A major part of the work involved debugging Checker Framework integration issues, including Gradle configuration, annotation processor errors, dependency management, classpath issues, Java compilation failures, constructor validation logic and field initialisation problems. I initially explored creating a custom checker before moving towards a more practical solution that extended the semantics of the existing Units Checker through application level validation.

Project Details

Name: Checker Framework: Vulnerability Debugging
Author:
Date: December 10, 2025
Categories: Checker Framework, Java
Get in touch with me
Please fill out the form below to start chatting with me directly.