Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations - ICT Systems Security and Privacy Protection Access content directly
Conference Papers Year : 2018

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

Wei Chen
  • Function : Author
  • PersonId : 1042882
Yuhui Lin
  • Function : Author
  • PersonId : 1042883
Vashti Galpin
  • Function : Author
  • PersonId : 1022459
Vivek Nigam
  • Function : Author
  • PersonId : 849255
Myungjin Lee
  • Function : Author
  • PersonId : 1042884


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 formalized 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.
Fichier principal
Vignette du fichier
472722_1_En_22_Chapter.pdf (735.34 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-02023718 , version 1 (21-02-2019)




Wei Chen, Yuhui Lin, Vashti Galpin, Vivek Nigam, Myungjin Lee, et al.. Formal Analysis of Sneak-Peek: A Data Centre Attack and Its Mitigations. 33th IFIP International Conference on ICT Systems Security and Privacy Protection (SEC), Sep 2018, Poznan, Poland. pp.307-322, ⟨10.1007/978-3-319-99828-2_22⟩. ⟨hal-02023718⟩
56 View
52 Download



Gmail Mastodon Facebook X LinkedIn More