APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Tue 28 Nov 2023 09:00 - 10:00 at Room 106 & 107, IIS - Keynote 2 Chair(s): Yannick Forster

Cryptographic primitive programs are the building blocks of computer cryptography. In this talk, I will motivate the verification problem of cryptographic primitive programs and present the automatic formal verification tool CoqCryptoLine to address the problem. CoqCryptoLine is a formally verified tool for cryptographic primitive programs. It is built upon OCAML programs extracted from algorithms verified in the proof assistant Coq. Its verification results are moreover validated by certificate checkers. We will see the design of CoqCryptoLine. Verification results of cryptographic primitive programs from Bitcoin, OpenSSL, and Kyber NTT will also be presented.

Tue 28 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change