High-assurance field inversion for pairing-friendly primes

Introduction. Bilinear pairings have become popular for deploying privacy-preserving cryptocurrencies, as they represent a fundamental building block for the zero-knowledge proofs required for security. ZCash is a clear example of this trend, where pairing-based zero-knowledge Succint Non-Interactive Arguments of Knowledge (zk-SNARKs) underlie private shielded transactions [8]. Another example of application of pairing-based protocols comes from the Chia blockchain, where Boneh-Lynn-Shacham (BLS) [10] signatures were adopted for improved smart transaction support. There has been substantial progress in the past decade towards selecting parameters [6, 4, 5] and implementing pairing-based cryptography efficiently in software [3]. However, current record-setting implementations rely on hand-optimized architecture-specific Assembly code for the underlying field arithmetic and a great deal of manual tuning to unlock the best performance across a range of architectures. This introduces low-level code which is both hard to audit and to verify as correct, and a number of cryptographic libraries have suffered with simple bugs as a direct consequence [12]. Due to its many optimizations efficient code can be hard to verify in a post hoc way. Recently, an alternative path for implementing cryptographic libraries was demonstrated as viable in the Fiat-Crypto framework [12]. By combining correct-by-design optimized low-level code with automatically generated and formally verified high-level code, it became possible to develop libraries which are both efficient and formally verified. The approach was illustrated through the implementation of field arithmetic for several standardized elliptic curves using an extensible code generation framework, capable of producing code competitive in performance with popular hand-optimized multi-precision libraries [12]. The verification steps are conducted using the Coq proof assistant, a state-of-the-art theorem prover [11]. Such high assurance cryptographic implementations have recently been adopted by the industry: Google’s BoringSSL on Fiat-Crypto [12], Firefox on Evercrypt [13], and the WireGuard VPN on both. A SHA-3 implementation was made using Jasmin [1], another framework for developing high-speed and high-assurance cryptographic software.