13 citations · 19 across the 3 of their papers we have counts for
5 papers
An Abstract Framework for Choreographic Testing
Alex Coto, Roberto Guanciale, Emilio Tuosto
We initiate the development of a model-driven testing framework for message-passing systems. The notion of test for communicating systems cannot simply be borrowed from existing pr…
Speculative Leakage in ARM Cortex-A53
Hamed Nemati, Roberto Guanciale, Pablo Buiras +1
The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and s…
Validation of Abstract Side-Channel Models for Computer Architectures
Hamed Nemati, Pablo Buiras, Andreas Lindner +2
Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to vali…
InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis
Roberto Guanciale, Musard Balliu, Mads Dam
The recent Spectre attacks has demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation…
TrABin: Trustworthy Analyses of Binaries
Andreas Lindner, Roberto Guanciale, Roberto Metere
Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analy…