16 citations · 31 across the 10 of their papers we have counts for
12 papers
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…
Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA
Karl Palmskog, Andreas Lindner, Scott Constable +2
Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be…
Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
Hamed Nemati, Mads Dam
Shared-memory concurrency is notoriously difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments…
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…
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Andreas Lindner, Karl Palmskog, Scott Constable +3
Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when…
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…