Edinburgh Research Explorer

Formal Analysis of Sneak-Peek: A Data-Centre Attack and its Mitigations

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publication33rd International Conference on Information Security and Privacy Protection (IFIP SEC 2018)
Place of PublicationPoznan, Poland
PublisherSpringer, Cham
Number of pages16
ISBN (Electronic)978-3-319-99828-2
ISBN (Print)978-3-319-99827-5
Publication statusPublished - 2018
Event33rd IFIP TC-11 SEC 2018 International Conference on Information Security and Privacy Protection (IFIPSEC 2018) - Poznań, Poland
Duration: 18 Sep 201820 Sep 2018


Conference33rd IFIP TC-11 SEC 2018 International Conference on Information Security and Privacy Protection (IFIPSEC 2018)
Abbreviated titleIFIPSEC 2018
Internet address


Attackers can exploit covert channels, such as timing side-channels, to transmit information without data owners or network administrators being aware. Sneak-Peek is a recently considered data centre attack, where, in a multi-tenant setting, an insider attacker can communicate with colluding outsiders by intentionally adding delays to traffic on logically isolated but physically shared links. Timing attack mitigations typically introduce delays or randomness which can make it difficult to understand the trade-off between level of security (bandwidth of the covert channel) and performance loss. We demonstrate that formal methods can help. We analyse the impacts of two Sneak-Peek mitigations, namely, noise addition and path hopping. We provide a precise mathematical model of the attack and of the effectiveness these defences. This mathematical analysis is extended by two tool-based stochastic formal models, one formalised in UPPAAL and the other in CARMA. The formal models can capture more general and larger networks than a paper-based analysis, can be used to check properties and make measurements, and are more easily modifiable than conventional network simulations. With UPPAAL, we can analyse the effectiveness of mitigations and with CARMA, we can analyse how these mitigations affect latencies in typical data centre topologies. As results, we show that using a selective strategy for path hopping is better than a random strategy, that using the two defences in conjunction may actually be worse than using a single defence, and we show the connection between hop frequency and network latency.

Download statistics

No data available

ID: 61150175