3 papers
cs.CR2024
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…
cs.LO2024
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…
cs.CR2024
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…