Lisp Ireland Meetup @ Stripe Dublin

Please join us for the monthly Lisp Ireland meetup hosted at the Stripe office in Dublin. This month, Rafael Sadykov will talk about using ACL2 for the hardware verification of cryptographic chips.

To attend, you must register here in accordance with Stripe’s security policy. If you only RSVP on Meetup.com, you will be asked to register at the door when you arrive.

Abstract:
This presentation focuses on ACL2 for the hardware verification of cryptographic chips that utilize the Feistel block ciphers. ACL2, a powerful theorem prover and a variant of Common Lisp, is instrumental in verifying the correctness and security of hardware designs. The presentation delves into methodologies for ensuring that cryptographic hardware (designed in Verilog) meets rigorous safety and performance standards. It highlights the challenges and solutions in hardware verification, describing the role of formal methods in achieving low-latency bug-free cryptographic devices.

Speaker:
Rafael Sadykov is a mathematician with a degree in Fundamental Mathematics and Mechanics, an M.Sc. in Financial Mathematics and a PhD (ABD) in Computer Science. His work spans formal software verification, blockchain design, smart contract verification, and ML. He's also developed courses in software quality, formal verification, and deep learning.