ABZ 2024 – 10th International Conference on Rigorous State Based Methods

Keynote speakers

Here it is the list of keynote speakers (in alphabetic order by name).

David Basin @ ETH Zurich

Getting Electronic Payments Right


- Lecture partially supported by FME
Abstract
EMV is the international protocol standard for smartcard payments and is used in billions of payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s lengthy and complex specification, running over 2,000 pages. We have formalized various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new. For example, we discovered multiple ways that an attacker can use a victim's EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim's supposedly required PIN. Said more simply, the PIN on your EMV card is useless! We report on this, as well as follow-up work with an EMV consortium member on verifying the latest, improved version of the protocol, the EMV Kernel C-8. Overall our work provides evidence that security protocol model checkers like Tamarin have an essential role to play in developing real-world payment protocols and that they are up to this challenge.
Short Bio
David Basin is a full professor of Computer Science at ETH Zurich, since 2003. His research areas are Information Security and Software Engineering. He is the founding director of the ZISC, the Zurich Information Security Center, which he led from 2003-2011. He served as Editor-in-Chief of the ACM Transactions on Privacy and Security (2015-2020) and of Springer-Verlag's book series on Information Security and Cryptography (2008-present). He has co-founded three security companies, is on the board of directors of Anapaya Systems AG, and on various management and scientific advisory boards. He is an IEEE Fellow and an ACM Fellow.

Joe Kiniry @ Galois Inc.

What happens when the Government starts encouraging the use of formal methods?

Abstract
Over the past decade, US Government R&D RFPs have gone from never mentioning formal methods to frequently mandating formal methods. What's more, several recent White House reports have explicitly called out formal methods. For example, the 2016 NIST Interagency Report "Dramatically Reducing Software Vulnerabilities: Report to the White House Office of Science and Technology Policy" calls out formal methods as one of five key technical approaches critical to fulfilling the goals set forth in the US Government's 2016 Federal Cybersecurity R&D Strategic Plan.

More recently, in February 2024 the Office of the National Cyber Director (ONCD) published the report "Back to the Building Blocks: A Path Toward Secure and Measurable Software" in response to President Biden's National Cybersecurity Strategy and in alignment with Executive Order 14028 on Improving the Nation's Cybersecurity, issued in 2021. Its abstract states:
"In this report, the case is made that the technical community is well-positioned to drive progress on both strategic goals. First, in order to reduce memory safety vulnerabilities at scale, creators of software and hardware can better secure the building blocks of cyberspace. This report focuses on the programming language as a primary building block, and explores hardware architecture and formal methods as complementary approaches to achieve similar outcomes. Second, in order to establish accurate cybersecurity quality metrics, advances can be made to address the hard and complex research problem of software measurability. This report explores how such metrics can shift market forces to improve cybersecurity quality across the ecosystem. In essence, the US Government is now strongly recommending that nationally critical systems are written in safe programming languages, models and implementations of critical components must be formally assured, and that code should run on security-centric hardware architectures."
This talk reflects upon this evolution over the past ten years from my point of view as a PI of dozens of major formal methods-centric R&D programs for the Government and industry. Why has there been such an uptick in interest? What are the R&D challenges that lie ahead? How might we, as a community, prioritize R&D activities for transition? What can the ABZ community learn from this arc? What's next?
Short Bio
Dr. Joe Kiniry is a Principal Scientist at Galois and is the CEO and Chief Scientist at Free & Fair. Over the past twenty-five years he has been everything from a tenured professor at several universities to a founder and chief scientist or CTO at several companies. He has been involved in security in some fashion since the early 80s when he hacked and wrote video games on 8 bit computers. These days, his day job is applying formal methods to nationally critical systems and trying to help the worlds’ elections and democracies be more trustworthy.

Maurice ter Beek @ ISTI, CNR

Formal Methods and Tools applied in the railway domain


- Lecture partially supported by FME
Abstract
ABZ and other state-based formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single language or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the current safety standards in the railway industry, but railway engineers often lack the knowledge to transform their semi-formal models into formal models, with a precise semantics, to serve as input to formal methods tools. We share the results of performing empirical studies in the railway domain, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying rigorous state-based methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to drive future research towards facilitating further synergies between - on the one hand - researchers and developers of ABZ and other state-based formal methods and tools, and - on the other hand - practitioners from the railway industry.
Short Bio
Maurice ter Beek is senior researcher at CNR-ISTI (Pisa, Italy) where he heads the Formal Methods and Tools lab. He obtained his Ph.D. at Leiden University (The Netherlands). He has authored over 150 peer-reviewed papers, edited over 30 proceedings and special issues of journals, and serves on the editorial boards of the journals Formal Aspects of Computing, International Journal on Software Tools for Technology Transfer, Journal of Logical and Algebraic Methods in Programming, Science of Computer Programming, PeerJ Computer Science and ERCIM News. His research interests are formal methods and model-checking tools for the specification and verification of safety-critical software systems and communication protocols, focusing in particular on applications in software product line engineering and railway systems. He is member of the Steering Committees of the COORDINATION, ETAPS, FMICS (currently chair), iFM and SPLC conference series, and regularly serves on the PC of relevant formal methods and software product line conferences like FM, FMICS, iFM, SPLC and VaMoS, all of which he also chaired, and ABZ, FASE, FormaliSE, SEFM and SPIN. He is board member of Formal Methods Europe (FME).