Formal Methods for Safe and Cybersecure Critical Systems

Designing reliable and Cybersecure critical systems requires great care and precision, as errors in their development can lead to catastrophic consequences, especially in sectors such as medicine, finance, aviation, space, and defense.
For example, consider cryptographic protocols that aim to secure communications on the Internet by relying on cryptographic primitives. These protocols are essential for various applications, including online shopping, banking transactions, electronic voting, and securing government communications and vital infrastructure. However, designing error-free cryptographic protocols can be challenging as demonstrated by the discovery of a critical flaw 17 years after the original publication of the famous Needham-Schroeder public-key protocol. Even today, many flaws are still found in current cryptographic protocols, resulting in financial losses and eroding user confidence. The analysis of cryptographic protocols is very complex because the set of scenarios to consider can be infinite.
Thanks to their solid mathematical foundation, Formal Methods make it possible to manage endless possibilities, offering a powerful approach to validating cryptographic protocols and, more generally, critical systems.
This talk will explore how Formal Methods can be applied to various domains, such as cryptographic protocols and firewall configurations. Additionally, it will investigate the main challenges that Formal Methods techniques face in the validation process and discuss ongoing efforts to overcome these challenges.