Even the most renowned implementors of cryptographic primitives are not infallible. A number of tools for computer-aided verification have been proposed. For example, fiat-crypto can directly synthesize correct-by-construction code for cryptographic primitives. There is an ongoing effort to extend fiat-crypto correctness guarantees to assembly-language implementations by automatically checking their equivalence to fiat-crypto-generated code. This project aims to (1) extend a python version program equivalence checker for assembly programs, specifically for vector instructions. (2) Use the checker on existing vectorized implementations and if possible modify the higher-level fiat-crypto pipeline (including proofs) to generate vector operations.

I am participating in SuperUROP because I want to apply to graduate school and it would be helpful to gain some research experience in the field (Programming Language) I am interested in.