Abstract
Since the discovery of transient execution attacks, we know that the micro-architecture of computers has a major impact on the security of cloud and other computers running code from multiple players. The speaker described these transient execution attacks and the corresponding protections. To do this, he used modeling techniques from programming language research, and showed how to describe out-of-order and speculative executions, as well as attackers able to observe and modify the state of the micro-architecture. He then used these models to describe several attacks on transient executions and to present protections against these attacks, insisting on the precise definition of the security objectives expected for these protections.