ARITH 2023 Keynotes and Industrial Panel
Verified computer arithmetic for cryptography and elsewhere
John Harrison, Automated Reasoning Group, Amazon Web Services
I will describe my recent work at AWS developing a library of formally verified primitives for integer arithmetic, designed specifically for cryptographic applications. I will first describe the specific needs of this application domain, and in particular the importance of "constant-time" execution, a somewhat misleading term that I will try to explain accurately. I will then cover a few highlights of the algorithm design and formal verification, and compare with related approaches. I will also compare and contrast verifications in this domain with analogous proofs of floating-point algorithms that were a primary focus of my earlier work at Intel. While these domains have obvious dramatic differences, I will also show that some common intellectual themes and even specific classes of verification problems reappear in both settings.
John Harrison is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. He received his PhD from the University of Cambridge in 1996 and has worked on a variety of topics in automated theorem proving, formal verification and the design of numerical software, first in academia, then at Intel, and now at AWS. At Intel his primary focus was on floating-point algorithms, while more recently at AWS he has worked on the development of a formally verified and secure integer arithmetic library to support cryptographic applications. He is the primary developer of the HOL Light interactive theorem prover and author of the textbook "Handbook of Practical Logic and Automated Reasoning" (Cambridge University Press 2009).
“Formal for Arithmetic” and “Arithmetic for Formal”
Dr Pallab Dasgupta, Head of Research and Innovation, Formal Verification, Synopsys
This keynote explores the problem of Formal Verification of Complex Arithmetic Systems from two different directions. In one direction, traditional SAT/SMT engines for formal verification have been successfully deployed for proving data path implementations of various arithmetic functions, and Synopsys has a rich product portfolio in this domain. We venture into the formal verification of more complex arithmetic, such as deep neural networks, and study how such problems can be attacked with existing formal verification methods. In the other direction, for verification of real valued dynamical continuous systems such as analog designs and embedded software, the research community is looking beyond Boolean arithmetic to develop solvers. This includes the use of interval arithmetic, the ability to handle precision, and bringing the notions of sampling and approximations into the fold of formal verification.
Dr Pallab Dasgupta currently leads Research and Innovation on Formal Verification at Synopsys, Sunnyvale. He has more than 25 years of experience in formal verification technologies. He had been a professor and former Dean of Sponsored Research at the Indian Institute of Technology Kharagpur for many years, collaborating with many semiconductor and EDA companies, and heading one of the most well-known research groups on formal methods and EDA — one that has produced more than 250 research publications and generations of students who are formal verification practitioners today.
Industrial Panel
Brent Boswell (NVIDIA), Marius Cornea (Intel), Nicholas Knight (SiFive), David Lutz (Arm) and Alex Tenca (Synopsys)
Moderator: Theo Drane (Intel)
The topic of this panel is “The Impact of Machine Learning on Computer Arithmetic”. The growing importance of several new floating-point formats in Machine Learning (illustrated also by the IEEE P3109 Working Group activity or by the recent Open Compute Project Spec for FP8) calls for a discussion between leaders in industrial computer arithmetic. The discussion will include questions as
- Is this the final word in the future of machine learning number formats, with FP8 or even narrower formats?
- Are ML number formats part of a general trend toward more multi-precision and multi-accuracy platforms?
- Do any of the traditional floating-point hardware architectures make sense at such small bit-widths, or is it just fixed-point or look up tables?
- Will consumer demands for reproducibility force all ML hardware to be bit-identical?
- What is next for ML hardware?
- What does it take to prove correctness of ML hardware? What does this currently mean? What will, or should it mean?
- Formats like the OCP OFP8 have triggered new interest and highlighted the importance of computer arithmetic — have we fully exploited the opportunity and risen to its challenges?
The first part of this one-hour session will be dedicated to short presentations from the panelists.
The second part of the session will be for Q&A.
