-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
620 lines (578 loc) · 46.5 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<title>ERC SECOMP - Efficient Formally Secure Compilation to a Tagged Architecture</title>
<link rel="stylesheet" type="text/css" href="./css/default.css" />
</head>
<body>
<div id="header">
<div id="logo">
<a href="./">ERC SECOMP</a>
</div>
<div id="navigation">
<!-- <a href="/">Home</a> -->
<a href="#team">Team</a>
<a href="#project">Project</a>
<a href="#positions">Positions</a>
</div>
</div>
<div id="content">
<h1>Efficient Formally Secure Compilation to a Tagged Architecture</h1>
<p><strong>SECOMP</strong> is a research project aimed at building the first efficient
formally secure compilation chains for realistic programming languages (see
<a href="#project">project description</a> below). The project encompasses a
<a href="#core">core team</a> at <a href="https://www.mpi-sp.org">MPI-SP</a> and <a href="#external">several external collaborators</a>.
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a> and the core team at MPI-SP were generously
funded for 5 years (until the end of 2021) by an <a href="https://erc.europa.eu/funding-and-grants/funding-schemes/starting-grants">ERC Starting Grant</a>.
<!-- Over the project's duration we are looking to hire several -->
<!-- excellent young researchers and students to work on the project. --></p>
<!-- at [Inria Paris] (see [open positions](#positions) below). -->
<h1 id="team">Team</h1>
<p>The core SECOMP team is located at <a href="https://www.mpi-sp.org">MPI-SP</a> in <a href="https://prosecco.gforge.inria.fr/personal/hritcu/">Bochum, Germany</a>, and currently
includes <a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>, several students, and one postdoc.
<!-- We expect to [hire a few more people](#positions) in the coming years. -->
The project also includes <a href="#external">excellent external collaborators</a>
and we are looking forward to work with additional world-class researchers with
an interest in secure compilation (see <a href="https://popl20.sigplan.org/home/prisc-2020">the PriSC workshop @ POPL</a> and
a series of Dagstuhl Seminars on secure compilation
(<a href="https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=18201">2018</a>,
<a href="https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=21481">2021</a>)).</p>
<h4 id="core">Core team at <a href="https://www.mpi-sp.org">MPI-SP</a> as of end of 2021</h4>
<ul>
<li><a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a> (SECOMP PI, Tenured Faculty)</li>
<li><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a> (PhD Student)</li>
<li><a href="https://www.linkedin.com/in/cezar-andrici-49771663/">Cezar-Constantin Andrici</a> (PhD Student)</li>
<li><a href="http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/">Jérémy Thibault</a> (PhD Student)</li>
<li><a href="https://robblanco.github.io/">Roberto Blanco</a> (PostDoc)</li>
<li><a href="https://theowinterhalter.github.io">Théo Winterhalter</a> (PostDoc)</li>
</ul>
<h4 id="external">External collaborators</h4>
<ul>
<li><a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a> (PostDoc, <a href="https://www.cylab.cmu.edu/">Carnegie Mellon University</a>)</li>
<li><a href="https://people.mpi-sws.org/~dg/">Deepak Garg</a> (Tenured Faculty, <a href="https://www.mpi-sws.org/">MPI-SWS</a>)</li>
<li><a href="https://pleiad.cl/people/etanter">Éric Tanter</a> (Visiting Professor, <a href="https://pleiad.cl/">University of Chile</a>)</li>
<li><a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a> (Professor, <a href="http://www.pdx.edu/computer-science/">Portland State University</a>)</li>
<li><a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a> (Professor, <a href="https://www.cis.upenn.edu/">University of Pennsylvania</a>)</li>
<li><a href="https://people.mpi-sws.org/~elkorashy">Akram El-Korashy</a> (PhD Student, <a href="https://www.mpi-sws.org/">MPI-SWS</a>)</li>
<li><a href="https://people.mpi-sws.org/~marcopat/">Marco Patrignani</a> (Visiting Assistant Professor, <a href="https://cs.stanford.edu/">Stanford University</a> and <a href="https://cispa.saarland/">CISPA</a>)</li>
<li><a href="http://research.microsoft.com/en-us/people/nswamy/">Nikhil Swamy</a> (Senior Researcher, <a href="http://research.microsoft.com/">Microsoft Research</a>)</li>
<li><a href="https://profs.info.uaic.ro/~stefan.ciobaca/">Ștefan Ciobâcă</a> (Associate Professor, <a href="http://www.info.uaic.ro/bin/Main/?language=en">University of Iași</a>)</li>
</ul>
<h4 id="past-members">Past members</h4>
<!-- TODO: move these to a separate page, or somehow fold them out -->
<ul>
<li><a href="https://dblp.org/pers/hd/d/Durier:Adrien">Adrien Durier</a> (PostDoc at Inria Paris and <a href="https://www.mpi-sp.org">MPI-SP</a>)</li>
<li><a href="https://github.com/kyoDralliam">Kenji Maillard</a> (PhD Student)</li>
<li><a href="https://danelahman.github.io/">Danel Ahman</a> (PostDoc)</li>
<li><a href="http://www.stronati.org/">Marco Stronati</a> (PostDoc)</li>
<li><a href="https://mtzguido.github.io">Guido Martínez</a> (PhD Student at <a href="https://www.cifasis-conicet.gov.ar">CIFASIS-CONICET</a> and <a href="https://unr.edu.ar">UNR</a>)</li>
<li><a href="https://github.com/GuglielmoS">Guglielmo Fachini</a> (Research Engineer)</li>
<li><a href="http://yannis.computer/">Yannis Juglaret</a> (Student at Inria and Paris 7)</li>
<li><a href="https://github.com/engboris">Boris Eng</a> (Research Intern at Inria, undergraduate student at Paris 8)</li>
<li><a href="https://www.cs.virginia.edu/~ans5k/">Ana Nora Evans</a> (Visiting Researcher at Inria, PhD Student at <a href="https://www.cs.virginia.edu/">University of Virginia</a>)</li>
<li><a href="https://github.com/floriangru">Florian Groult</a> (Research Intern/Engineer, Orléans University)</li>
<li><a href="https://github.com/victor-dumitrescu">Victor Dumitrescu</a> (Research Engineer)</li>
<li><a href="https://github.com/theolaurent">Théo Laurent</a> (Research Intern at Inria, ENS Paris)</li>
<li><a href="http://pit-claudel.fr/clement/">Clément Pit-Claudel</a> (Research Intern at Inria, <a href="https://www.csail.mit.edu/">MIT</a>)</li>
<li><a href="http://www.ccs.neu.edu/home/amal/">Amal Ahmed</a> (Visiting Professor at Inria, <a href="http://www.ccs.neu.edu/">Northeastern University</a>)</li>
<li><a href="https://www.williamjbowman.com/">William J. Bowman</a> (Research Intern at Inria, <a href="http://www.ccs.neu.edu/">Northeastern University</a>)</li>
<li><a href="https://aaronweiss.us/">Aaron Weiss</a> (Visiting Researcher at Inria, <a href="http://www.ccs.neu.edu/">Northeastern University</a>)</li>
<li><a href="https://www.linkedin.com/in/jake-silverman-3698aa89">Jake Silverman</a> (Visiting Researcher at Inria, <a href="https://www.cornell.edu/">Cornell University</a>)</li>
<li><a href="https://pleiad.cl/people/elabrada">Elizabeth Labrada</a> (Research Intern, <a href="https://pleiad.cl/">University of Chile</a>)</li>
</ul>
<h1 id="project">SECOMP Project</h1>
<h2 id="description">Description</h2>
<p>Severe low-level vulnerabilities abound in today’s computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilation chains, and hardware architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. Mainstream programming languages like C are currently insecure, since any undefined behavior (e.g., a buffer overflow) can compromise the security of the whole application. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient and inconvenient for most practical scenarios.</p>
<p>This line of research is aimed at leveraging emerging hardware capabilities for fine-grained compartmentalization and memory safety to build the first efficient secure compilation chains for realistic programming languages, in particular for C. Such compilation chains enforce that compartmentalized applications are compiled securely, so every component in C is protected from other C components compromised by undefined behavior. To achieve such security without sacrificing efficiency, we compile to a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules.</p>
<p>At the conclusion of the project, we have achieved and in some ways exceeded our most important objective. We have built a secure compilation chain for C components based on the CompCert formally verified C compiler, as well as several smaller prototype compilation chains targeting a tagged architecture and software-fault isolation. We used a combination of machine-checked proofs and property-based testing in the Coq proof assistant to provide high confidence that our compilation chains achieve an unprecedented level of security.</p>
<!-- TODO: update description, maybe take from habil -->
<!-- TODO: also include the 4 pages from habil somewhere? -->
<!-- Severe low-level vulnerabilities abound in today's computer systems, -->
<!-- allowing cyber-attackers to remotely gain full control. This happens -->
<!-- in big part because our programming languages, compilation chains, and -->
<!-- architectures were designed in an era of scarce hardware resources and -->
<!-- too often trade off security for efficiency. The semantics of -->
<!-- mainstream low-level languages like C is inherently insecure, and even -->
<!-- for safer languages, establishing security with respect to a -->
<!-- high-level semantics does not guarantee the absence of low-level -->
<!-- attacks. Secure compilation using the coarse-grained protection -->
<!-- mechanisms provided by mainstream hardware architectures would be too -->
<!-- inefficient for most practical scenarios. -->
<!-- This project is aimed at leveraging emerging hardware capabilities for -->
<!-- fine-grained protection to build the first, efficient secure compilation chains -->
<!-- for realistic low-level programming languages (the C language, and [Low\*] a -->
<!-- safe subset of C embedded in [F\*] for verification). These compilation chains -->
<!-- will provide a secure semantics for all programs and will ensure that high-level -->
<!-- abstractions cannot be violated even when interacting with untrusted low-level -->
<!-- code. To achieve this level of security without sacrificing efficiency, our -->
<!-- secure compilation chains target a tagged architecture, which associates a -->
<!-- metadata tag to each word and efficiently propagates and checks tags according -->
<!-- to software-defined rules. We are using property-based testing and formal -->
<!-- verification to provide high confidence that our compilation chains are indeed -->
<!-- secure. Formally, we are constructing machine-checked proofs in Coq of various -->
<!-- new security criteria, which are defined as the preservation of property classes -->
<!-- even against an adversarial context. These strong criteria complement compiler -->
<!-- correctness and ensure that no machine-code attacker can do more harm to -->
<!-- securely compiled components than a component already could with respect to a -->
<!-- secure source-level semantics. -->
<h2 id="github-repos">Github Repos</h2>
<ul>
<li><a href="https://github.com/secure-compilation/SECOMP" class="uri">https://github.com/secure-compilation/SECOMP</a></li>
<li><a href="https://github.com/secure-compilation/when-good-components-go-bad" class="uri">https://github.com/secure-compilation/when-good-components-go-bad</a></li>
<li><a href="https://github.com/secure-compilation/when-good-components-go-bad/tree/memory-sharing" class="uri">https://github.com/secure-compilation/when-good-components-go-bad/tree/memory-sharing</a></li>
<li><a href="https://github.com/secure-compilation/exploring-robust-property-preservation" class="uri">https://github.com/secure-compilation/exploring-robust-property-preservation</a></li>
<li><a href="https://github.com/secure-compilation/different_traces" class="uri">https://github.com/secure-compilation/different_traces</a></li>
<li><a href="https://github.com/FStarLang/FStar" class="uri">https://github.com/FStarLang/FStar</a></li>
<li><a href="https://github.com/SSProve/ssprove" class="uri">https://github.com/SSProve/ssprove</a></li>
<li><a href="https://github.com/QuickChick" class="uri">https://github.com/QuickChick</a></li>
<li><a href="https://github.com/arthuraa/memory-safe-language" class="uri">https://github.com/arthuraa/memory-safe-language</a></li>
</ul>
<h2 id="chatting">Chatting</h2>
<ul>
<li><a href="https://secure-compilation.zulipchat.com/register/" class="uri">https://secure-compilation.zulipchat.com/register/</a></li>
</ul>
<h2 id="publications">Most Relevant Publications</h2>
<ul>
<li><p><a href="http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/">Jérémy Thibault</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://mori1116.github.io">Dongjae Lee</a>,
<a href="https://informatik.rub.de/seceng/personen/argo">Sven Argo</a>,
<a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="https://people.mpi-sws.org/~algeorges">Aïna Linn Georges</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>, and
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="http://arxiv.org/abs/2401.16277">SECOMP: Formally Secure Compilation of Compartmentalized C Programs</a></strong>.
In <a href="https://www.sigsac.org/ccs/CCS2024/">31th ACM SIGSAC Conference on Computer and Communications Security (CCS)</a>,
pages 1061–1075. ACM, October 2024.</p>
<ul>
<li><a href="https://github.com/secure-compilation/CompCert">Coq development</a></li>
<li><a href="https://catalin-hritcu.github.io/publications/SECOMP2CHERI-PriSC23.pdf">An extended abstract</a>
about this work was presented at <a href="https://popl23.sigplan.org/home/prisc-2023">PriSC’23</a></li>
</ul></li>
<li><p><a href="https://www.linkedin.com/in/cezar-andrici-49771663/">Cezar-Constantin Andrici</a>,
<a href="https://profs.info.uaic.ro/~stefan.ciobaca/">Ștefan Ciobâcă</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://mtzguido.github.io">Guido Martínez</a>,
<a href="https://dcc.fceia.unr.edu.ar/~erivas">Exequiel Rivas</a>,
<a href="https://pleiad.cl/people/etanter">Éric Tanter</a>, and
<a href="https://theowinterhalter.github.io">Théo Winterhalter</a>.
<strong><a href="https://arxiv.org/abs/2303.01350">Securing Verified IO Programs Against Unverified Code in F*</a></strong>.
PACMPL, 8(<a href="https://popl24.sigplan.org/">POPL</a>):74:1–74:34, January 2024.</p>
<ul>
<li><a href="http://github.com/andricicezar/fstar-io">F* development</a></li>
<li><a href="https://cezarandrici.com/wp-content/uploads/2022/11/prisc23.pdf">An extended abstract</a>
about this work was presented at <a href="https://popl23.sigplan.org/home/prisc-2023">PriSC’23</a></li>
</ul></li>
<li><p><a href="https://www.linkedin.com/in/sean-noble-anderson/">Sean Noble Anderson</a>,
<a href="https://lemonidas.github.io/">Leonidas Lampropoulos</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>, and
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="https://arxiv.org/abs/2105.00417">Formalizing Stack Safety as a Security Property</a></strong>.
In <a href="https://www.ieee-security.org/TC/CSF2023/">36th IEEE Computer Security Foundations Symposium (CSF)</a>,
July 2023.</p></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>.
<strong><a href="https://doi.org/10.13154/294-9870">A Formal Framework for Correct and Secure Compilation</a></strong>
PhD Thesis, Ruhr University Bochum, October 2022.</p></li>
<li><p><a href="https://people.mpi-sws.org/~elkorashy">Akram El-Korashy</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/">Jérémy Thibault</a>,
<a href="https://dblp.org/pers/hd/d/Durier:Adrien">Adrien Durier</a>,
<a href="https://people.mpi-sws.org/~dg/">Deepak Garg</a>, and
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>.
<strong><a href="https://arxiv.org/abs/2110.01439">SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation</a></strong>.
In <a href="https://www.ieee-security.org/TC/CSF2022/">35th IEEE Computer Security Foundations Symposium (CSF)</a>,
August 2022.</p>
<ul>
<li><a href="https://github.com/secure-compilation/when-good-components-go-bad/tree/memory-sharing">Coq development</a></li>
</ul></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://profs.info.uaic.ro/~stefan.ciobaca/">Ștefan Ciobâcă</a>,
<a href="https://people.mpi-sws.org/~dg/">Deepak Garg</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://people.mpi-sws.org/~marcopat/">Marco Patrignani</a>,
<a href="https://pleiad.cl/people/etanter">Éric Tanter</a>, and
<a href="http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/">Jérémy Thibault</a>.
<strong><a href="https://doi.org/10.1145/3460860">An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation</a></strong>.
ACM Transactions on Programming Languages and Systems (TOPLAS). Volume 43, Issue 4, pages 1-48. ACM, December 2021.</p>
<ul>
<li><a href="https://github.com/secure-compilation/different_traces">Coq development</a></li>
<li>A short version appeared at In <a href="https://www.etaps.org/2020/esop">29th European Symposium on Programming (ESOP)</a>
and was <strong>Nominated for EATCS Award for the best ETAPS 2020 paper in theoretical computer science.</strong></li>
</ul></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>,
<a href="https://matteobusi.github.io/">Matteo Busi</a>, and
<a href="https://scholar.google.com/citations?user=P_acVKwAAAAJ&hl=en">Stelios Tsampas</a>.
<strong><a href="https://arxiv.org/abs/2006.14969">Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly</a></strong>.
In <a href="https://conf.researchr.org/home/aplas-2021">19th Asian Symposium on Programming Languages and Systems (APLAS)</a>. October 2021.</p></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>,
<a href="https://haselwarter.org">Philipp G. Haselwarter</a>,
<a href="https://dcc.fceia.unr.edu.ar/~erivas">Exequiel Rivas</a>,
<a href="https://antoinevanmuylder.github.io">Antoine Van Muylder</a>,
<a href="https://theowinterhalter.github.io">Théo Winterhalter</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://github.com/kyoDralliam">Kenji Maillard</a>, and
<a href="https://cs.au.dk/~spitters">Bas Spitters</a>.
<strong><a href="https://eprint.iacr.org/2021/397/20210526:113037">SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq</a></strong>.
In 34th IEEE Computer Security Foundations Symposium (CSF), pages 608–622. June 2021.
<strong>Distinguished Paper Award.</strong></p>
<ul>
<li><a href="https://github.com/SSProve/ssprove">Coq development</a></li>
</ul></li>
<li><p><a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>.
<strong><a href="https://catalin-hritcu.github.io/publications/catalin_habil.pdf">The Quest for Formally Secure Compartmentalizing Compilation</a></strong>
Habilitation Thesis, ENS Paris, January 2019.</p></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://people.mpi-sws.org/~dg/">Deepak Garg</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://people.mpi-sws.org/~marcopat/">Marco Patrignani</a>, and
<a href="http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/">Jérémy Thibault</a>.
<strong><a href="http://arxiv.org/abs/1807.04603">Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation</a></strong>.
In <a href="https://web.stevens.edu/csf2019/index.html">32nd IEEE Computer Security Foundations Symposium (CSF)</a>, June 2019.
<strong>Distinguished Paper Award</strong>.</p>
<ul>
<li><a href="https://github.com/secure-compilation/exploring-robust-property-preservation">Coq development</a></li>
<li>A previous extended abstract was called
<a href="https://arxiv.org/abs/1710.07309">Robust hyperproperty preservation for secure compilation</a></li>
</ul></li>
<li><p><a href="https://dblp.org/pers/hd/a/Abate:Carmine">Carmine Abate</a>,
<a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://www.cs.virginia.edu/~ans5k/">Ana Nora Evans</a>,
<a href="https://github.com/GuglielmoS">Guglielmo Fachini</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://github.com/theolaurent">Théo Laurent</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>,
<a href="http://www.stronati.org/">Marco Stronati</a>, and
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="https://arxiv.org/abs/1802.00588">When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise</a></strong>.
In <a href="https://ccs2018.sigsac.org/">25th ACM Conference on Computer and Communications Security (CCS)</a>, October 2018.</p>
<ul>
<li><a href="https://github.com/secure-compilation/when-good-components-go-bad">Coq proofs</a></li>
<li>A previous extended abstract was called <a href="https://arxiv.org/abs/1710.07308">Formally secure compilation of unsafe low-level components</a></li>
</ul></li>
<li><p><a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>, and
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>.
<strong><a href="http://arxiv.org/abs/1705.07354">The Meaning of Memory Safety</a></strong>.
In 7th International Conference on Principles of Security and Trust (POST), pages 79–105, April 2018.</p>
<ul>
<li><a href="https://github.com/arthuraa/memory-safe-language">Coq proofs</a></li>
</ul></li>
<li><p><a href="http://yannis.computer/">Yannis Juglaret</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="https://github.com/engboris">Boris Eng</a>, and
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>.
<strong><a href="http://arxiv.org/abs/1602.04503">Beyond Good and Evil: Formalizing the Security Guarantees
of Compartmentalizing Compilation</a></strong>.
In <a href="http://csf2016.tecnico.ulisboa.pt/">29th IEEE Symposium on Computer Security Foundations (CSF)</a>, pages 45-60. IEEE Computer Society Press, July 2016.</p>
<ul>
<li><a href="https://github.com/secure-compilation/beyond-good-and-evil">Auxiliary materials including Coq proofs</a></li>
</ul></li>
<li><p><a href="http://yannis.computer/">Yannis Juglaret</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>,
<a href="https://stackoverflow.com/users/237428/antal-spector-zabusky">Antal Spector-Zabusky</a>, and
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="http://arxiv.org/abs/1510.00697">Towards a Fully Abstract Compiler Using Micro-Policies:
Secure Compilation for Mutually Distrustful Components</a></strong>.
Technical Report, arXiv:1510.00697, October 2015.</p></li>
<li><p><a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="http://www.maximedenes.fr/">Maxime Dénès</a>,
<a href="http://scholar.princeton.edu/nick/home">Nick Giannarakis</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>,
<a href="https://stackoverflow.com/users/237428/antal-spector-zabusky">Antal Spector-Zabusky</a>,
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="http://prosecco.gforge.inria.fr/personal/hritcu/publications/micro-policies.pdf">Micro-Policies: Formally Verified, Tag-Based Security Monitors</a></strong>.
In <a href="http://www.ieee-security.org/TC/SP2015/">36th IEEE Symposium on Security and Privacy (Oakland S&P)</a>, pages 813-830. IEEE Computer Society, May 2015.</p>
<ul>
<li><a href="https://github.com/micro-policies/micro-policies-coq">Coq proofs</a></li>
</ul></li>
<li><p><a href="https://www.linkedin.com/in/udit-dhawan-016ab67">Udit Dhawan</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="http://nikos.vasilak.is">Nikos Vasilakis</a>,
<a href="https://www.seas.upenn.edu/~rafi">Raphael Rubin</a>,
<a href="https://www.linkedin.com/in/silviuchiricescu">Silviu Chiricescu</a>,
<a href="https://www.cis.upenn.edu/~jms">Jonathan M. Smith</a>,
<a href="https://en.wikipedia.org/wiki/Tom_Knight_(scientist)">Thomas F. Knight, Jr.</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>, and
<a href="https://www.seas.upenn.edu/~andre">André DeHon</a>.
<strong><a href="http://ic.ese.upenn.edu/abstracts/sdmp_asplos2015.html">Architectural Support for Software-Defined Metadata Processing</a></strong>.
In <a href="http://asplos15.bilkent.edu.tr/">20th International Conference on Architectural Support for Programming Languages
and Operating Systems (ASPLOS)</a>, pages 487-502. ACM, March 2015.</p></li>
<li><p><a href="http://arthuraa.net/">Arthur Azevedo de Amorim</a>,
<a href="https://galois.com/team/nathan-collins">Nathan Collins</a>,
<a href="https://www.seas.upenn.edu/~andre">André DeHon</a>,
<a href="https://www.irisa.fr/celtique/demange">Delphine Demange</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://www.irisa.fr/celtique/pichardie">David Pichardie</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>,
<a href="http://homepages.inf.ed.ac.uk/rpollack">Randy Pollack</a>, and
<a href="http://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>.
<strong><a href="http://arxiv.org/abs/1509.06503">A Verified Information-Flow Architecture</a></strong>.
Journal of Computer Security (JCS);
Special Issue on Verified Information Flow Security, 24(6):689–734,
December 2016.
(arXiv:1509.06503; supersedes POPL 2014 paper with the same name.)</p>
<ul>
<li><a href="https://github.com/micro-policies/verified-ifc">Coq proofs</a></li>
</ul></li>
<li><p><a href="http://prosecco.gforge.inria.fr/personal/karthik">Karthikeyan Bhargavan</a>,
<a href="http://antoine.delignat-lavaud.fr">Antoine Delignat-Lavaud</a>,
<a href="http://research.microsoft.com/en-us/um/people/fournet/">Cédric Fournet</a>,
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>,
<a href="https://jonathan.protzenko.fr">Jonathan Protzenko</a>,
<a href="https://www.normalesup.org/~ramanana">Tahina Ramananandro</a>,
<a href="https://www.microsoft.com/en-us/research/people/aseemr">Aseem Rastogi</a>,
<a href="http://research.microsoft.com/en-us/people/nswamy/">Nikhil Swamy</a>,
<a href="https://people.csail.mit.edu/wangpeng">Peng Wang</a>,
<a href="https://www.microsoft.com/en-us/research/people/santiago">Santiago Zanella-Béguelin</a>, and
<a href="https://github.com/jkzinzindohoue">Jean-Karim Zinzindohoué</a>.
<strong><a href="http://arxiv.org/abs/1703.00053">Verified Low-Level Programming Embedded in F*</a></strong>.
In <a href="https://conf.researchr.org/home/icfp-2017">22nd ACM SIGPLAN International Conference on Functional Programming (ICFP)</a>,
PACMPL, 1(ICFP):17:1–17:29, September 2017.</p></li>
</ul>
<h2 id="talks-on-secomp">Talks on SECOMP</h2>
<ul>
<li><a href="https://casa.rub.de/en/events/casa-summer-school">CASA Summer School 2023</a>: <a href="https://catalin-hritcu.github.io/talks/2023-08-14-CASA-Summer-School.pdf">slides</a> (2023-08-14)</li>
<li><a href="https://www.mpi-sp.org/">MPI-SP</a> Scientific Advisory Board visit: <a href="https://catalin-hritcu.github.io/talks/2023-05-11-SAB-MPI-SP-evaluation.pdf">slides</a> (2023-05-11)</li>
<li><a href="https://research-symposium.mpi-sws.org">MPI-SWS Research Symposium</a>: <a href="https://catalin-hritcu.github.io/talks/2023-03-10-MPI-SWS-Research-Symposium.pdf">slides</a> (2023-03-10)</li>
<li><a href="http://www.dagstuhl.de/21481">Dagstuhl Seminar 21481 on Secure Compilation</a>: <a href="https://catalin-hritcu.github.io/talks/2021-12-01-Formally-verifying-a-secure-compilation-chain-for-unsafe-C-components-at-Dagstuhl.pdf">slides</a> (2021-12-01)</li>
<li>Invited Talk at <a href="http://hotspot.compute.dtu.dk/hotspot2020.html">HotSpot Workshop</a>: <a href="https://catalin-hritcu.github.io/talks/2020-09-07-Journey-Beyond-Full-Abstraction-HotSpot.pdf">slides</a> and <strong><a href="https://youtu.be/hTLHDJGKKpc">video</a></strong> (2020-09-07)</li>
<li><a href="https://www.cis.mpg.de/graduate-programs/">CS @ Max Planck Open House</a>: <a href="https://prosecco.gforge.inria.fr/personal/hritcu/talks/2020-04-03-CS-at-Max-Planck-Open-House.pdf">slides</a> and <strong><a href="https://prosecco.gforge.inria.fr/personal/hritcu/talks/2020-04-03-CS-at-Max-Planck-Open-House.mp4">video</a></strong> (2020-04-03)</li>
<li><a href="http://gtmfsec.irisa.fr/">Formal Methods Working Group of GDR Security</a>: <a href="https://prosecco.gforge.inria.fr/personal/hritcu/talks/2020-01-30-When-Good-Components-Go-Bad-GDR-Security-Paris.pdf">slides</a> (2020-01-30)</li>
<li><a href="https://www.cse.chalmers.se/research/group/security/talk/css-talk27/">Chalmers Security Seminar</a>: <a href="https://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-06-27-Journey-Beyond-Full-Abstraction-CSF.pdf">slides</a> (2019-12-05)</li>
<li><a href="https://www.cse.chalmers.se/research/group/security/talk/css-talk27/">EPFL IC Colloquium</a>: <a href="https://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-12-05-When-Good-Components-Go-Bad-Chalmers.pdf">slides</a> (2019-09-26)</li>
<li><a href="https://web.stevens.edu/csf2019/">CSF 2019</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-06-27-Journey-Beyond-Full-Abstraction-CSF.pdf">slides</a> (2019-06-27)</li>
<li><a href="https://www.mpi-sws.org/">MPI-SWS</a>, Saarbrücken: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-05-23-When-Good-Components-Go-Bad-Saarbruecken.pdf">slides</a> (2019-05-23)</li>
<li>CASA-MPI Distinguished Lecture at Ruhr University Bochm: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-05-13-When-Good-Components-Go-Bad-Bochum.pdf">slides</a> (2019-05-13)</li>
<li>Habilitation defense, Inria Paris: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-01-29-Secure-Compilation-Habil.pdf">slides</a> (2019-01-29)</li>
<li><a href="https://popl19.sigplan.org/track/prisc-2019">PriSC @ POPL’19</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2019-01-13-Journey-Beyond-Full-Abstraction-PriSC.pdf">slides</a> (2019-01-13)</li>
<li><a href="https://www.sigsac.org/ccs/CCS2018/">CCS 2018</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2018-10-18-When-Good-Components-Go-Bad-CCS.pdf">slides</a> and <strong><a href="https://www.youtube.com/watch?v=Wwx-g513zFs">video</a></strong> (2018-10-18)</li>
<li><a href="https://fmse.info.uaic.ro/event/from-2018/">Working Formal Methods Symposium (FROM 2018)</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2018-06-20-Secure-Compilation-FROM.pdf">slides</a> (2018-06-20)</li>
<li><a href="https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=18201">Dagstuhl Seminar on Secure Compilation</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/2018-05-14-Secure-Compilation-Goals-and-Attackers-Dagstuhl.pdf">slides1</a> <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/talks/2017-01-15-What-Is-Secure-Compilation-SCM.pdf">slides2</a> (2018-05-14)</li>
<li>IRIF, Paris 7: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2018-02-26-Secure-Compilation-IRIF.pdf">slides</a> (2018-02-26)</li>
<li><a href="http://seminaire-dga.gforge.inria.fr/2017/CatalinHritcu_fr.html">SoSySec seminar: Software and Systems Security at IRISA</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2018-02-05-Secure-Compilation-Rennes.pdf">slides</a>; <strong><a href="https://videos-rennes.inria.fr/video/BkHzYy-jM">video</a></strong> (2018-02-05)</li>
<li><a href="http://popl18.sigplan.org/track/prisc-2018">PriSC’18 in LA</a>: <a href="https://popl18.sigplan.org/event?action-call-with-get-request-type=1&action253048efca6aee4547702963143c6170288=1&__ajax_runtime_request__=1&context=POPL-2018&event=prisc-2018-formally-secure-compilation-of-unsafe-low-level-components">slides</a> (2018-01-13)</li>
<li><a href="https://www.info.uaic.ro/bin/Main/">Infoiasi</a>: <a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2017-12-18-Secure-Compilation-Infoiasi.pdf">slides</a> (2017-12-18)</li>
<li><a href="http://www.ccs.neu.edu/home/weiss/esop18/pc.html">ESOP PC Workshop</a>: <a href="talks/2017-12-15-Secure-Compilation-ESOP-PC.pdf">slides</a> (2017-12-15)</li>
<li><a href="http://confiance-numerique.clermont-universite.fr/">Université Clermont Auvergne</a>:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2017-04-06-Secure-Compilation-Clermont-Ferrand.pdf">slides</a>
and <strong><a href="http://webtv.u-clermont1.fr/media-MEDIA170410150815297">video</a></strong>
(2017-04-06)</li>
<li><a href="https://vals.lri.fr/">LRI VALS seminar at University Paris-Sud</a>:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2017-03-17-Secure-Compilation-LRI.pdf">slides</a>
(2017-03-17)</li>
<li><a href="http://www-list.cea.fr/recherche-technologique/programmes-de-recherche/systemes-embarques/validation-et-verification">CEA List</a> seminar:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-12-13-Secure-Compilation-CEA.pdf">slides</a>
(2016-12-13)</li>
<li><a href="https://www.microsoft.com/en-us/research/lab/microsoft-research-redmond/">Microsoft Research Redmond</a>
security seminar:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-11-03-Secure-Compilation-MSR.pdf">slides</a>
(2016-11-03)</li>
<li><a href="http://gallium.inria.fr/">Inria Gallium</a>
<a href="http://gallium.inria.fr/seminar.html">seminar</a>:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-09-02-Secure-Compilation-Gallium.pdf">slides</a>
(2016-09-02)</li>
<li>Secure compilation meeting (informal) at Inria Paris:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-08-17-Secure-Compilation-Mini-Workshop-Paris.pdf">slides</a>
(2016-08-17)</li>
<li>ERC Starting Grant interview:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-05-31-Secure-Compilation-ERC.pdf">slides</a>
(2016-05-31)</li>
<li><a href="http://prosecco.gforge.inria.fr/events.php">Inria Prosecco Seminar</a>:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-03-02-Micro-Policies-Secure-Compilation-Prosecco.pdf">slides</a>
(2016-03-02)</li>
<li><a href="http://www.mpi-sws.org/">MPI-SWS</a>
<a href="http://www.mpi-sws.org/index.php?n=events/swscolloquium/program">Colloquium</a>:
<a href="http://prosecco.gforge.inria.fr/personal/hritcu/talks/2016-02-22-Micro-Policies-Secure-Compilation-MPI-SWS.pdf">slides</a>
(2016-02-22)</li>
</ul>
<h2 id="course-on-secure-compilation">Course on Secure Compilation</h2>
<ul>
<li><a href="http://prosecco.gforge.inria.fr/personal/hritcu/teaching/fosad2018/">Formally Secure Compartmentalizing Compilation</a> course at <a href="http://www.sti.uniurb.it/events/fosad18/">International School on Foundations of Security Analysis and Design (FOSAD)</a> in <a href="https://goo.gl/maps/oqzrpd6aMfr">Bertinoro, Italy</a> (2018-08-27)</li>
</ul>
<h2 id="related-projects">Related Projects</h2>
<!-- TODO: update to add SSITH/HOPE -->
<!-- TODO: add F* too -->
<ul>
<li><p><strong>Micro-Policies</strong> was a project aimed at showing how a rich
set of <em>micro-policies</em> – instruction-level security monitoring
mechanisms based on fine-grained metadata tags – can be described as
instances of a common dynamic monitoring framework, formalized and
reasoned about with unified verification tools, and efficiently
implemented using programmable metadata-propagation hardware. This
project was a collaboration between <a href="https://www.inria.fr/en/centre/paris">Inria Paris</a>,
<a href="https://www.cis.upenn.edu/">University of Pennsylvania</a>, <a href="https://www.csail.mit.edu/">MIT</a>, <a href="http://www.pdx.edu/computer-science/">Portland State University</a>,
and <a href="http://www.draper.com/">Draper Labs</a> (who have built <a href="https://www.youtube.com/watch?v=r5dIS1kDars">a RISC-V processor extended with
support for micro-policies</a>).
Micro-policies will be the main enabler for <em>efficient</em>
secure compilation in SECOMP.</p></li>
<li><p><strong><a href="http://www.crash-safe.org/">CRASH/SAFE</a></strong> was a DARPA-funded
project (2011-2014) that has undertaken the clean-slate co-design of
a secure network host including novel hardware, operating system,
programming language, and the systematic testing and verification of
key components. This large effort (≈40 people team) brought together
academia (<a href="https://www.cis.upenn.edu/">University of Pennsylvania</a>, <a href="https://www.seas.harvard.edu/computer-science">Harvard University</a>,
<a href="http://www.ccs.neu.edu/">Northeastern University</a>) and industry (<a href="http://www.baesystems.com/en/home">BAE Systems</a>). The
hardware mechanism we use for enforcing micro-policies originated in
CRASH/SAFE, where it was mainly used for information-flow control.</p></li>
</ul>
<!--
# Open Positions {#positions}
We are looking for excellent young researchers and students for
[PostDoc](#postdoc),
[Starting Researcher](#starting),
[PhD Student](#phd),
[Research Internship](#intern),
and [Research Engineer](#engineer) positions at [Inria Paris],
under the supervision of [Cătălin Hriţcu].
We can additionally support exceptional candidates for
permanent [Researcher](#cr) positions funded and awarded competitively by Inria.
More details about each of these positions are followed by some
**[general information](#general) about all the positions**.
## Postdoctoral Researcher Positions {#postdoc}
We are seeking exceptional candidates with a strong, internationally
competitive research track record in programming languages, formal
verification, or security. Particularly interesting for us is research
expertise in:
- formal verification in a proof assistant like Coq and
verified compilation in particular
- security foundations, e.g., reference monitoring, hyperproperties,
noninterference
Our most [recent](https://arxiv.org/abs/1807.04603)
[two](https://arxiv.org/abs/1802.00588) papers should provide
a good idea for the kind of research we're currently doing.
And [here is a (non-exhaustive) lists of potential research
topics](http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2019/secomp-2019.pdf).
We are open to new ideas though.
Candidates are expected to work collaboratively on project-relevant
topics and help advise students, but can also dedicate a part of their
time to their own independent projects.
Inria PostDocs are hired on 2 year contracts (extensible up 6 years)
and have a net monthly salary of €2122-2574.
For exceptional candidates with enough experience we can also discuss
about [Starting Researcher positions](#starting), who can propose and
follow their own research agenda and be fairly independent ([see
below](#starting)). Moreover, our team can also support such
exceptional candidates for permanent [Researcher](#cr) positions
funded and awarded competitively by Inria ([see below](#cr)).
## Starting Researcher Positions {#starting}
Starting Researchers can propose and follow their own research agenda
in secure compilation and be fairly independent.
We are seeking exceptional candidates with enough experience
(normally 2 years after PhD) and with a strong, internationally
competitive research track record in programming languages, formal
verification, or security.
Inria Starting Researchers are hired on 3 year contracts (extensible
up to 6 years) and earn €2348-3344 net each month, based on experience.
## Research Internships {#intern}
Our research internships are for highly motivated students at the MSc
level interested in getting a research immersion.
Successful internships normally result in a research publication at a good
international conference, and most often the MSc students we advise
[continue with a PhD](http://prosecco.gforge.inria.fr/personal/hritcu/students.html).
Research internships at Inria are very
flexible: they usually take between 3 and 6 months and can happen any
time of the year, not just in the summer.
We are especially interested in interns with previous exposure or strong desire to learn:
- functional programming (e.g., ML or Haskell);
- formal verification, especially in a proof assistant like Coq;
- security foundations or building secure systems;
- compilation (for imperative or functional languages);
For some potential topics, please
[have a look here](http://prosecco.gforge.inria.fr/personal/hritcu/publications/catalin_habil.pdf#page=81).
## PhD Student Positions {#phd}
We are seeking exceptional PhD candidates with a strong theoretical
background and eager to strike a balance between solving
deep foundational problems and achieving a practical impact by
building innovative security and verification tools.
We are particularly looking for candidates with some prior exposure to
state-of-the-art research in
- programming languages in general and functional programming in particular;
- verification in a proof assistant like Coq or [F\*]; verified compilation in particular
- security foundations (e.g. full abstraction, noninterference, and other security properties);
- building secure systems
In France, an MSc degree or equivalent is required for pursuing a
PhD. A PhD typically takes 3 years, and involves very little
to no course-work, so a strong theoretical background and previous
exposure to research are *pre-requisites* for a successful PhD. We
thus strongly encourage prospective PhD students without a strong
research background to follow at least the 2nd year of the [MPRI]
programme, an intensive, research-oriented MSc programme in computer
science taught by some of the best researchers in Paris.
The 2nd year in the [MPRI] ends with a 4.5 month
[research internship](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=stages),
and, as mentioned above, SECOMP is also looking for good interns.
For the more mathematically inclined, the 2nd year of the [LMFI]
MSc programme could also be an option.
[MPRI]: https://wikimpri.dptinfo.ens-cachan.fr/doku.php
[LMFI]: http://www.math.univ-paris-diderot.fr/m2lmfi/
Inria PhD students
[have a gross salary](https://www.inria.fr/en/institute/recruitment/offers/phd/faq#section4) of
€1958 per month for their first two years (€1586 net) and €2059
per month for their third year (€1668 net).
For more information about doing a PhD at Inria please consult
[Xavier Leroy's post on the topic](http://gallium.inria.fr/~xleroy/these.html)
or the
[official Inria FAQ](https://www.inria.fr/en/centre/paris/overview/offers/phd/faq).
## Research Engineer Positions {#engineer}
Are you an amazing hacker with an interest in state-of-the-art
security and verification tools? Are you experienced at programming in
C and/or ML and/or Haskell? Have you worked on a compiler before? Can
you envision hacking in Coq or [F\*]? If
you answered yes to some of these questions a Research Engineer
position on SECOMP could be well-suited for you.
Research Engineer positions are full time and moving to Paris is a
prerequisite. The net monthly salary is €2049-4265 based on experience.
These are temporary positions that can be prolonged up to
5-6 years, but we can also support excellent candidates for permanent
research engineering positions awarded competitively by Inria.
## Support for Permanent Researcher Positions at Inria {#cr}
[Researcher positions at Inria](https://www.inria.fr/en/institute/recruitment/offers/young-graduate-scientist/competitive-selection-crcn)
are permanent and are awarded via an extremely competitive contest.
Each Inria team can realistically support **at most one** candidate
in each yearly competition. If you are an exceptional candidate
interested in working in the [Prosecco] team,
the right time to get in touch with us is before the end of December.
Working in [Prosecco] as a PostDoc or Starting Researcher is not a
prerequisite but can also help in obtaining our support for a
permanent position.
[Prosecco]: http://prosecco.gforge.inria.fr/
These are permanent French civil servant positions that provide a lot
of scientific freedom and opportunities to grow. They are, however,
poorly payed, especially so compared to the cost of living in Paris.
The precise amounts vary based on experience and slowly increase with
time, but you can expect to have around €2000-2500 as your starting
net monthly salary. This can be topped up by bonuses (quite
substantial if obtaining an ERC grant for instance), consulting for
industry, etc.
## Flexible Starting Dates, but Long Hiring Process {#general}
The non-permanent positions above can be filled over several years,
so the starting dates are very flexible. Please be advised
though that the hiring process for Inria Prosecco normally takes 3+
months, irrespective of the level at which you apply (including
internships!). Getting in touch with us early enough is thus crucial.
(The "normal" hiring process takes 2+ months at Inria, but Prosecco gets
_special treatment_ in the form of an extra security clearance check,
that makes the whole process even longer!)
## Pardon My French
The language of communication in the SECOMP project is **English** and
normally one can get along just fine in Paris with only a minimal
level of French. Inria Paris provides free French courses to
interested students and researchers.
## How to Apply
If you are interested in applying for a position on the SECOMP project
please send an email to <[email protected]> including an up-to-date
curriculum vitae. For any questions please use the same email address.
-->
</div>
</body>
</html>