jadep.bib

@inproceedings{fiat-crypto,
  title = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
  author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
  booktitle = {Proceedings of the \href{https://www.ieee-security.org/TC/SP2019/}{40th IEEE Symposium on Security and Privacy (S\&P'19)}},
  year = {2019},
  month = {May},
  abstract = {We introduce a new approach for implementing cryptographic arithmetic in short high-level code with machine-checked proofs of functional correctness.
We further demonstrate that simple partial evaluation is sufficient to transform into the fastest-known C code, breaking the decades-old pattern that the only fast implementations are those whose instruction-level steps were written out by hand.

These techniques were used to build an elliptic-curve library that achieves competitive performance for 80 prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases.
As one outcome, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve.
Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare.},
  code-github = {https://github.com/mit-plv/fiat-crypto},
  timestamp = {2018.11.18},
  url = {https://people.csail.mit.edu/jadep/papers/2019-fiat-crypto-ieee-sp.pdf}
}

@mastersthesis{mastersthesis,
  author = {Jade Philipoom},
  title = {Correct-by-Construction Finite Field Arithmetic in Coq},
  school = {Massachusetts Institute of Technology},
  year = 2018,
  month = {February},
  url = {https://people.csail.mit.edu/jadep/papers/meng_thesis.pdf}
}