Analysis of low-level implementations of cryptographic protocols
Gkaniatsou, Andriana Evgenia
This thesis examines the vulnerabilities due to low-level implementation deficiencies of otherwise secure communication protocols in smart-cards. Smart-cards are considered to be one of the most secure, tamper-resistant, and trusted devices for implementing confidential operations, such as authentication, key management, encryption and decryption for financial, communication, security and data management purposes. The self-containment of smart-cards makes them resistant to attacks as they do not depend on potentially vulnerable external resources. As such, smart-cards are often incorporated in formally-verified protocols that require strong security of the cryptographic computations. Such a setting consists of a smart-card which is responsible for the execution of sensitive operations, and an Application Programming Interface (API) which implements a particular protocol. For the smart-card to execute any kind of operation there exists a confidential low-level communication with the API, responsible for carrying out the protocol specifications and requests. This communication is kept secret on purpose by some vendors, under the assumption that hiding implementation details enhances the system’s security. The work presented in this thesis analyses such low-level protocol implementations in smart-cards, especially those whose implementation details are deliberately kept secret. In particular, the thesis consists of a thorough analysis of the implementation of PKCS#11 and Bitcoin smart-cards with respect to the low-level communication layer. Our hypothesis is that by focusing on reverse-engineering the low-level implementation of the communication protocols in a disciplined and generic way, one can discover new vulnerabilities and open new attack vectors that are not possible when looking at the highest levels of implementation, thereby compromising the security guarantees of the smart-cards. We present REPROVE, a system that automatically reverse-engineers the low-level communication of PKCS#11 smart-cards, deduces the card’s functionalities and translates PKCS#11 cryptographic functions into communication steps. REPROVE deals with both standard-conforming and proprietary implementations, and does not require access to the card. We use REPROVE to reverse-engineer seven commercially available smart-cards. Moreover, we conduct a security analysis of the obtained models and expose a set of vulnerabilities which would have otherwise been unknown. To the best of our knowledge, REPROVE is the first system to address proprietary implementations and the only system that maps cryptographic functions to communication steps and on-card operations. To that end, we showcase REPROVE’s usefulness to a security ecosystem by integrating it with an existing tool to extract meaningful state-machines of the card’s implementations. To conduct a security analysis of the results we obtained, we define a threat model that addresses low-level PKCS#11 implementations. Our analysis indicates a series of implementation errors that leave the cards vulnerable to attacks. To that end, we showcase how the discovered vulnerabilities can be exploited by presenting practical attacks. The results we obtained from the PKCS#11 smart-card analysis showed that proprietary implementations commonly hide erroneous behaviours. To test the assumption that the same practice is also adopted by other protocols, we further examine the low-level implementation of the only available smart-card based Bitcoin wallets, LEDGER. We extract the different protocols that the LEDGER wallets implement and conduct a through analysis. Our results indicate a set of vulnerabilities that expose the wallets as well as the processed transactions to multiple threats. To that end, we present how we successfully mounted attacks on the LEDGER wallets that lead to the loss of the wallet’s ownership and consequently loss of the funds. We address the lack of well-defined security properties that Bitcoin wallets should conform to by introducing a general threat model. We further use that threat model to propose a lightweight fix that can be adopted by other, not necessarily smart-card-based, wallets.