5 papers
SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
Shixin Song, Davide Davoli, Elias Storme +4
Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leaka…
dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era (Extended Version)
Davide Davoli, Marton Bognar, Lesly-Ann Daniel +3
Speculative execution attacks such as Spectre-PHT and Spectre-STL remain a critical security concern in modern processors. While software-based mitigations like Speculative Load Ha…
Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)
Davide Davoli, Martin Avanzini, Tamara Rezk
The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs…
A quantitative probabilistic relational Hoare logic
Martin Avanzini, Gilles Barthe, Davide Davoli +1
We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-condition…
On Kernel's Safety in the Spectre Era (Extended Version)
Davide Davoli, Martin Avanzini, Tamara Rezk
The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs…