Model Checking Timed Hyperproperties
Jens Heinen
Timing attacks have become fairly known in context of the Meltdown exploit, where attackers used the vulnerability of CPU caches against timing attacks on kernel space data. The threat of timing attacks on privacy-critical systems raises the need of time dependent analysis and checking specific properties on these systems. A well known example of a timing attack is the extraction of the password from a bad password checking algorithm, which stops processing the input on the first index where the saved password and the user input differ. We can create a simple MITL property for a timing-attack free system (G[2,2] answer). The property ensures that the password checker always has to give the answer exactly after two time units, independently of the correctness of the input. However, this excludes traces where the password checker can give the answer earlier. To improve the response time of the password checker while remaining timing attack free, an improved property can be formulated as follows: Every pair of execution traces agree on the answer and give an answer at least in two time steps. This cannot be expressed in MITL as it is a hyperproperty. A hyperproperty is a set of sets of traces and hence relates multiple computation traces. HyperLTL is a temporal logic to express hyperproperties. The example property additionally has a timing constraint, which in turn cannot be formalized in HyperLTL. In this thesis a new logic for timed hyperproperties is constructed. Properties to prevent timing attacks on password checking systems and cryptographic systems are formulated and checked on suitable models. The corresponding model checking problem for Timed HyperLTL is studied together with its complexity.
Master Thesis.