Conference Papers: Checking Applications using Security APIs with JOANA

JOANA is a tool for software security analysis, checking up to 100kLOC of full multithreaded Java. JOANA is based on sophisticated program analysis techniques and very precise. JOANA includes a new algorithm guaranteeing probabilistic noninterference, named RLSOD. JOANA needs few annotations, is open source, and was applied in several case studies. The current extended abstract discusses the analysis of security APIs using JOANA. In particular, we practically demonstrate a method which guarantees that code using a cryptographic API does not contain confidentiality leaks. The method is backed by a theorem from Küsters.