Commit 45694588 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[Jobs] Complete runtime verification jobs desc

parent 6e92f428
Pipeline #37107 passed with stages
in 5 minutes and 28 seconds
...@@ -50,6 +50,15 @@ techniques that are necessary for generating an efficient CFI monitor from a ...@@ -50,6 +50,15 @@ 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 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 [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. developed in our lab. [Frama-C](https://www.frama-c.com) itself is developed in Ocaml.
More precisely, the following contributions are expected:
- designing a CFI-based technique for remote attestation;
- implementing this technique as a new \framac plug-in
- evaluating the implemented technique on concrete examples
- design one or several new intermediate representations that would make these
developments easier
- (optionally:) designing and implementing optimization strategies to reduce the
time overhead.
#### Qualifications #### Qualifications
......
...@@ -49,7 +49,20 @@ powerful safety and security properties. Another key feature is the efficiency ...@@ -49,7 +49,20 @@ powerful safety and security properties. Another key feature is the efficiency
of the generated code which relies on a custom memory library of the generated code which relies on a custom memory library
and dedicated static analyses. and dedicated static analyses.
The main goal of this position is to improve [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html). However [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html) can still be
improved in many ways in order to extend its expressivity and to reduce its
memory and time overheads. To reach this goal, (s)he shall make several
contributions, for example regarding some of the following objectives:
- improving the current compilation scheme to reduce the memory footprint of the
generated code;
- designing new compilation techniques and/or adapt existing ones in order to
optimize the efficiency of the generated code;
- designing novel dedicated fast static analyses to minimize the generated code;
- designing one or several new intermediate representations that would make
these developments easier
- evaluating the benefits of these improvements on concrete benchmarks and/or
use cases.
#### Qualifications #### Qualifications
......
...@@ -50,7 +50,8 @@ monitors the [ACSL](https://www.frama-c.com/html/acsl.html) annotations. This te ...@@ -50,7 +50,8 @@ monitors the [ACSL](https://www.frama-c.com/html/acsl.html) annotations. This te
depending on the context of application, this heavy instrumentation may lead to depending on the context of application, this heavy instrumentation may lead to
prohibitive memory and runtime overheads, as well as security concerns. prohibitive memory and runtime overheads, as well as security concerns.
The goal of the PhD consists in designing and implementing an *outline runtime verification technique* The goal of the PhD consists in designing and implementing an *outline runtime
verification technique*
for [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html), compatible with the existing for [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html), compatible with the existing
inline technique. Outline runtime verification consists in placing the monitor inline technique. Outline runtime verification consists in placing the monitor
in an external entity (e.g., another thread, or a remote server) for limiting in an external entity (e.g., another thread, or a remote server) for limiting
...@@ -58,7 +59,17 @@ the instrumentation to communication activities with the remote ...@@ -58,7 +59,17 @@ the instrumentation to communication activities with the remote
monitor. While this technique is well known and often monitor. While this technique is well known and often
applied to monitoring of temporal properties, it was never applied to runtime applied to monitoring of temporal properties, it was never applied to runtime
assertion checking, which raises several challenges regarding the data that need assertion checking, which raises several challenges regarding the data that need
to be monitored. to be monitored. The expected contributions are:
- designing a new instrumentation scheme for outline runtime assertion checking;
- designing a new internal representation for the monitor, usable for both
inline and outline runtime assertion checking;
- implementing the new representation and the new instrumentation scheme inside
[E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html);
- evaluating the new outline runtime assertion checker on representative
benchmarks and/or use cases;
- (optionally:) designing and implementing optimization strategies to reduce the
time and/or memory overheads
#### Qualifications #### Qualifications
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment