Side Channel Finder^AVR (SCF^AVR)

Timing-side-channel vulnerabilities are serious security threats at the level of implementations. An implementation is vulnerable to a timing side channel if its running time depends on secret information, like cryptographic keys. An attacker who observes the running time of a vulnerable implementation might be able to deduce the secret from his observations.

Side-Channel Finder^AVR can automatically detect timing-side-channel vulnerabilities in AVR assembly programs (programs running on AVR - popular processors for embedded devices and Internet of Things applications).

Overview of the Tool

Side-Channel Finder^AVR takes as input an AVR assembly program, together with a configuration that specifies a security policy. In a security policy, security levels are assigned to inputs and outputs of the AVR assembly program. These levels specify whether an input or output is considered secret or public.

The tool parses the program and the configuration, precomputes control dependence information of the program, and the applies a timing-sensitive security type system.

If the program is typeable with the timing-sensitive security type system, Side-Channel Finder^AVR reports success. If the program is not typeable, Side-Channel Finder^AVR reports a failure, i.e., a potential timing-side-channel vulnerability. A failure report contains the instruction at which the potential vulnerability is located and a description of the potential vulnerability (e.g., a loop whose iterations depend on secret information).

Example: Analysis Output of SCFAVR - Detection of a Timing-Side-Channel Vulnerability	Example: Analysis Output of SCFAVR - Successful verification of a Program without Timing-Side-Channel Leakage

Theory underlying the Tool

The security type system applied by Side-Channel Finder^AVR only allows to type programs (using security levels as types) if they satisfy a security propoerty called timing-sensitive noninterference. That is, the type system is sound with respect to the security property. The property itself is defined based on a formal operational semantics of AVR assembly. The semantics is faithful with respect to the timing behaviour specified in the official AVR instruction set manual. That is, a program that satisfies timing-sensitive noninterference is free from timing-side-channel vulnerabilities. Overall, an implementation that is successful verified with Side-Channel Finder^AVR does not contain timing-side-channel vulnerabilities.

Case Study

Side-Channel Finder^AVR has been applied to cryptographic implementations from the library muNaCl. More concretely, it has been applied to the implementations of Salsa20, xSalsa20, Poly1305, and string comparison. For these implementations, it was successfully verified that they contain no timing-side-channel vulnerabilities.

The following figure visualizes the application of Side-Channel Finder^AVR to two implementations of string comparison: one implementation that aborts the comparison as soon as the strings differ, and one implementation that always compares the entire strings. Both implementations are shown at the source-code level for better readability.

The first implementation, depicted on the upper left-hand side, contains a timing-side-channel vulnerability. More concretely, it leaks the index at which the strings (e.g., passwords) differ through its running time. The second implementation (from μNaCl), depicted in the lower left-hand side, contains no timing-side-channel vulnerability.

The upper right-hand side shows the output of Side-Channel Finder^AVR after analyzing the first (vulnerable) implementation. The tool reports a loop on secret data. The lower right-hand side shows the output of Side-Channel Finder^AVR after analyzing the second, non-vulnerable implementation. The tool reports a successful verification.

Source Code

The source code of Side-Channel Finder^AVR (including case studies) is available for download below.

 SCF^AVR

 

AVR-Semantics, Type System, and Soundness Proof

The full formalization of the type system underlying Side-Channel Finder^AVR, the full soundness proof, and the operational semantics on which it is based are available for download below.

Formalization and Proofs

Publications

Florian Dewald, Heiko Mantel and Alexandra Weber. AVR Processors as a Platform for Language-Based Security. In Proceedings of the 22nd European Symposium on Research in Computer Security (ESORICS), pages 427-445, 2017.
[ BibTeX entry | PDF ]

Florian Dewald, Heiko Mantel and Alexandra Weber. Poster: Side-Channel Finder for AVR. Poster at the 20th International Conference on Cryptographic Hardware and Embedded Systems (CHES), 2018.
[ BibTeX entry | PDF ]