Side Channel FinderAVR (SCFAVR)

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 FinderAVR 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 FinderAVR 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 FinderAVR reports success. If the program is not typeable, Side-Channel FinderAVR 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 FinderAVR 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 FinderAVR does not contain timing-side-channel vulnerabilities.

Case Study

Side-Channel FinderAVR 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 FinderAVR 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 FinderAVR 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 FinderAVR after analyzing the second, non-vulnerable implementation. The tool reports a successful verification.

Source Code

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

 SCFAVR

 

AVR-Semantics, Type System, and Soundness Proof

The full formalization of the type system underlying Side-Channel FinderAVR, 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 ]



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