« BACK TO PROGRAM

Mixing formal methods to increase robustness against cyber-attacks

Laurent Voisin - Systerel

Already known as a specialist in applying formal methods for the development or the evaluation of safety critical systems, Systerel has recently expanded its usage of these mathematical technologies to cybersecurity. Its first concrete realisation is the production of a safe and secure open-source implementation of the OPC-UA protocol (available at https://s2opc.com). The OPC-UA protocol (IEC 62541) is dedicated to machine to machine communication and is a cornerstone of the Industry 4.0 initiative for smart manufacturing. By using concurrently two formal approaches, Systerel has reduced drastically the presence of specification and design flaws thanks to the B method, while code vulnerabilities have been eliminated with Frama-C and TrustInSoft Analyser. In this talk, we will present the rationale for the choice of using two different verification approaches and the advantages that they bring together.

Download this presentation

About Laurent Voisin

Laurent Voisin has been applying formal methods in industry for 20 years. He has gained experience in both using formal methods in actual development projects, which are now in daily use (e.g., many CBTC metro systems, KVB), and developing and maintaining the necessary tooling for such developments. He is a recognized expert of both the B method and the Event-B notation.