INTERSCT. Round Table on formal methods to achieve ‘security-by-design

Venue

On 19 March 2026, from 13:00 until 17:00, INTERSECT is organising another INTERSCT. Round Table, this time on the use of formal methods during the design and development of high-tech systems that require a high level of confidence or even assurance with respect to the level of cyber security of the IoT Product being made.

Program

As software has become an integral part of the entire infrastructure and society at large, cybersecurity has become a fundamental requirement of all software design instead of only being considered when designing critical components. Additionally, the massive parallelization of software architectures, largely driven by the proliferation of IoT, means that the complexity of software systems has grown exponentially. 

Unlike sequential systems, where complexity grows linearly with the size of the software, parallel systems experience an exponential explosion in state-space. This complexity makes it nearly impossible for human developers to manually account for every interleaving of events or combination of states, thus creating a breeding ground for race conditions, deadlocks, and software vulnerabilities.

 Formal Methods, Model-Driven Engineering (MDE), combined with code generation, will provide significantly more secure software:

• Model-Driven Engineering techniques allow us to scale back the complexity of parallel systems. This reduction in complexity then in turn reduces the associated likeliness of introducing software vulnerabilities in the code.
• With the usage of formal verification tools we give watertight guarantees about the model-based code deployed in vulnerable systems. For example, model checking can be used to ensure that components strictly adhere to the communication protocol being used. Another example is the usage of theorem provers to give a mathematical proof of specific end-to-end requirements.
  
• By generating the actual low level code, we only have to ensure that the translation steps for the individual building blocks do not introduce vulnerability exploits instead of having to validate the entire code base. In turn, having to not worry about these “low hanging fruit” vulnerabilities, means that software engineers can redirect their focus to the much more complex and difficult to solve vulnerabilities of their software systems.

 Ultimately, we demonstrate that by moving the source of truth from the code to the model, we can build parallel systems that are not only easier to maintain but which inherently provide so called “Security by Design”.