International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Flavio D. Garcia

Publications

Year
Venue
Title
2021
TCHES
Cutting Through the Complexity of Reverse Engineering Embedded Devices
Performing security analysis of embedded devices is a challenging task. They present many difficulties not usually found when analyzing commodity systems: undocumented peripherals, esoteric instruction sets, and limited tool support. Thus, a significant amount of reverse engineering is almost always required to analyze such devices. In this paper, we present Incision, an architecture and operating-system agnostic reverse engineering framework. Incision tackles the problem of reducing the upfront effort to analyze complex end-user devices. It combines static and dynamic analyses in a feedback loop, enabling information from each to be used in tandem to improve our overall understanding of the firmware analyzed. We use Incision to analyze a variety of devices and firmware. Our evaluation spans firmware based on three RTOSes, an automotive ECU, and a 4G/LTE baseband. We demonstrate that Incision does not introduce significant complexity to the standard reverse engineering process and requires little manual effort to use. Moreover, its analyses produce correct results with high confidence and are robust across different OSes and ISAs.
2020
TCHES
Dismantling DST80-based Immobiliser Systems 📺
Car manufacturers deploy vehicle immobiliser systems in order to prevent car theft. However, in many cases the underlying cryptographic primitives used to authenticate a transponder are proprietary in nature and thus not open to public scrutiny. In this paper we publish the proprietary Texas Instruments DST80 cipher used in immobilisers of several manufacturers. Additionally, we expose serious flaws in immobiliser systems of major car manufacturers such as Toyota, Kia, Hyundai and Tesla. Specifically, by voltage glitching the firmware protection mechanisms of the microcontroller, we extracted the firmware from several immobiliser ECUs and reverse engineered the key diversification schemes employed within. We discovered that Kia and Hyundai immobiliser keys have only three bytes of entropy and that Toyota only relies on publicly readable information such as the transponder serial number and three constants to generate cryptographic keys. Furthermore, we present several practical attacks which can lead to recovering the full 80-bit cryptographic key in a matter of seconds or permanently disabling the transponder. Finally, even without key management or configuration issues, we demonstrate how an attacker can recover the cryptographic key using a profiled side-channel attack. We target the key loading procedure and investigate the practical applicability in the context of portability. Our work once again highlights the issues automotive vendors face in implementing cryptography securely.
2020
TCHES
Fill your Boots: Enhanced Embedded Bootloader Exploits via Fault Injection and Binary Analysis
The bootloader of an embedded microcontroller is responsible for guarding the device’s internal (flash) memory, enforcing read/write protection mechanisms. Fault injection techniques such as voltage or clock glitching have been proven successful in bypassing such protection for specific microcontrollers, but this often requires expensive equipment and/or exhaustive search of the fault parameters. When multiple glitches are required (e.g., when countermeasures are in place) this search becomes of exponential complexity and thus infeasible. Another challenge which makes embedded bootloaders notoriously hard to analyse is their lack of debugging capabilities.This paper proposes a grey-box approach that leverages binary analysis and advanced software exploitation techniques combined with voltage glitching to develop a powerful attack methodology against embedded bootloaders. We showcase our techniques with three real-world microcontrollers as case studies: 1) we combine static and on-chip dynamic analysis to enable a Return-Oriented Programming exploit on the bootloader of the NXP LPC microcontrollers; 2) we leverage on-chip dynamic analysis on the bootloader of the popular STM8 microcontrollers to constrain the glitch parameter search, achieving the first fully-documented multi-glitch attack on a real-world target; 3) we apply symbolic execution to precisely aim voltage glitches at target instructions based on the execution path in the bootloader of the Renesas 78K0 automotive microcontroller. For each case study, we show that using inexpensive, open-design equipment, we are able to efficiently breach the security of these microcontrollers and get full control of the protected memory, even when multiple glitches are required. Finally, we identify and elaborate on several vulnerable design patterns that should be avoided when implementing embedded bootloaders.
2018
TCHES
Dismantling the AUT64 Automotive Cipher 📺
Christopher Hicks Flavio D. Garcia David Oswald
AUT64 is a 64-bit automotive block cipher with a 120-bit secret key used in a number of security sensitive applications such as vehicle immobilization and remote keyless entry systems. In this paper, we present for the first time full details of AUT64 including a complete specification and analysis of the block cipher, the associated authentication protocol, and its implementation in a widely-used vehicle immobiliser system that we have reverse engineered. Secondly, we reveal a number of cryptographic weaknesses in the block cipher design. Finally, we study the concrete use of AUT64 in a real immobiliser system, and pinpoint severe weaknesses in the key diversification scheme employed by the vehicle manufacturer. We present two key-recovery attacks based on the cryptographic weaknesses that, combined with the implementation flaws, break both the 8 and 24 round configurations of AUT64. Our attack on eight rounds requires only 512 plaintext-ciphertext pairs and, in the worst case, just 237.3 offline encryptions. In most cases, the attack can be executed within milliseconds on a standard laptop. Our attack on 24 rounds requires 2 plaintext-ciphertext pairs and 248.3 encryptions to recover the 120-bit secret key in the worst case. We have strong indications that a large part of the key is kept constant across vehicles, which would enable an attack using a single communication with the transponder and negligible offline computation.
2010
EPRINT
Dismantling SecureMemory, CryptoMemory and CryptoRF
The Atmel chip families SecureMemory, CryptoMemory, and CryptoRF use a proprietary stream cipher to guarantee authenticity, confidentiality, and integrity. This paper describes the cipher in detail and points out several weaknesses. One is the fact that the three components of the cipher operate largely independently; another is that the intermediate output generated by two of those components is strongly correlated with the generated keystream. For SecureMemory, a single eavesdropped trace is enough to recover the secret key with probability 0.57 in 2^{39} cipher ticks. This is a factor of 2^{31.5} faster than a brute force attack. On a 2 GHz laptop, this takes around 10 minutes. With more traces, the secret key can be recovered with virtual certainty without significant additional cost in time. For CryptoMemory and CryptoRF, if one has 2640 traces it is possible to recover the key in 2^{52} cipher ticks, which is 2^{19} times faster than brute force. On a 50 machine cluster of 2 GHz quad-core machines this would take less than 2 days.
2006
EPRINT
Sound Computational Interpretation of Formal Hashes
Flavio D. Garcia Peter van Rossum
This paper provides one more step towards bridging the gap between the formal and computational approaches to cryptographic protocols. We extend the well-known Abadi-Rogaway logic with probabilistic hashes and we give precise semantic to it using Canetti's oracle hashing. Finally, we show that this interpretation is computationally sound.
2006
EPRINT
Completeness of Formal Hashes in the Standard Model
Flavio D. Garcia Peter van Rossum
We study an extension of the well-known Abadi-Rogaway logic with hashes. Previously, we have given a sound computational interpretation of this extension using Canetti's oracle hashing. This paper extends Micciancio and Warinschi's completeness result for the original logic to this setting.