Ensuring correct cryptographic algorithm and provider usage at compile time
Using cryptographic APIs to encrypt and decrypt data, calculate digital signatures, or compute hashes is error prone. Weak or un- supported 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. We present 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 Crypto Checker is 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.
Tue 13 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
| 16:50 - 18:50 | |||
| 16:5030m Talk | IntelliJML: A JML plugin for IntelliJ IDEA FTfJP P: Steven Monteiro University of Twente, P: Erikas Sokolovas University of Twente, The Netherlands, P: Ellen Wittingen University of Twente, Tom van Dijk University of Twente, Marieke Huisman University of TwenteFile Attached | ||
| 17:2030m Talk | Ensuring correct cryptographic algorithm and provider usage at compile time FTfJP P: Weitian Xing University of Waterloo, Yuanhui Cheng University of Waterloo, Werner Dietl University of WaterlooMedia Attached | ||
| 17:5030m Talk | Behavioural Separation with Parallel Usages FTfJP Iaroslav Golovanov Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, P: Mathias Steen Jakobsen Department of Computer Science, Aalborg University, Denmark, Mikkel Klinke Kettunen Department of Computer Science, Aalborg University, Denmark | ||
| 18:2030m Talk | Combining Formal and Machine Learning Techniques for the Generation of JML Specifications FTfJPDOI File Attached | ||
| 18:5030m Talk | JML and OpenJML for Java 16 FTfJPFile Attached | ||
