SPARKNaCl是一种基于TweetNaCl分布的新的、经过验证的、快速的NaCl API reefrence实现。它具有全自动、完整且隔音的类型安全性和几个关键的正确性属性。此外，该代码在所有优化级别上以3倍的速度在Ed25519符号操作上快速执行。本讲座将介绍如何"；证明驱动优化"；可以在裸机嵌入式目标上生成正确且快速的代码。
TweetNaCl是NaCl API的紧凑参考实现。它最初是为了表明一个完整的加密库可以放入"；100条推文"；，但HASSINE已被重新用于一些关键应用，如WireGuard VPN。代码中没有任何注释，所有保证都基于一篇简短的学术论文，以及作者令人敬畏的声誉。
我们能做得更好吗？我们能不能生产一个易于自动验证的参考实现，并且在性能和代码大小方面与TweetNaCl竞争？
本演讲介绍SPARKNaCl——SPARK中WeetNACL的完整重新实现，它提供了类型安全性、内存安全性和一些关键正确性属性的全自动证明。在建立了坚实的基础之后，我们继续比较SPARKACL的性能和代码大小与原来的C实现。应用了各种转换和优化，使SPARKNaCl在单个Ed25519和#34的裸机32位RISC-V机器上的性能优于TweetNaClon；标志"；操作，同时保持自动化和证据的完整性。此外，SPARKNaCl根据3条款BSD许可证免费提供。
本次演讲将概述SPARKNaCl的预防工作和性能分析的结果。