Frank Piessens is a full professor in the Department of Computer Science at the Katholieke Universiteit Leuven, Belgium. His research field is software and system security, where he focuses on the development of high-assurance techniques to deal with implementation-level software vulnerabilities and bugs, including techniques such as software verification, run-time monitoring, hardware security architectures, type systems and programming language design. He has served on the program committee of numerous security and software conferences including ACM CCS, Usenix Security, IEEE Security & Privacy, and ACM POPL. He acted as program chair for the International symposium on Engineering Secure Software and Systems (ESSOS 2014 & 2015), for the International Conference on Principles of Security and Trust (POST 2016) and for the IEEE European Symposium on Security & Privacy (Euro S&P 2018 & 2019).

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

90 Minutes

Saarbrücken

Microarchitectural security is one of the most challenging and exciting problems in system security today. With the discovery of transient execution attacks, it has become clear that microarchitectural attacks have significant impact on the security properties of software running on a processor that runs code from various stakeholders (such as, for instance, in the cloud). This talk will first provide an overview of the current understanding of microarchitectural security, with a focus on how the research community has built formal models for processors that support proving that software is resilient to specific classes of microarchitectural attacks. Next, we turn to the problem of validating these proposed formal models: how can we convince ourselves and others that a given formal model is an adequate model for a given real-world processor, and that we can justifiably trust the security properties proven based on the model. This is an instance of the more general problem of empirically validating whether a real-world system satisfies the assumptions on which a formal model relies. We will discuss a small case study where we empirically validated a formally proven security property of a simple processor by systematically attacking the corresponding real-world implementation of the processor. We end with some conclusions and reflections on how our experiences from this case study might help us build more adequate formal models.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Annika Meiser

+49 681 9303 9105

--email hidden