Showing 1–10 of 10 results for author: Nemati, H

Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization

Authors: Tiziano Marinaro, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Hamed Nemati

Abstract: Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using s… ▽ More Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered. △ Less

Submitted 15 December, 2023; originally announced December 2023.

Comments: The paper will appear in ACM AsiaCCS 2024

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time

Authors: Nicholas Mosier, Hamed Nemati, John C. Mitchell, Caroline Trippel

Abstract: We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by s… ▽ More We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives--instructions that can transiently assign a secret value to a publicly-typed register. We evaluate Serberus on cryptographic primitives in the OpenSSL, Libsodium, and HACL* libraries. Serberus introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure. △ Less

Submitted 10 September, 2023; originally announced September 2023.

Comments: Authors' version; to appear in the Proceedings of the IEEE Symposium on Security and Privacy (S&P) 2024

CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati

Abstract: We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic e… ▽ More We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGuard, a modern VPN protocol. △ Less

Submitted 18 September, 2023; v1 submitted 28 August, 2023; originally announced August 2023.

Microarchitectural Leakage Templates and Their Application to Cache-Based Side Channels

Authors: Ahmad Ibrahim, Hamed Nemati, Till Schlüter, Nils Ole Tippenhauer, Christian Rossow

Abstract: The complexity of modern processor architectures has given rise to sophisticated interactions among their components. Such interactions may result in potential attack vectors in terms of side channels, possibly available to user-land exploits to leak secret data. Exploitation and countering of such side channels require a detailed understanding of the target component. However, such detailed infor… ▽ More The complexity of modern processor architectures has given rise to sophisticated interactions among their components. Such interactions may result in potential attack vectors in terms of side channels, possibly available to user-land exploits to leak secret data. Exploitation and countering of such side channels require a detailed understanding of the target component. However, such detailed information is commonly unpublished for many CPUs. In this paper, we introduce the concept of Leakage Templates to abstractly describe specific side channels and identify their occurrences in binary applications. We design and implement Plumber, a framework to derive the generic Leakage Templates from individual code sequences that are known to cause leakage (e.g., found by prior work). Plumber uses a combination of instruction fuzzing, instructions' operand mutation and statistical analysis to explore undocumented behavior of microarchitectural optimizations and derive sufficient conditions on vulnerable code inputs that, if hold can trigger a distinguishing behavior. Using Plumber we identified novel leakage primitives based on Leakage Templates (for ARM Cortex-A53 and -A72 cores), in particular related to previction (a new premature cache eviction), and prefetching behavior. We show the utility of Leakage Templates by re-identifying a prefetcher-based vulnerability in OpenSSL 1.1.0g first reported by Shin et al. [40]. △ Less

Submitted 25 November, 2022; originally announced November 2022.

Relational Models of Microarchitectures for Formal Security Analyses

Authors: Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, Caroline Trippel

Abstract: There is a growing need for hardware-software contracts which precisely define the implications of microarchitecture on software security-i.e., security contracts. It is our view that such contracts should explicitly account for microarchitecture-level implementation details that underpin hardware leakage, thereby establishing a direct correspondence between a contract and the microarchitecture it… ▽ More There is a growing need for hardware-software contracts which precisely define the implications of microarchitecture on software security-i.e., security contracts. It is our view that such contracts should explicitly account for microarchitecture-level implementation details that underpin hardware leakage, thereby establishing a direct correspondence between a contract and the microarchitecture it represents. At the same time, these contracts should remain as abstract as possible so as to support efficient formal analyses. With these goals in mind, we propose leakage containment models (LCMs)-novel axiomatic security contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our core contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage-focusing on leakage through hardware memory systems-so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we present two case studies. First, we demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Second, we develop a static analysis tool based on LCMs which automatically identifies Spectre vulnerabilities in programs and scales to analyze realistic-sized codebases, like libsodium. △ Less

Submitted 20 December, 2021; originally announced December 2021.

Osiris: Automated Discovery of Microarchitectural Side Channels

Authors: Daniel Weber, Ahmad Ibrahim, Hamed Nemati, Michael Schwarz, Christian Rossow

