How did your project originate?
It grew out of the SAFE project, on which I worked at the University of Pennsylvania between 2011 and 2013 and which was at that time funded by the US Defense Department through the DARPA agency. The aim was to build a new secure system from scratch, without any backwards compatibility constraints. It was essentially a thought experiment and some of the ideas that emerged were retained in our follow-up project, called “Micro-policies”, which is a collaboration between Inria, the University of Pennsylvania and some other academic and industrial partners. The basic idea is to use hardware support to strengthen security and to prove formally that security was achieved. For example, one of the problems that we need to resolve is memory safety, ensuring for instance that memory pointers are not accessed out of bounds and thus preventing today’s most devastating cyber-attacks.
Current hardware architectures do not provide suitable security mechanisms for this and obtaining memory safety by software checks would be too expensive. Beyond just memory safety we, have generally looked at how to improve cyber security by way of novel hardware, at the lowest level of the system. But now I would like to take this to the a whole new level and study how our hardware innovations can be used to devise secure compilers for realistic programming languages to beef up cyber security on all levels. Devising the first efficient formally secure compilers is the topic of my new ERC grant.
Why did you get involved in this adventure?
I wanted to build a research team around my ideas. I believe that cyber security in general and secure compilation in particular are crucial issues. That’s why I want to help promote the secure compilation idea among the research community and show that using novel hardware and formal verification for this is a feasible way forward. The ERC grant will also enable us to gain international visibility for our project. So I submitted an application in November 2015 and took part in the second selection round in July.
Concretely, how will you use the funding you will receive?
I will receive €1.5 million in funding over the next 5 years. This will allow me to put together a team to work with me on this project, so I’m looking to hire PhD students and young researchers with an interest in security, programming languages, and formal verification. This will also allow us to further develop our partnerships. I am already collaborating with researchers at the University of Pennsylvania and other institutions in the United States, but I would also like to increase my collaborations in Europe. This means foreign travel for the researchers on my team and I will also invite foreign researchers to visit us more often.
- 2007-2012: PhD at the University of Saarland, in Saarbrücken, Germany
- 2011-2013: Research Associate at the University of Pennsylvania working on the SAFE project
- 2013: Joined the Inria Prosecco team in Paris
- 2016: Awarded a European Research Council grant on Efficient Formally Secure Compilers to a Tagged Architecture