A Lightweight Type System with Uniqueness and Typestates for the Java Cryptography API

Abstract

Java cryptographic APIs facilitate building secure applications, but not all developers have strong cryptographic knowledge to use these APIs correctly. Several studies have shown that misuses of those cryptographic APIs may cause significant security vulnerabilities, compromising the integrity of applications and exposing sensitive data. Hence, it is an important problem to design methodologies and techniques, which can guide developers in building secure applications with minimum effort, and that are accessible to non-experts in cryptography. In this thesis, we present a methodology that reasons about the correct usage of Java cryptographic APIs with types, specifically targeting to cryptographic applications. Our type system combines aliasing control and the abstraction of object states into typestates, allowing users to express a set of user-defined disciplines on the use of cryptographic APIs and invariants on variable usage. More specifically, we employ the typestate automaton to depict typestates within our type system, and we control aliases by applying the principle of uniqueness to sensitive data.

We mainly focus on the usage of initialization vectors. An initialization vector is a binary vector used as the input to initialize the state for the encryption of a plaintext block sequence. Randomization and uniqueness are crucial to an initialization vector. Failing to maintain a unique initialization vector for encryption can compromise confidentiality. Encrypting the same plaintext with the same initialization vector always yields the same ciphertext, thereby simplifying the attacker's task of guessing the cipher pattern.

To address this problem practically, we implement our approach as a pluggable type system on top of the EISOP Checker Framework. To minimize the cryptographic expertise required by application developers looking to incorporate secure computing concepts into their software, our approach allows cryptographic experts to plug in the protocols into the system. In this setting, developers merely need to provide minimal annotations on sensitive data—requiring little cryptographic knowledge.

We also evaluated our work by performing experiments over one benchmark and 7 real-world Java projects from Github. We found that 6 out 7 projects have security issues. In summary, we found 12 misuses in initialization vectors.