Abstract

Caches pose a significant challenge to formal verification, as the cache access pattern of security-critical services may leak secret information. We present a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack on various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place inconsistent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defense mechanisms on the binary code of the trusted software.