Cryptography and Security
This grant is associated to the certified implementation of a cryptographic component for the generation of random numbers, to be integrated on the Password Manager adopted for the proof of concept of the PassCert project. The project will adopt the Jasmin programming language (https://github.com/jasmin-lang/jasmin), and related verification tools (specifically, the Easycrypt proof assistant -- https://www.easycrypt.info/trac/ ). Specifically, the project 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); - 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
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 13 Dec 2021 to 27 Dec 2021
Cluster / Centre
Computer Science / High-Assurance Software