Formally Verifying Data-Oblivious Behavior In HW Using Standard Property Checking Techniques


A technical paper titled “A Scalable Formal Verification Methodology for Data-Oblivious Hardware” was published by researchers at RPTU Kaiserslautern-Landau and Stanford University. Abstract: "The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique... » read more

Security Research: Technical Paper Round-up


A number of hardware security-related technical papers were presented at the August 2023 USENIX Security Symposium. Here are some highlights with associated links. [table id=130 /] A complete listing of all papers presented at this summer's USENIX conference can be found here and here. The organization provides open access research, and the presentation slides and papers are free to the p... » read more

Formally Modeling A Security Monitor For Virtual Machine-Based Confidential Computing Systems (IBM)


A technical paper titled “Towards a Formally Verified Security Monitor for VM-based Confidential Computing” was published by researchers at IBM Research and IBM T.J. Watson Research Center. Abstract: "Confidential computing is a key technology for isolating high-assurance applications from the large amounts of untrusted code typical in modern systems. Existing confidential computing syste... » read more

Hardware-Assisted Malware Analysis


A technical paper titled "On the Feasibility of Malware Unpacking via Hardware-assisted Loop Profiling" was published by researches at Shandong University & Hubei Normal University, Tulane University and University of Texas at Arlington.  This paper was included at the recent 32nd USENIX Security Symposium. Abstract "Hardware Performance Counters (HPCs) are built-in registers of modern... » read more

Transient Execution Attacks That Leaks Arbitrary Kernel Memory (ETH Zurich)


A technical paper titled “Inception: Exposing New Attack Surfaces with Training in Transient Execution” was published by researchers at ETH Zurich. Abstract: "To protect against transient control-flow hijacks, software relies on a secure state of microarchitectural buffers that are involved in branching decisions. To achieve this secure state, hardware and software mitigations restrict or... » read more

Side-Channel Security Analysis of Intel Optane Persistent Memory


A new technical paper titled "Side-Channel Attacks on Optane Persistent Memory" was published by researchers at University of Virginia, Cornell University, and Graz University of Technology. This paper was included at the recent 32nd USENIX Security Symposium. Abstract: "There is a constant evolution of technology for cloud environments, including the development of new memory storage tech... » read more

Modeling and Testing Microarchitectural Leakage of CPU Exceptions (Microsoft, Vrije Universiteit Amsterdam)


A new technical paper titled "Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions" was published by researchers at Microsoft and Vrije Universiteit Amsterdam. This paper was included at the recent 32nd USENIX Security Symposium. Abstract: "Microarchitectural leakage models provide effective tools to prevent vulnerabilities such as Spectre and Meltdown vi... » read more

Microarchitectural Side-Channel Attacks And Defenses on NVRAM DIMMs


A new technical paper titled "NVLeak: Off-Chip Side-Channel Attacks via Non-Volatile Memory Systems" was published by researchers at UC San Diego, Purdue University, and UT Austin. This paper was included at the recent 32nd USENIX Security Symposium. Abstract: "We study microarchitectural side-channel attacks and defenses on non-volatile RAM (NVRAM) DIMMs. In this study, we first perform r... » read more

Formal Processor Model Providing Provably Secure Speculation For The Constant-Time Policy


A new technical paper titled "ProSpeCT: Provably Secure Speculation for the Constant-Time Policy" was published by researchers at imec-DistriNet, KU Leuven, CEA, and INRIA. This paper was included at the recent 32nd USENIX Security Symposium. Abstract: "We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-tim... » read more

How Attackers Can Read Data From CPU’s Memory By Analyzing Energy Consumption


A technical paper titled “Collide+Power: Leaking Inaccessible Data with Software-based Power Side Channels” was published by researchers at Graz University of Technology and CISPA Helmholtz Center for Information Security. Abstract: "Differential Power Analysis (DPA) measures single-bit differences between data values used in computer systems by statistical analysis of power traces. In th... » read more

← Older posts Newer posts →