ESC/Java2 as a Tool to Ensure Security in the Source Code of Java Applications
Aleksy Schubert, Jacek Chrza̧szcz · 2007
The paper shows how extended static checking tools like ESC/Java2 can be used to ensure source code security properties of Java applications. It is demonstrated in a case study on a simple personal password manager. In case of such an application the ensuring of security is one of the most important goals. We present the possible threats connected with the current state of the code and its possible future extensions. This investigation is further accompanied by a presentation on how these threats can be controlled by JML specifications and ESC/Java2.