3 papers
cs.CR2025
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.CR2025
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…
cs.LO2025
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…