Candidate: Weitian Xing
Title: Light-weight verification of cryptographic API usage
Date: December 2, 2020
Time: 11:00 AM
Place: Remote
Supervisor(s): Dietl, Werner
Abstract:
A pluggable type system is a light-weight approach for compile-time program verification, which provides more powerful types to both developers and compilers. Developers use pluggable types to boost program understanding and enforce interesting properties, e.g., NullPointerExceptions freedom, while compilers leverage the new types to perform extra type checking, which gives more run time guarantees. This thesis presents a new type system, the Crypto Checker, to help developers prevent cryptographic APIs misuses. In addition, this thesis presents the Property File Handler and the Network Request Checker as two effect systems. The Property File Handler performs type refinement to Java Properties by reading property files at compile time, while the Network Request Checker reports all the possible network requests to prevent potential information leakage in Java and Android applications.
Using cryptographic APIs to encrypt and decrypt data, calculate digital signatures, or compute hashes is error prone. Weak or unsupported cryptographic algorithms can cause information leakage and runtime exceptions, such as a NoSuchAlgorithmException in Java. Using the wrong cryptographic service provider can also lead to unsupported cryptographic algorithms. Moreover, for Android developers who want to store their key material in the Android Keystore, misused cryptographic algorithms and providers make the key material unsafe. This thesis presents the Crypto Checker, a pluggable type system that detects the use of forbidden algorithms and providers at compile time. For typechecked code, the Crypto Checker guarantees that only trusted algorithms and providers are used, and thereby ensures that the cryptographic APIs never cause runtime exceptions or use weak algorithms or providers. The type system consists of an easy-to-understand type qualifier hierarchy. The Crypto Checker is flexible and easy-to-use---it allows developers to determine which algorithms and providers are permitted by writing specifications using type qualifiers. We implemented the Crypto Checker for Java and evaluated it with 32 open-source Java applications (over 2 million LOC). We found 2 issues that cause runtime exceptions and 62 violations of security recommendations and best practices. We also used the Crypto Checker to analyze 65 examples from a public benchmark of hard security issues and discuss the differences between our approach and a different static analysis in detail.
Malicious or unsafe applications collect and send users' data to untrusted external servers via network requests, e.g., HTTP and socket requests, which will cause information leakage. Detecting the possible network requests on the source code level without running the applications is a light-weight approach to solve the problem. Application stores that have the source code of the uploaded apps can take advantage of this to ensure application security. Security teams in companies also use similar technologies to guarantee compliance. This thesis presents the Network Request Checker, an effect system for Java to detect and report all the possible network requests to developers at compile time. The Network Request Checker can be integrated into any other pluggable type system or be seen as a stand-alone type system depending on developers' needs. We evaluated this type system with 6 real-world Java and Android applications and discuss the experimental results.
To improve the Crypto Checker, the Network Request Checker, and the other type systems' precision, i.e., to obtain more valuable information from the program at compile time, this thesis presents the Property File Handler, a type system extension that reads property files to perform type refinement on Java Properties. When the applications read property files, the Property File Handler will also try to load, store, and propagate the information from property files. A simple type hierarchy is proposed to achieve this functionality. By using the Property File Handler, we fixed a potential false negative found in SonarSource.