activity
20162023
most citedStrong and Provably Secure Database Access Control

8 citations · 25 across the 8 of their papers we have counts for

collaborators

13 papers

cs.CR2023★ 3 cited

Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Zilong Wang, Gideon Mohr, Klaus von Gleissenthall +2

Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the informatio…

cs.CR2023★ 6 cited

Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing

Oleksii Oleksenko, Marco Guarnieri, Boris Köpf +1

Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect spec…

cs.CR2022★ 1 cited

Automatic Detection of Speculative Execution Combinations

Xaver Fabian, Marco Guarnieri, Marco Patrignani

Modern processors employ different prediction mechanisms to speculate over different kinds of instructions. Attackers can exploit these prediction mechanisms simultaneously in orde…

cs.CR2022★ 2 cited

A Turning Point for Verified Spectre Sandboxing

Sunjay Cauligi, Marco Guarnieri, Daniel Moghimi +2

Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to blo…

cs.PL2022

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

Sankha Narayan Guria, Niki Vazou, Marco Guarnieri +1

Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but bre…

cs.CR2020★ 2 cited

Contract-Aware Secure Compilation

Marco Guarnieri, Marco Patrignani

Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the con…