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 new file mode 100644 index 0000000000000000000000000000000000000000..efd79a7744592818824bb9ae3b11fede1f387191 --- /dev/null +++ b/_jobs/2021-08-05-control-flow-integrity-for-remote-attestation.md @@ -0,0 +1,71 @@ +--- +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 +--- + +[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. + +#### 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) 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 new file mode 100644 index 0000000000000000000000000000000000000000..4f2312c1a18f4fabc3a81c2a64b94592c95d079c --- /dev/null +++ b/_jobs/2021-08-05-designing-compilation-techniques-for-improving-efficiency-of-e-acsl.md @@ -0,0 +1,71 @@ +--- +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 +--- + +[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. + +The main goal of this position is to improve [E-ACSL](https://www.frama-c.com/fc-plugins/e-acsl.html). + +#### 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) diff --git a/_jobs/2021-08-05-outline-runtime-assertion-checking.md b/_jobs/2021-08-05-outline-runtime-assertion-checking.md new file mode 100644 index 0000000000000000000000000000000000000000..fddd890386f38a24354b7358cb1d886c067528f1 --- /dev/null +++ b/_jobs/2021-08-05-outline-runtime-assertion-checking.md @@ -0,0 +1,79 @@ +--- +layout: job +title: Postdoc Position at CEA List - LSL +short_title: Postdoc Position +short: Outline Runtime Assertion Checking +date: 05-08-2021 +filled: false +keywords: runtime assertion checking, outline monitoring, compilation, source code generation +--- + +[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. + +#### 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)