Research Projects

Novel tools for Analysing Privacy Leakages
Provably Secure and Verifiable Systems
Verification of quantum cryptography
Cyber defence simulation of Internet of Things and Mobile Networks in the Cyber Range

PROJECT DESCRIPTIONS

Novel tools for Analysing Privacy LEakageS

Project funded by DARPA is executed by the Software Engineering and Information Systems chair.

Key persons:
- Marlon Dumas
- Luciano Garcia Banuelos
- Raimundas Matulevičius
- Jake Tom

Partner: Cybernetica AS
Project description: This project will demonstrate how to seamlessly add security analysis and optimization capabilities on top of business process management tools. The main outcome will be a tool that takes as input process models with privacy metadata (which it may compute itself), and analyzes these models to detect unintentional disclosures of private data and to quantify the leakage of private information through the outputs of the process. Where privacy leakages are discovered, the tool will identify possible counter-measures. The tool will generate reports that explain to data owners the maximum extent of possible leakage of their private data, making it easier to certify the system as secure and private. The project is funded by DARPA's BRANDEIS program and is performed in cooperation with Cybernetica.
Publications:
- Toots A., Tuuling R., Yerokhin M., Dumas M., García-Bañuelos L., Laud P., Matulevičius R., Pankova A., Pettai M., Pullonen P., Tom J. (2019) Business Process Privacy Analysis in PLEAK, Accepted at the 22nd International Conferene on Fundamental Approaches to Software Engineering (FASE 2019), Springer, LNCS 11424.
- Pullonen P., Tom J., Matulevičius R., Toots A., Privacy-Enhanced BPMN: Enabling Data Privacy Analysis in Business Process Models, Accepted at SoSyM (impact factor = 1.722), Springer 2019
- Dumas M., García-Bañuelos L., Laud P.: Disclosure Analysis of SQL Workflows, GraMSec@CSF 2018
- Pullonen P., Matulevičius R., Bogdanov D., PE-BPMN: Privacy-Enhanced Business Process Model and Notation. BPM 2017: 40-56
- Dumas M., García-Bañuelos L., Laud P.: Differential Privacy Analysis of Data Processing Workflows. GraMSec@CSF 2016: 62-79
Read more at project website

Provably Secure and Verifiable Systems

Project funded by Estonian Research Council is executed by the Security and Theoretical Computer Science chair.

Key persons:
- Dominique Unruh (PI)
- Helger Lipmaa
- Varmo Vene
- Vesal Vojdani
- Yangjia Li
- Tore Vincent Carstens
- Ehsan Ebrahimi Targhi

Project description: Sensitive and critical personal and business information is stored and managed by a multitude of electronic devices. Integrity and confidentiality of that data is threatened by software errors and malicious attacks. Yet, designing secure and verifiable systems is inherently difficult: The correct use of cryptography requires expert knowledge, the sheer complexity of the systems defies manual analysis; minor mistakes in implementation and analysis can completely destroy all security and correctness guarantees. For a high level of trust in a system, this system needs to be designed properly (using state-of-the-art cryptographic schemes where needed), and its proper operation (both security and correct behavior) needs to be proven (ideally with the help of a computer as humans are likely to make mistakes). In this project, we will study methods for designing secure systems (based on cryptographic primitives and protocols), and methods for computer-aided verification of their security and correctness.

Verification of quantum cryptography

Project funded by Air Force Office of Scientific Research, is executed by the Security and Theoretical Computer Science chair.

Key persons:
- Dominique Unruh (PI)
- Yangjia Li
- Tore Vincent Carstens

Project description: The security of cryptographic systems is normally ensured by mathematical proofs. Due to human error, these proofs may often contain errors, limiting the usefulness of said proofs. In recent years, methods for verifying cryptographic security proofs using computers have been developed (e.g., the EasyCrypt tool). However, there is an increasing demand for post-quantum secure protocols (protocols that stay secure if the attacker has a quantum computer); existing proof tools cannot handle post-quantum security. In this project, we will design theoretical foundations and tools (software) for developing and verifying security proofs on the computer, supporting post-quantum security and also allowing us to analyze protocols that use quantum communication. Our main approach is the design of a logic (quantum relational Hoare logic, qRHL) for reasoning about the relationship between pairs of quantum programs, together with a set of reasoning rules. This logic then allows us to formalize game-based proofs (game-based proofs are an established method for formulating cryptography proofs). The anticipated outcome is a tool that allows us to write and verify proofs written using qRHL, as well as proofs for selected protocols. The impact of this research is to improve the security of protocols in a quantum age, by removing one possible source of human error. In addition, it will impact the research community, by providing new foundations in program verification, and by providing cryptographers with new tools for the verification of their protocols.

Cyber defence simulation of Internet of Things and Mobile Networks in the Cyber Range

The research is funded by the Estonian Research Council through the RITA program, which aims to help the country become a smart subscriber and user of applied research. The budget of the program comes from the resources of the European Regional Development Fund and the Estonian state. The project is executed by UT Institute of Education, HPC center and Institute of Computer Science.

Key persons:
- Mario Mäeots (Institute of Education)
- Ilya Livenson (HPC center)
- Pelle Jakovits (Institute of Computer Science)

Partners: CybExer Technologies OÜ, NATO Cooperative Cyber Defence Centre (NATO CCDCOE), Thinnect OÜ and Elisa Eesti AS
Project description: The hidden side of ever increasing digitalization is the vulnerability of vital cyber systems and services to attacks. In order to prepare for and prevent possible threats, the Estonian Research Council commissioned an applied research project based on the needs of the Ministry of Defense and the Estonian Information System Authority (RIA). The objective of the project is to create a Cyber Range extension for conducting cyber defense exercises to improve the capabilities of Critical Infrastructure Providers to protect the society against potential threats arising with the use of emerging technologies, such as the Internet of Things and next-generation mobile connectivity technologies. A simulated Physical Village will be created that comprises multiple Critical Infrastructure applications that make use of different connectivity technologies for end devices. Also, virtual copies of the Physical Village will be created, where all the hardware components and communication links are virtualized, enabling training at a larger scale and at a lower cost. A Cyber Exercise Range extension will be designed and created that facilitates training to improve the safety of the society today and tomorrow, an environment, methods, and tools will be developed for protecting information systems of Critical Infrastructure.