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 View Formal Call
Research Opportunity

Cryptography and Security


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 (, and the correctness proof shall be conducted in Easycrypt ( ). 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


Cluster / Centre

Computer Science / High-Assurance Software

Scientific Advisor

José Bacelar Almeida