Cryptography and Security
[Open]
Work description
Each grant of this announcement is associated to the certified implementation of a cryptographic component to be integrated on the Password Manager adopted for the proof of concept of the PassCert project. The identified components concern the password generation mechanism and the encrypted secret store. The adopted programming language is Jasmin (https://github.com/jasmin-lang/jasmin), and the correctness proof shall be conducted in Easycrypt (https://www.easycrypt.info/trac/ ). Specifically, these projects shall comprise: - Implementation of a reference implementation in Jasmin, based on a specification from a standard or a research article; - Refinement of the code to an high-speed implementation, possibly resorting to vectorised instructions extensions (e.g. AVX2); - Prove correctness guaranties in Easycrypt; - Write the activity report. The above task ask for the application and development of basic concepts and techniques from the area of Informatics Engineering, typically lectured on nuclear courses from MSc programs in Informatics.
Academic Qualifications
Graduation degree in Informatics, or equivalent
Minimum profile required
- Graduation mark of 12 or higher.
Preference factors
- Experience in low-level programming (assembly) - Experience in program verification based on interactive theorem provers (e.g. Coq, Easycrypt); - Previous contact with the tools adopted by the PassCert project (Jasmin language, and EasyCrypt theorem prover). - Acquaintance in english language.
Application Period
Since 31 Mar 2021 to 14 Apr 2021
[Open]
Cluster / Centre
Computer Science / High-Assurance Software