- Benjamin Smith (INRIA-Saclay)
- Maryline Laurent (SAMOVAR-Telecom SudParis)
The security of computer systems has always been essential. This is even more true today, when so much of our data is captured, and stored and treated remotely, and when automation and the Internet of Things have brought the penetration of computer systems and networks in our everyday lives and work to previously unimaginable levels.
Formal methods are an essential tool in building and maintaining high-assurance computer systems. Properly used, formal methods can help us to prevent design errors at every level, from the conception of distributed systems, through internet communication protocols, and software implementations, right down to hardware designs. Today, formal methods are used not only during the design of protocols, software, and hardware, where they can prevent fundamental design errors and prove the safety of systems, but also to analyse and find errors in systems that have already been deployed. They are therefore crucial not only in the development of new, trustworthy systems, but also in the maintenance and evolution of existing systems.
Moreover, building secure systems relies on designing – and enforcing in practice – scientific and technological means to support cybersecurity, resilience, and privacy preservation. If some techniques and scientific progress in each of these dimensions have been made so far, further investigations are still required. This is true on a one-dimension basis – for example, AI for efficient attack detection and countermeasure decision making – but also when considering several dimensions simultaneously, such as cybersecurity and resilience, or cybersecurity and privacy.