Luca De Feo (IBM Research)
On the (in)security of ElGamal in OpenPGP
Do you think you know ElGamal encryption? Think twice.
We uncover vulnerabilities in the OpenPGP ecosystem stemming from confusion about the definition of ElGamal encryption (and the lack of an unequivocable standard). The first vulnerability leads to practical plaintext recovery in a limited number of cases. The second one, combined with side-channel leakage we found in some popular OpenPGP libraries, leads to feasible key recovery, in relatively rare cases.
We hope that these attacks, that we dub "cross-configuration", serve as a cautionary tale for standards designers. Cryptographic algorithms, even when they may appear very simple, hide a great deal of complexity in the choices of parameters and data representation. While an instantiation may appear to be safe in isolation, the interaction of two incompatible instantiations may lead to a security disaster, which can only be avoided by a carefully written standard.
Joint work with Bertram Poettering and Alessandro Sorniotti.
Omar Haider Chowdhury (University of Iowa)
Towards a High-Assurance and Specification-Compliant X.509 PKI Implementation
The X.509 Public-Key Infrastructure (PKI) is one of the most prominent and widely used authentication mechanisms, which plays a crucial role in different applications such as secure communication (e.g., SSL/TLS, IPSec), software updates, and emails. Flaws in an X.509 PKI implementation can make an application relying on X.509 PKI susceptible to impersonation attacks or interoperability issues. In this talk, I will discuss my group's effort in developing a high-assurance and specification-compliant implementation of X.509 PKI.
First, I will discuss the Symcerts system that uses domain-specific optimizations, symbolic execution, and differential analysis to automatically identify specification non-compliance in open-source SSL/TLS libraries. Second, I will discuss Morpheus, a black-box analysis engine, that automatically checks the logical correctness of RSA signature verification implementations in open-source SSL/TLS libraries through a formally verified oracle. Third, I will discuss my group's effort to formalize and re-engineer the specification of the X.509 certificate chain validation using an executable specification. I will conclude my talk with a sneak peek of our ongoing work on developing a formally verified implementation of the X.509 PKI.
Yuzhe Tang (Syracuse University)
Understanding and Hardening Blockchain Systems Security under DoS Attacks
Ethereum is the largest smart-contract platform and second-largest cryptocurrency only after Bitcoin. Under the hood, Ethereum is a peer-to-peer network where miner nodes come to a consensus and decide what transactions to include in the blockchain. In practice, Ethereum's P2P network receives transactions sent from millions of web clients and propagates them to the tens of thousands of miner nodes. While the blockchain-to-client communication channel is a part of the system's critical path, its security is understudied in the existing research literature. This talk presents our recent research examining Ethereum systems security under the denial-of-service attack vectors (CCS'21, NDSS'21, and IMC'21). The security vulnerabilities discovered in these works have been confirmed and then fixed by the Ethereum developer community.