Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Research Opportunity
Apply now Final Selection Minute View Formal Call
Research Opportunity

Cryptography and Security


Work description

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 (, and related verification tools (specifically, the Easycrypt proof assistant -- ). 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.

Academic Qualifications

Graduation degree in Informatics

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 13 Dec 2021 to 27 Dec 2021


Cluster / Centre

Computer Science / High-Assurance Software

Scientific Advisor

José Bacelar Almeida