From 44c677b7d4a2b5f8e652906797eb84528a4f1b8a Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 10 Feb 2025 20:32:14 +0100 Subject: [PATCH] docs: add hax paper --- docs/publications.md | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/docs/publications.md b/docs/publications.md index bfcd23a56..f09653579 100644 --- a/docs/publications.md +++ b/docs/publications.md @@ -2,15 +2,22 @@ weight: 5 --- +To cite hax, please use + +
+[**hax: Verifying Security-Critical Rust Software using Multiple Provers**](https://eprint.iacr.org/2025/142). +
+ # Publications -* [📕 hacspec Tech report](https://hal.inria.fr/hal-03176482) -* [📕 HACSpec: A gateway to high-assurance cryptography](https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf) -* [📕 Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf) +* [hax: Verifying Security-Critical Rust Software using Multiple Provers](https://eprint.iacr.org/2025/142) +* [hacspec Tech report](https://hal.inria.fr/hal-03176482) +* [HACSpec: A gateway to high-assurance cryptography](https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf) +* [Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf) ### Secondary literature, using hacspec & hax: -* [📕 Last yard](https://eprint.iacr.org/2023/185) -* [📕 A Verified Pipeline from a Specification Language to Optimized, Safe Rust](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl22-final61.pdf) at [CoqPL'22](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust) -* [📕 Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify24](https://sites.google.com/view/rustverify2024) -* [📕 A formal security analysis of Blockchain voting](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper8-2.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/8/A-formal-security-analysis-of-Blockchain-voting) -* [📕 Specifying Smart Contract with Hax and ConCert](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper9-13.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert) +* [Last yard](https://eprint.iacr.org/2023/185) +* [A Verified Pipeline from a Specification Language to Optimized, Safe Rust](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl22-final61.pdf) at [CoqPL'22](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust) +* [Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify24](https://sites.google.com/view/rustverify2024) +* [A formal security analysis of Blockchain voting](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper8-2.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/8/A-formal-security-analysis-of-Blockchain-voting) +* [Specifying Smart Contract with Hax and ConCert](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper9-13.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert)