- JOB
- France
Job Information
- Organisation/Company
- CNRS
- Department
- Laboratoire lorrain de recherche en informatique et ses applications
- Research Field
- Computer scienceMathematics » Algorithms
- Researcher Profile
- First Stage Researcher (R1)
- Country
- France
- Application Deadline
- Type of Contract
- Temporary
- Job Status
- Full-time
- Hours Per Week
- 35
- Offer Starting Date
- Is the job funded through the EU Research Framework Programme?
- Not funded by a EU programme
- Is the Job related to staff position within a Research Infrastructure?
- No
Offer Description
The doctoral student will be hosted at Loria, Vandœuvre-lès-Nancy, France, will
join the Pesto team, and will interact with the members of the Formosa Crypto
group. Loria is a research unit (UMR 7503), common to CNRS, the University of
Lorraine, CentraleSupélec and Inria. Pesto is an Inria research team whose aim
is to build formal models and techniques, for computer-aided analysis and design
of security protocols (in a broad sense). The Formosa Crypto Group studies and
develops formally verified cryptography and its high-efficiency implementations,
in particular through the Jasmin and EasyCrypt tools.
The Jasmin low-level programming language is designed for implementing
high-assurance cryptographic libraries. It gives to programmers enough control
so as to reach optimal run-time performances and guarantee various safety and
security properties, such as “constant-time”, a widespread software
counter-measure against timing side-channel attacks. The compiler that produces
assembly from Jasmin programs is written and certified using the Coq proof
assistant: its correctness theorem justifies that results established at the
source level do apply at the assembly level.
The aim of this doctoral work is to study how compilation techniques, dedicated
to low-level programming, can streamline both tasks of writing low-level
efficient secure programs and of verifying them. Indeed today Jasmin programmers
must take care of many low-level details, usually automatically dealt with by
compilers: instruction selection and scheduling, spilling, etc. Moreover, as
shown by the various case studies that have been carried on until now, there is
a real practical difficulty of reusing parts of existing Jasmin programs or of
their proofs. Therefore this doctoral study aims on one hand to improve the
flexibility of the compiler without compromising the ability to finely control
low-level details when necessary, and without loosing the possibility of
precisely reasoning at the source level about behaviors of the target program
after compilation. On the other hand it will explore techniques of separate
compilation so as to make Jasmin programs more modular. These works about the
Jasmin language and its certified compiler shall be validated through large
realistic case studies.
Any previous experience with the Jasmin compiler is strongly recommended.
Where to apply
Requirements
- Research Field
- Computer science
- Education Level
- Master Degree or equivalent
- Research Field
- Mathematics
- Education Level
- Master Degree or equivalent
- Languages
- FRENCH
- Level
- Basic
- Research Field
- Computer science
- Years of Research Experience
- None
- Research Field
- Mathematics » Algorithms
- Years of Research Experience
- None
Additional Information
- Website for additional job details
Work Location(s)
- Number of offers available
- 1
- Company/Institute
- Laboratoire lorrain de recherche en informatique et ses applications
- Country
- France
- City
- VANDOEUVRE LES NANCY
- Geofield
Contact
- City
- VANDOEUVRE LES NANCY
- Website