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

abstract

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