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

Tuesday, August 8, 2023 3:00 pm - 4:00 pm EDT (GMT -04:00)

Candidate: Alex Liu

Date: August 8, 2023

Time: 3:00 pm

Location: EIT 3145

Supervisor(s): Werner Dietl

Abstract

Java cryptographic APIs facilitate building secure applications, but not all developers have sufficient cryptographic knowledge to use those APIs correctly. Several studies have shown that misuses of those cryptographic APIs may cause significant security vulnerabilities. Hence, it is an important problem to design methodologies and techniques, which can guide developers to build secure applications with minimum effort and are accessible to non-experts in cryptography. In this thesis, we present a methodology that reasons about the correct usage of Java cryptographic APIs in types, specifically targeted 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 uses of cryptographic APIs and invariants on variable usage. Moreover, 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 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 the 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. 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.