The Verification Problem Introduced by Highly Specialized Cryptographic Implementations
11 January 2014 ∞
As cryptographic implementations naturally strive for better and better performances it's actually very common to see generic implementations dropped in favor of highly specialized ones. Therefore, there's often a dedicated implementation not only for any single family of crypto algorithm but also for any single combination of parameters and cpu architectures. The obvious downside is this could easily result in large code bases difficult to verify and audit.
TweetNaCl – a compact implementation of NaCl – developped by Bernstein et al. discusses the challenges introduced by these specialized cryptographic implementations:
However, NaCl’s performance comes at a price. A single NaCl function usually consists of several different implementations, often including multiple assembly-language implementations optimized for different CPUs. NaCl’s compilation system is correspondingly complicated. Auditing the NaCl source is a time-consuming job. For example, four implementations of the ed25519 signature system have been publicly available and waiting for integration into NaCl since 2011, but in total they consist of 5521 lines of C code and 16184 lines of qhasm code.
Highlighting a bug found in the relatively large amount of code implementing operations on Edwards curves such as point addition.
Partial audits have revealed a bug in this software (r1 += 0 + carry should be r2 += 0 + carry in amd64-64-24k) that would not be caught by random tests; this illustrates the importance of audits. There has been some progress towards computer verification of formal proofs of correctness of software, but this progress is still far from complete verification of a usable high-security cryptographic library.