From 456945882be19aba61284af4faef4335d8387824 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Fri, 6 Aug 2021 08:49:07 +0200 Subject: [PATCH] [Jobs] Complete runtime verification jobs desc --- ...ntrol-flow-integrity-for-remote-attestation.md | 9 +++++++++ ...chniques-for-improving-efficiency-of-e-acsl.md | 15 ++++++++++++++- ...21-08-05-outline-runtime-assertion-checking.md | 15 +++++++++++++-- 3 files changed, 36 insertions(+), 3 deletions(-) diff --git a/_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md b/_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md index efd79a77..e764afd8 100644 --- a/_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md +++ b/_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md @@ -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 [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. +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 diff --git a/_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md b/_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md index 4f2312c1..79013aae 100644 --- a/_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md +++ b/_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md @@ -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 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 diff --git a/_jobs/2021-08-05-outline-runtime-assertion-checking.md b/_jobs/2021-08-05-outline-runtime-assertion-checking.md index ec5ebb51..b116720b 100644 --- a/_jobs/2021-08-05-outline-runtime-assertion-checking.md +++ b/_jobs/2021-08-05-outline-runtime-assertion-checking.md @@ -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 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 inline technique. Outline runtime verification consists in placing the monitor 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 monitor. While this technique is well known and often applied to monitoring of temporal properties, it was never applied to runtime 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 -- GitLab