16 citations · 31 across the 10 of their papers we have counts for
9 papers · 1 filter
SADRA: Sound Capability-based Access Control System for Resource-Disaggregated Architectures
Hamed Rasifard, Amir Farahani Khojasteh, Hamed Nemati +1
Resource disaggregation separates memory and accelerators from compute nodes and makes them remotely accessible. This improves resource sharing, but also removes the local kernel f…
Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs
Elvira Moreno, Tiziano Marinaro, Ryan Williams +4
Side-channel attacks pose a significant security threat for modern computing platforms, because they exploit subtle discrepancies in CPU behaviors to leak sensitive information. To…
CryptoBap: A Binary Analysis Platform for Cryptographic Protocols
Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati
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 transpilin…
Microarchitectural Leakage Templates and Their Application to Cache-Based Side Channels
Ahmad Ibrahim, Hamed Nemati, Till Schlüter +2
The complexity of modern processor architectures has given rise to sophisticated interactions among their components. Such interactions may result in potential attack vectors in te…
Relational Models of Microarchitectures for Formal Security Analyses
Nicholas Mosier, Hanna Lachnitt, Hamed Nemati +1
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 t…
Osiris: Automated Discovery of Microarchitectural Side Channels
Daniel Weber, Ahmad Ibrahim, Hamed Nemati +2
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 bui…
Speculative Leakage in ARM Cortex-A53
Hamed Nemati, Roberto Guanciale, Pablo Buiras +1
The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and s…
Validation of Abstract Side-Channel Models for Computer Architectures
Hamed Nemati, Pablo Buiras, Andreas Lindner +2
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 vali…
Secure System Virtualization: End-to-End Verification of Memory Isolation
Hamed Nemati
Over the last years, security kernels have played a promising role in reshaping the landscape of platform security on today's ubiquitous embedded devices. Security kernels, such as…