Commit 954a8661 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Removed old positions and added position skeleton

parent 682a6550
......@@ -34,7 +34,7 @@ theme: minima
plugins: [jekyll-feed, jekyll-paginate, jekyll-category-pages]
include: ['html']
exclude: ['download']
exclude: ['download',_jobs/skeleton.md]
collections:
fc-plugins:
......
---
layout: job
title: Postdoc Position at CEA LIST - LSL
position: Postdoc
duration: 18-months
short: Extensive Code Security Analyses for Frama-C
posted: 06-04-2020
keywords: information flow security, abstract-interpretation, runtime verification
---
#### Context: CEA LIST, Software Security and Reliability Lab
The Software Security and Reliability Laboratory (LSL) at CEA LIST has an ambitious goal: help
designers, developers and validation experts ship high-condence systems and software. Objects in
our surroundings are getting more and more complex, and we have built a reputation for efficiently
using formal reasoning to demonstrate their trustworthiness. Within the CEA LIST Institute, LSL is
dedicated to inventing the best possible means to conduct formal verification. In collaboration with the
most creative people in academia and the industry, we design methods and tools that leverage innovative
approaches to ensure that real-world systems can comply with the highest safety and security standards
Our organizational structure is simple: those who pioneer new concepts are the ones who get to
implement them. We are a forty-person team, and your work will have a direct and visible impact on
the state of formal verification. CEA LIST's offices are located at the heart of Campus Paris Saclay, in
the largest European cluster of public and private research.
#### Work Description
Our team develops Frama-C (http://frama-c.com), a code analysis platform for C programs which
provides several collaborative analyzers as plug-ins. Frama-C itself is developed in OCaml. Frama-C
allows the user to annotate C programs with formal specications written in the ACSL specification
language. Frama-C can then ensure that a C program satisfies its formal specification by relying on
several techniques including abstract interpretation (plug-in Eva), weakest preconditions calculus
(plug-in Wp), and runtime verification (plug-in E-ACSL).
In the context of the newly accepted H2020 European project ENSURESEC (2020-2022) that aims
at protecting e-commerce, we plan to use Frama-C for detecting security threats in cyber interfaces
such as middleware, cryptographic libraries, or communication protocol implementations. The postdoc
researcher will adapt existing Frama-C plug-ins and/or design new ones for that purpose.
Among others, one important topic is information flow security in order to detect information leakage.
In that respect, possible solutions include:
- abstract interpretation through the design of a new Eva's abstract domain ;
- runtime verification by taking advantage of unused bits of the E-ACSL's shadow memory state ;
- extending and improving the dedicated hybrid information flow plug-in SecureFlow that allows
the user to combine static and dynamic verifcations to check non-interference.
Another topic of interest is access control enforcement checking that could be performed within
and/or the MetACSL plug-in that allows the user to specify high-level global program
properties such as security policies. Designing a dedicated plug-in could also be an option.
The postdoc researcher should formalize and implement his/her solutions, prove their soundness and
evaluate them on realistic use cases (e.g. provided by Ensuresec's industrial partners).
#### Application
Knowledge in at least one of the following fields is required:
- program development (Ocaml, C)
- semantics of programming languages
- information flow security
- compilation
- static analysis
- runtime verification
- formal methods for program verification
**Salary:** academic competitive (vary *w.r.t.* diploma and former experience)
**Availability:** 2<sup>nd</sup> semester 2020; a 3-month procedure for administrative and security purposes is required
**Contact:** Julien Signoles (`julien.signoles@cea.fr`)
\ No newline at end of file
---
layout: job
title: Permanent Research Engineer Position at CEA LIST - LSL
position: Reseach Engineer
duration: Permanent
short: Join the development team of Eva
posted: 26-06-2020
keywords: formal-methods, abstract-interpretation, static-analysis
---
The LSL laboratory at CEA LIST, located near Paris, France, is opening a new
permanent Research Engineer position in formal methods.
If you are interested in joining the development team of Eva, the Frama-C plugin
based on abstract interpretation, please consider applying.
More details are available below.
#### LSL Laboratory
The LSL Software Security Laboratory helps developers and validation experts
ship high-confidence software and systems. With everyday objects getting more
and more complex, we have built a reputation for efficiently applying formal
reasoning techniques to establish their trustworthiness.
As part of the CEA LIST Institute, at the heart of Campus Paris Saclay, teams at
LSL are researching the best possible means to conduct formal verification. We
design tools such as Binsec, Frama-C and UNISIM, that ensure production-level
systems can comply with the highest safety and cybersecurity expectations. And
in doing so, we get to interact with the most creative people in academia and
the industry.
Our team comprises about 30 permanent research engineers, plus a dozen PhDs and
postdocs. Our organizational structure is simple: those who pioneer new concepts
are the ones who get to lead their implementation. Your work will have a direct
and visible impact on the state of software verification.
#### Role
We need you to help us develop Frama-C's abstract interpretation plugin, both by
improving current analyses and by designing new approaches. You will contribute
to growing the community of users, handling feedback and helping real people
solve real problems.
You will take an active role in research and development activities and
industrial partnerships, alongside other members of the laboratory. This can
include writing proposals, managing projects, writing and reviewing code,
publishing papers, as well as attending scientific and technical events
worldwide (or, you know, their remote streams, during a pandemic lockdown).
#### Requirements
- Background in abstract interpretation and theory of programming languages.
- Hands-on experience with significant OCaml developments - other languages
are fine too, but you'll need to convince us you can adapt in a snap.
- Self-organized, with an ability to prioritize effectively.
- Team-minded - you know when to let someone else take the lead.
#### Pluses
Various areas of our overall activity can also benefit from specific skillsets.
- Break new ground with us:
* Hands-on expertise in the fields of software security.
* Flawless understanding of C, C++, assembly languages or hardware interfaces.
- Precision-drive our infrastructure:
* Technical administration of Linux environments and development tools.
* Robust grasp of IT service management processes.
- Help us spread the word:
* Strong proficiency in foreign languages.
* A knack for writing and editing longform content.
#### Applying
If you're interested in joining LSL, send us an email to share what inspires
you, and why you think you are a good match for the team. Send it with a resume
to `david.buhler@cea.fr` and `thibaud.antignac@cea.fr`.
---
layout: job
title: <Postdoc, Permanent, Intern, ...> Position at CEA LIST - LSL
position: <Postdoc, Research Engineer, Intern, ...>
duration: <N-months, Permanent>
short: <short description (visible on "contact" page)>
posted: 06-04-2020
keywords: <a few keywords>
---
#### Context: CEA LIST, Software Security and Reliability Lab
The Software Security and Reliability Laboratory (LSL) at CEA LIST has an ambitious goal: help
designers, developers and validation experts ship high-confidence systems and software. Objects in
our surroundings are getting more and more complex, and we have built a reputation for efficiently
using formal reasoning to demonstrate their trustworthiness. Within the CEA LIST Institute, LSL is
dedicated to inventing the best possible means to conduct formal verification. In collaboration
with the most creative people in academia and the industry, we design methods and tools that
leverage innovative approaches to ensure that real-world systems can comply with the highest
safety and security standards
Our organizational structure is simple: those who pioneer new concepts are the ones who get to
implement them. We are a forty-person team, and your work will have a direct and visible impact on
the state of formal verification. CEA LIST's offices are located at the heart of Campus Paris Saclay,
in the largest European cluster of public and private research.
#### Work Description
<Description>
#### Application
Knowledge in at least one of the following fields is required:
<list field>
**Salary:** < ... >
**Availability:** < ... > ; a 3-month procedure for administrative and security purposes is required
**Contact:** First Last (`first.last@cea.fr`)
\ No newline at end of file
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