Agenda

10 Dic 2021 12:00

Securing Interruptible Enclaved Execution on Small Microprocessors

Sala riunioni B (Zeta building) and Zoom

Matteo Busi, University of Pisa

Abstract:
Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features brings a risk of introducing new software-based side-channel attacks. In this talk we show how we extended a processor with new features without weakening the security of the isolation mechanisms that the processor offers. Our solution is heavily based on techniques from research on programming languages. More specifically, we propose to use the programming language concept of full abstraction as a general formal criterion for the security of a processor extension. We instantiate the proposed criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, prove that it satisfies our security criterion and explain how such design drove the actual implementation of an enclave-enabled microprocessor. The seminar will take place at Sala riunioni B in the Zeta building.

It will be also broadcasted through Zoom at the following link:
https://unive.zoom.us/j/84897290153?pwd=WXZ1dmJJR3F3MStRYmMvc2FrRWFXQT09
Meeting ID: 848 9729 0153
Passcode: Seminar22

Bio Sketch:
Matteo Busi got his PhD at the University of Pisa and he is currently a post-doc at the same university. His research interests include cybersecurity, programming languages, and formal methods. Currently, he is focusing is on secure compilation, that is how is it possible to guarantee that program transformations preserve security properties?

Lingua

L'evento si terrà in inglese

Organizzatore

Dipartimento di Scienze Ambientali, Informatica e Statistica, Pietro Ferrara

Cerca in agenda