Towards Formal Verification of Cache Access-based Side-Channel Attacks

Cache access-based side-channel attacks utilize the timing difference between cache hits and misses as a leakage source to jeopardize system security. Although previous works address such threat, finding secure and efficient solutions to verify the security is still a challenge. In this paper, we propose a method that allows the formal verification of the security properties of cache. In the experiments, we show our technique to formally verify the security of four cache configurations, by changing the number of cache lines, associativity and cache line size. We show that our method is an effective and efficient solution towards a secure cache.     «

Cache access-based side-channel attacks utilize the timing difference between cache hits and misses as a leakage source to jeopardize system security. Although previous works address such threat, finding secure and efficient solutions to verify the security is still a challenge. In this paper, we propose a method that allows the formal verification of the security properties of cache. In the experiments, we show our technique to formally verify the security of four cache configurations, by cha...     »