Abstract: In the last years, a series of side channels have been discovered on CPUs. These side channels have been used in powerful attacks, e.g., on cryptographic implementations, or as building blocks in transient-execution attacks such as Spectre or Meltdown. However, in many cases, discovering side channels is still a tedious manual process. In this paper, we present Osiris, a fuzzing-based framework… ▽ More In the last years, a series of side channels have been discovered on CPUs. These side channels have been used in powerful attacks, e.g., on cryptographic implementations, or as building blocks in transient-execution attacks such as Spectre or Meltdown. However, in many cases, discovering side channels is still a tedious manual process. In this paper, we present Osiris, a fuzzing-based framework to automatically discover microarchitectural side channels. Based on a machine-readable specification of a CPU's ISA, Osiris generates instruction-sequence triples and automatically tests whether they form a timing-based side channel. Furthermore, Osiris evaluates their usability as a side channel in transient-execution attacks, i.e., as the microarchitectural encoding for attacks like Spectre. In total, we discover four novel timing-based side channels on Intel and AMD CPUs. Based on these side channels, we demonstrate exploitation in three case studies. We show that our microarchitectural KASLR break using non-temporal loads, FlushConflict, even works on the new Intel Ice Lake and Comet Lake microarchitectures. We present a cross-core cross-VM covert channel that is not relying on the memory subsystem and transmits up to 1 kbit/s. We demonstrate this channel on the AWS cloud, showing that it is stealthy and noise resistant. Finally, we demonstrate Stream+Reload, a covert channel for transient-execution attacks that, on average, allows leaking 7.83 bytes within a transient window, improving state-of-the-art attacks that only leak up to 3 bytes. △ Less

Submitted 7 June, 2021; originally announced June 2021.

Comments: Will be published at USENIX Security'21

Speculative Leakage in ARM Cortex-A53

Authors: Hamed Nemati, Roberto Guanciale, Pablo Buiras, Andreas Lindner

Abstract: The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support o… ▽ More The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support out-of-order execution. We named this new class of vulnerabilities SiSCloak. △ Less

Submitted 17 July, 2020; v1 submitted 14 July, 2020; originally announced July 2020.

Validation of Abstract Side-Channel Models for Computer Architectures

Authors: Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs

Abstract: Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment… ▽ More Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior. △ Less

Submitted 11 May, 2020; originally announced May 2020.

Secure System Virtualization: End-to-End Verification of Memory Isolation

Authors: Hamed Nemati

Abstract: Over the last years, security kernels have played a promising role in resha** the landscape of platform security on today's ubiquitous embedded devices. Security kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms. They reduce the software portion of the system's trusted computing base to a thin layer, which enforces isolation between low… ▽ More Over the last years, security kernels have played a promising role in resha** the landscape of platform security on today's ubiquitous embedded devices. Security kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms. They reduce the software portion of the system's trusted computing base to a thin layer, which enforces isolation between low- and high-criticality components. The reduced trusted computing base minimizes the system attack surface and facilitates the use of formal methods to ensure functional correctness and security of the kernel. In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. In particular, we examine techniques related to the appropriate management of the memory subsystem. Once these techniques were implemented and functionally verified, they provide reliable a foundation for application scenarios that require strong guarantees of isolation and facilitate formal reasoning about the system's overall security. △ Less

Submitted 6 May, 2020; originally announced May 2020.

Varactor-Based Dynamic Load Modulation of High Power Amplifiers

Authors: Ali Soltani Tehrani, Hossein Mashad Nemati, Haiying Cao, Thomas Eriksson, Christian Fager

Abstract: In this work, dynamic load modulation of high power amplifiers using a varactor-based tunable matching network is presented. The feasibility of dynamic tuning and efficiency enhancement of this technique is demonstrated using a modular design approach for two existing high efficiency power amplifiers (PA), a 7-W class-E, and a 10-W class-J power amplifier PA at 1 GHz. For this purpose and for each… ▽ More In this work, dynamic load modulation of high power amplifiers using a varactor-based tunable matching network is presented. The feasibility of dynamic tuning and efficiency enhancement of this technique is demonstrated using a modular design approach for two existing high efficiency power amplifiers (PA), a 7-W class-E, and a 10-W class-J power amplifier PA at 1 GHz. For this purpose and for each of the PAs, a simple quasi-static inverse model is developed allowing an efficiency-optimized control of the PA and the varactor-based tunable matching network. Modulated measurements using a single carrier WCDMA signal with 11.3 dB peak-to-average ratio (PAR) indicate about 10 to 14 percentage units improvements in the average power-added efficiency (PAE) for the complete architecture. △ Less

Submitted 24 October, 2012; v1 submitted 12 October, 2012; originally announced October 2012.