2021-08-05-control-flow-integrity-for-remote-attestation.md 3.78 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
---
layout: job
title: Postdoc Position at CEA List - LSL
short_title: Postdoc Position
short: Control Flow Integrity for Remote Attestation
date: 05-08-2021
filled: false
keywords: control flow Integrity, remote attestation, runtime verification, static analysis, source code generation
---

11
12
# {{ page.short }}

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
[Full description](http://julien.signoles.free.fr/positions/postdoc-cfi.pdf)

#### Context: CEA List, Software Safety and Security Lab

[CEA List](http://www-list.cea.fr/en/)'s offices are located at the heart of Université Paris-Saclay, the
largest European cluster of public and private research. Within [CEA List](http://www-list.cea.fr/en/), the
Software Safety and Security Lab has an ambitious goal: help designers,
developers and validation experts ship high-confidence systems and software.

Systems in our surroundings are getting more and more complex, and we have built
a reputation for efficiently using formal reasoning to demonstrate their
trustworthiness through the design of methods and tools to ensure that
real-world systems can comply with the highest safety and security standards. In
doing so, we get to interact with the most creative people in academia and the
industry, worldwide.

Our organizational structure is simple: those who pioneer new concepts are the
ones who get to implement them. We are a fifty-person team, and your work will
have a direct and visible impact on the state of formal verification.

#### Work Description

Remote attestation allows some authorized parties to detect unexpected changes
(typically, performed by a malicious user) in a software component. It is
critical for trusted computing by providing strong guarantees about the software
component's integrity. Control flow integrity (CFI) is a security technique that
checks that a program follows its expected control flow when being executed, so
that the system is not being executed a piece of code in an unexpected way,
which could bypass some security checks, or would attempt some malicious
actions. Therefore, CFI can contribute to remote attestation by enforcing
integrity of the program's control flow during its execution.

The goal of the postdoc consists in designing a runtime verification
technique that enforces CFI for remote attestation during a
program execution. The works will be done in collaboration with researchers from
the [CEA List](http://www-list.cea.fr/en/)'s Communicating System Lab that will be in charge of providing the
necessary secure communications and system components. Therefore, the postdoc
work will focus on the code analysis, code instrumentation and monitoring
techniques that are necessary for generating an efficient CFI monitor from a
given source code. They will be implemented as a new plug-in for
[Frama-C](https://www.frama-c.com), the industrial-strength code analysis platform for C programs that is
developed in our lab. [Frama-C](https://www.frama-c.com) itself is developed in Ocaml.
55
56
57
More precisely, the following contributions are expected:

- designing a CFI-based technique for remote attestation;
Allan Blanchard's avatar
Allan Blanchard committed
58
59
- implementing this technique as a new [Frama-C](https://www.frama-c.com) plug-in;
- evaluating the implemented technique on concrete examples;
60
- design one or several new intermediate representations that would make these
Allan Blanchard's avatar
Allan Blanchard committed
61
  developments easier;
62
63
- (optionally:) designing and implementing optimization strategies to reduce the
  time overhead.
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

#### Qualifications

Knowledge in at least one of the following fields is required:

- Ocaml programming (at least, functional programming)
- C programming
- software security
- runtime verification
- static analysis
- program transformation


#### Application

This position will be filled as soon as possible; yet  a 3+-month procedure for
administrative and security purposes is required.

- [Julien Signoles](mailto:julien.signoles@cea.fr)