Livia Sun

Livia  Sun
MIT EECS | Analog Devices Undergraduate Research and Innovation Scholar
Advisor: Adam Chlipala
Department: EECS
Areas of Research: Computer Systems
Years: 2021-2022
Research Project Title:

Vector Instruction Extension in Program Equivalence Checker

abstract: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.