SPASCA: Secure-Programming Assistant and Side-Channel Analyzer

Information leakage in computer systems can be clustered in different classes based on how the information is leaked. Two examples of such classes are information leakage through data content and information leakage through execution time. The Secure-Programming Assistant and Side-Channel Analyzer (SPASCA) is an information-flow analysis tool for Java programs at the source-code level. SPASCA can be used to detect information leakage in programs written in a rich sequential Java subset. It implements two static type-based information-flow analyses: a timing-insensitive analysis detecting only leakage through data content, and a timing-sensitive analysis that builds on the former and additionally detects information leakage through execution time.


Overview

A static information-flow analysis for Java
SPASCA can be used to detect information leakage in programs written in a rich sequential subset of Java (with classes and sub-classes, methods, arrays, and expressions with side effects). SPASCA implements two static type-based information-flow analyses: a timing-insensitive analysis and a timing-sensitive analysis, detecting both information leakage through data content and information leakage through execution time. The two information-flow analyses are formalized as security type systems, a well-known lightweight technique for information-flow analysis. This technique often enables the automatic verification of the security of a program or the automatic detection of potential information leaks in a program.
Timing-Sensitive Type System
The timing-sensitive type system of SPASCA is based on a transcript model of time, where the transcript includes both, the program counter and the accesses to arrays. It has been applied to multiple crypto implementations. For instance, secret-dependent control flow and secret-dependent array accesses were detected in the GNU Classpath implementation of DES and the FlexiProvider implementations of AES and IDEA.
Eclipse IDE plug-in
SPASCA consists not only of an implementation of the two underlying security type systems but is also seamlessly integrated as plug-in for the Eclipse IDE. With this integration, SPASCA can be used to provide immediate feedback on potential information leaks during the development of security-critical software.

Example: Detecting a Timing Side Channel with SPASCA

The screenshot below shows how SPASCA can be used to detect a timing side channel in an implementation of modular exponentiation. The implementation of modular exponentiation is based on the square-and-multiply technique. It iterates over the exponent k and if the current bit of the exponent is set to 1, it multiplies the intermediate result with the base y. Afterwards, it squares the intermediate result. Since the multiplication happens only for the bits in the exponent that are set to 1, the execution time of the code depends on the number of set bits, i.e., on the Hamming weight, of the exponent.

In the example, the exponent k is marked as secret information with the annotation @High. That is, the dependence of the execution time on the exponent is a side-channel vulnerability because it reveals the Hamming weight of the secret exponent.
SPASCA detects this vulnerability and highlights it in Eclipse. It underlines the line of code that leads to the leakage and describes the reason (branching on high guards) in the summary of information flow problems.



Publications

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang