With the increasing reliance on digital platforms, securing sensitive healthcare data is more critical than ever. Traditional penetration tests help identify vulnerabilities but cannot guarantee complete coverage. In this thesis, you will explore the potential of formal verification to strengthen authentication mechanisms in a healthcare portal. By using mathematical models, you’ll investigate whether it’s possible to prove that unauthorized access can be fully prevented, providing an extra layer of confidence in the system’s security.

💡Areas of Interest: Formal Verification, Security, Model Checking, .NET

This master’s thesis is part of the graduation project ‘Ontzorg de zorg, zorg voor jezelf!’. This project gives the healthcare sector a digital boost through automation and data analysis, allowing caregivers to spend more time with patients while enabling patients to take control of their personal health data.

One of our clients in the healthcare sector has developed a portal that facilitates communication between various organizations, reducing Dutch healthcare costs by millions of euros each year. Numerous individuals need to log into this portal daily, and it also supports system-to-system connections with their customers. Ensuring the security of sensitive health data is of utmost importance.

Our clients usually perform security assessments by hiring a security firm to conduct penetration tests on their systems. While effective, these pen-tests do not guarantee 100% coverage, and it’s always possible for some leaks to go undetected.

Recent advancements in formal verification have made it possible to mathematically prove certain properties of systems. This technique has been used in security-critical software to establish robustness (under certain assumptions). For example, the popular VPN software WireGuard has undergone of formal verification. See: Formal Verification – WireGuard

We are curious if such techniques are also applicable on the software that we develop. Our client’s portal involves several types of users, each requiring authentication. Additionally, inter-service communication is performed in various ways, all of which are encrypted and authenticated. The system consists of multiple front-ends, microservices, a large monolith, and system-to-system connections with third parties.

The Assignment

Your assignment is to apply formal verification to the authentication mechanism of our client’s system. For instance, you could aim to prove that it is impossible to gain unauthorized access to a part of the system. You will choose a suitable verification tool, which will likely involve creating a model of the system, selecting specific properties to verify, and formalizing them within your chosen tool. It is crucial to ensure that your model closely represents the actual system while minimizing assumptions.

About Info Support Research Center

We anticipate on upcoming and future challenges and ensures our engineers develop cutting-edge solutions based on the latest scientific insights. Our research community proactively tackles emerging technologies. We do this in cooperation with renowned scientists, making sure that research teams are positioned and embedded throughout our organisation and our community, so that their insights are directly applied to our business. We truly believe in sharing knowledge, so we want to do this without any restrictions.

Read more about Info Support Research here.

About Info Support

Info Support specializes in custom software, data/AI solutions, management, and training and is active in the Finance, Industry, Agriculture, Food & Retail, Mobility & Public, and Healthcare sectors. We provide solid and innovative solutions for complex and critical software issues. Our headquarters are located in Veenendaal (NL) and Mechelen (BE). At present, approximately 500 employees are employed by Info Support.

Info Support's working method is characterized by a number of core values: solidity, integrity, craftsmanship, and passion. These core values are intertwined in our work and the way we interact with each other.

To ensure that all employees are always up to date with the latest developments, Info Support has an in-house knowledge center that eagerly satisfies the hunger for more or different knowledge and skills.

B2 language proficiency in Dutch is required.