INTERSCT. Round Table on IoT Product Security

Join the INTERSCT. Round Table on IoT Product Security for a deep dive into the world of innovative (formaI) methods for IoT security.

The digitalisation of our society, including our industry, is progressing rapidly and more and more products are becoming connected using the Internet.

As software has become an integral part of the entire infrastructure and society at large, cyber security 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".

The programme starts at 13:00 with an informal lunch followed at 14:00 by an introduction to the use of formal methods for attaining high confidence/ assurance on the level of cyber security during the design and development of high tech systems by Bert de Jong and Flip van Spaendonck of Verum Software Tools followed by a short pitch by the participants. The program ends at 17:00.