PRR Project

Summary

Privacy Enhancing Technologies (PET) promise a new generation of ITC systems that change the current (in)balance between data utility and data monetizing versus the protection of personal data and fundamental rights. There is a wide range of emerging solutions that fall within the PET category. However, the goal of this project is to focus on cryptography-based solutions such as secure multiparty computation and zero-knowledge proofs.The field of cryptographic PETs is fast-moving, and we have today a new generation of cryptographic protocols that start to be mature for practical deployment. However, the software engineering aspect of such systems is far from ready: most solutions are currently available at TRL levels corresponding to research prototypes and the path to widespread deployment and legal/regulatory support promises to be long and not without difficulty. Moreover, the migration to post-quantum cryptography poses new challenges, and introduces new long-term security requirements that imply a re-evaluation of current proposals for personal data protection.Computer-aided cryptography is an area of research that supports the development of high-assurance cryptography implementations, in which formally verified security proofs are linked to functionally correct and efficient implementations that are resilient to attacks, including those targeting implementation and microarchitectural vulnerabilities such as transient execution CPU vulnerabilities (e.g. Spectre). Computer-aided cryptography has the potential to speed-up the convergence to secure and correct solutions that can be certified under adequate regulatory frameworks.This position will contribute to the development of a research agenda on computer-aided cryptography solutions for the development of high-assurance PET software in a post-quantum world. This includes developing new post-quantum cryptography-based PET protocols, systematizing good practices for secure implementation and deployment, extending the foundations of computer-aided cryptography to cover this new generation of protocols, and constructing verified security proofs and implementations of PET solutions.Its context is the Cryptography and Information Security Group at INESC TEC, integrated in the High-Assurance Software Laboratory. The group has a leading role in the Formosa Crypto initiative (Formosa-crypto.org) which brings together the developers and users of Computer-Aided Cryptography tools EasyCrypt and Jasmin, and hosts the high-assurance libjade post-quantum cryptography library.The position is thus centred on a research agenda for High-Assurance Cryptography-Based Privacy Enhancing Technologies to be developed at two levels: i) PET protocols, implementations and proofs; and ii) computer-aided cryptography foundations and tools, and building on INESCTEC previous work within Formosa Crypto: PET protocols, implementations and proofs : consider new post-quantum cryptography PET protocols with a strong potential for the development of highly efficient general zero-knowledge and multiparty computation protocols; develop high-speed formally verified implementations of these protocols; and construct machine-checked security proofs to support them. Consider also the migration to post-quantum cryptography of current internet technology, and the opportunity to improve the privacy aspects of currently deployed systems in this context. Computer-aided cryptography foundations and tools : develop sound reasoning principles and program logics coping with quantum capable adversaries; tighten tool integration to reap the most benefits from different verification technologies in the framework (e.g. type-system based compositional reasoning vs. deductive verification of specialised leaf-properties; well-defined contract and API specifications for leveraging third-party verification tools for maximum effectiveness); address modularisation and scalability issues hindering the verification of large PQC proposals, both at the implementation and reasoning levels.Candidates should match the following profile, being able to:?   make original contributions to the state of the art in cryptography or formal verification;?   lead research teams, in particular, in the context of collaborative research projects and the application project funding entities;?    supervise students in this area;?    participate in development and technology transfer activities towards achieving wider economic and societal impact.The ideal candidate will possess:Ph.D. in Computer Science or a related field.Proven tesearch track tecord in the areas of cryptography, formal verification and, ideally, computer-aided cryptography.Collaborative mindset: Ability to work effectively in interdisciplinary research teams and contribute to collaborative projectsand good communication skills.