The 1^st International Symposium on Software Fault Prevention, Verification, and Validation

Kazuhiro Ogata received the B.S., M.S., and Ph.D. degrees in engineering from Keio University, in 1990, 1992, and 1995, respectively. He is currently a Professor with the Japan Advanced Institute of Science and Technology (JAIST), and the director with Research Center for Advanced Computing Infrastructure, JAIST. His research interest includes the applications of formal methods to systems, such as distributed systems and security protocols.

Title: Some Achievements of the International Joint Research Project "Formal Analysis and Verification of Post-quantum Cryptographic Protocols"

Abstract:

The international joint research project "Formal Analysis and Verification of Post-quantum Cryptographic Protocols" was carried out for April 2021 through March 2024. The main investigators are Santiago Escobar (Spain), Sedat Akleylek (Turkey), Ayoub Otmani (France) and me (Japan). Quantum era will be coming soon, when it is predicted that most of the currently used public-key cryptosystems become insecure because of the Shor's algorithm. Accordingly, cryptographers have been developing new cryptosystems that can replace the the currently used public-key cryptosystems and are resistant to the Shor's algorithm running on practical quantum computers that are expected to appear in the near future. Such new cryptosystems are called post-quantum cryptosystems, while the currently used public-key cryptosystems are called classical public-key cryptosystems. Some security protocols, such as TLS and SSH, have been revised such that post-quantum cryptosystems are used instead of classical public-key cryptosystems. The revised versions of TLS and SSH are called hybrid post-quantum TLS and hybrid post-quantum SSH because both classical public-key cryptosystems and post-quantum cryptosystems are used. In the international joint research project, some post-quantum cryptosystems, hybrid post-quantum TLS and hybrid post-quantum SSH have been formally analyzed. The formal analysis/verification of some post-quantum cryptosystems has been conducted with Maude, the one of hybrid post-quantum TLS has been conducted with Maude-NPA and CafeOBJ. and the one of hybrid post-quantum SSH has been conducted with CafeOBJ. I will talk about some achievements of the project.

Geguang Pu is a full professor of software engineering at East China Normal University. His research interests span the areas of software modeling, automated testing, and model checking. A common thread in Geguang's research is improving software reliability and trustworthiness by developing FM-based tools. Geguang joined East China Normal University in 2005 as an assistant professor and prior to that, he studied for Ph. D in Peking University. In July 2018, he was appointed as CEO of Shanghai Trusted Industrial Control Platform Co., Ltd for the technique transfer, where he is leading an effective engineering teams to develop the tool chains for software modeling, testing and verification, and these tools are used by more than 100 institutes/companies for structuring more reliable software systems.

Title: Developing the industrial-strength tools for modeling, testing and verification: A formal-methods perspective

Abstract:

FM-related techniques are very helpful to ensure the quality of software. For instance, the model checking technique has been successfully applied in hardware/software verification and it becomes the key element for EDA tool chains. In this talk, I will share the experiences of developing the industrial-strength tools for modeling, testing and verification from the formal methods perspective. We will show how to find the real problems about testing and verification from the industry and also show how the formal methods can guide to solve these problems by developing tools. We will illustrate our experiences and insights by three interesting tools under development. The first one is a formal modeling and verification tool for the formal verification of Interlock system of the train, that is key part of signal systems in railway. The second one is a testing tool for embedded systems, where the symbolic execution technique plays an important role. The last one is a new model checking solver for hardware verification, and its performance is tuned effectively by the new observations on the search process in the state space. These tools are successfully applied in our industry partners and their effectiveness is also proved by large scale examples. Last but not least, we will also share the lessons we have learned during the tool development.