Merge branch 'jobs/e-acsl-2021-0' into 'master'

2 postdoc and 1 PhD positions on runtime verification

See merge request !129

_events/framac-23.1.md

 ---
 layout: default
 date: "21-07-2021"
-event: Frama-C 23.1 (Vanadium)
+short_title: Frama-C 23.1 (Vanadium)
 title: Release of Frama-C 23.1 (Vanadium)
 link: /fc-versions/vanadium.html
 ---

_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md

+---
+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
+---
+
+# {{ page.short }}
+
+[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.
+More precisely, the following contributions are expected:
+
+- designing a CFI-based technique for remote attestation;
+- implementing this technique as a new [Frama-C](https://www.frama-c.com) 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
+
+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)

_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md

+---
+layout: job
+title: Postdoc Position at CEA List - LSL
+short_title: Postdoc Position
+short: Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C Programs
+date: 05-08-2021
+filled: false
+keywords: runtime assertion checking, compilation, source code generation, static analysis
+---
+
+# {{ page.short }}
+
+[Full description](http://julien.signoles.free.fr/positions/postdoc-eacsl.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
+
+Our team develops [Frama-C](https://www.frama-c.com), a code analysis platform for C programs which
+provides several analyzers as plug-ins. [Frama-C](https://www.frama-c.com) itself is developed in Ocaml.
+[Frama-C](https://www.frama-c.com) allows the user to annotate C programs with formal specifications
+written in the [ACSL](https://www.frama-c.com/html/acsl.html) specification language. [Frama-C](https://www.frama-c.com) can then ensure that a C program
+satisfies its formal specification by relying on several techniques including
+abstract interpretation, weakest preconditions calculus, and runtime assertion
+checking.
+
+[E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html) is the [Frama-C](https://www.frama-c.com) plug-in dedicated to runtime assertion checking. It
+converts a C program extended with formal annotations written in a subset of [ACSL](https://www.frama-c.com/html/acsl.html)
+into a new C program which checks the validity of annotations at runtime: by
+default, the program execution stops whenever one annotation is violated, or
+behaves in the same way than the
+input program if all its annotations are valid. One key feature of [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html) is the
+expressivity of its specification language which allows the user to describe
+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.
+
+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:
+
+- improve the current compilation scheme to reduce the memory footprint of the
+  generated code;
+- design new compilation techniques and/or adapt existing ones in order to
+  optimize the efficiency of the generated code;
+- design novel dedicated fast static analyses to minimize the generated code;
+- design one or several new intermediate representations that would make
+  these developments easier;
+- evaluate the benefits of these improvements on concrete benchmarks and/or
+  use cases.
+
+#### Qualifications
+
+Knowledge in at least one of the following fields is required:
+
+- Ocaml programming (at least, functional programming)
+- C programming
+- compilation
+- semantics of programming languages
+- static analysis
+- runtime verification
+- formal specification
+
+#### 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)

_jobs/2021-08-05-outline-runtime-assertion-checking.md

+---
+layout: job
+title: PhD Position at CEA List - LSL
+short_title: PhD Position
+short: Outline Runtime Assertion Checking
+date: 05-08-2021
+filled: false
+keywords: runtime assertion checking, outline monitoring, compilation, source code generation
+---
+
+# {{ page.short }}
+
+[Full description](http://julien.signoles.free.fr/positions/phd-outline-rac.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
+
+Our team develops [Frama-C](https://www.frama-c.com), a code analysis platform for C programs which
+provides several analyzers as plug-ins. [Frama-C](https://www.frama-c.com) itself is developed in Ocaml.
+[Frama-C](https://www.frama-c.com) allows the user to annotate C programs with formal specifications
+written in the [ACSL](https://www.frama-c.com/html/acsl.html) specification language. [Frama-C](https://www.frama-c.com) can then ensure that a C program
+satisfies its formal specification by relying on several techniques including
+abstract interpretation, weakest preconditions calculus, and runtime assertion
+checking.
+
+[E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html) is the [Frama-C](https://www.frama-c.com) plug-in dedicated to runtime assertion
+checking. It converts a C program extended with
+formal annotations written in a subset of [ACSL](https://www.frama-c.com/html/acsl.html) into a new C program which
+checks the validity of annotations at runtime: by default, the program execution
+stops whenever one annotation is violated, or behaves in the same way than the
+input program if all its annotations are valid. For doing so, [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html) performs an
+heavy implementation of the original source code to insert its own code that
+monitors the [ACSL](https://www.frama-c.com/html/acsl.html) annotations. This technique is usually referred to as
+*(online) inline runtime verification*. However,
+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*
+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
+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. 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
+
+Knowledge in at least one of the following fields is required:
+
+- Ocaml programming (at least, functional programming)
+- C programming
+- compilation
+- runtime verification
+- formal semantics of programming languages
+
+
+#### 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)