Cryptography and Security
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.
Graduation degree in Informatics, or equivalent
Minimum profile required
- Graduation mark of 12 or higher.
- 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.
Since 31 Mar 2021 to 14 Apr 2021
Cluster / Centre
Computer Science / High-Assurance Software