Verification of SERUMS System, Eduard Baranov UCLouvain
Modern systems are often composed of multiple concurrent components based on various technologies. As a result, verification ensuring correctness and security of such systems is quite complex. Bugs and vulnerabilities can appear not only within a single component but during the interactions between components as well. Therefore, verification of separate components is not sufficient, the complete system must be checked. For a healthcare system, correctness and security are of utmost importance. Operating on medical data, an error could have catastrophic consequences. At the same time, high level of privacy is also required: the system must prevent data leaks.
One of the approaches we use to ensure correctness and security of the SERUMS system is Model Checking (MC) that provides mathematical guarantees about the properties satisfaction. The approach requires to build a model of the system in a formal language where no ambiguity or undefined behaviour are allowed. The desired properties are also formalised and checked on the model by exploring its reachable states. MC is an extremely powerful approach; however, it suffers from a so-called state space explosion: computational expensiveness makes the approach infeasible on large systems. In order to avoid the limitation, we use statistical model checking (SMC) – an alternative approach that combines ideas from MC with statistics.
Similar to MC, SMC operates on a system model, but instead of the exploration of all reachable states, SMC performs a large number of simulations until it ensures the satisfaction of the properties with a desired level of confidence. Being simulation-based, it has low time and memory requirements.
Within the project we have built a model of the SERUMS system in Uppaal tool that supports both MC and SMC. To represent the complete SERUMS system, we modelled each component of the system as well as their communications. This allows us to perform the analysis of local properties on subsystems and of global and communication related properties of the full model. To check the resilience against malicious attacks we build models of attackers that are given additional capabilities to interact with the model of the SERUMS system. We check whether the security properties are satisfied even with the presence of different attackers.
The SERUMS project allows us to demonstrate that formal methods such as SMC can be applied in large and complex projects, while projects can benefit from the mathematical guarantees provided by the formal methods.
