Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.

Abstract We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. Algebraic techniques are employed to analyze abstract polynomial programs; SMT QF_BV solvers are adopted for bit-accurate analysis of soundness conditions. We explain how to verify our abstraction algorithm and certify verification results. Our hybrid technique has verified non-linear computations in various security libraries such as Bitcoin and OpenSSL. We also report the certified verification of Number-Theoretic Transform programs from the post-quantum cryptosystem Kyber.

Abstract We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine verification algorithm consists of two reductions. The algebraic reduction transforms into a root entailment problem; and the bit-vector reduction transforms into an SMTQF_BV problem. We specify and verify both reductions formally using Coq with MathComp. The CoqCryptoLine tool is built on the OCaml programs extracted from verified reductions. CoqCryptoLine moreover employs certified techniques for solving the algebraic and logic problems. We evaluate CoqCryptoLine on cryptographic programs from industrial security libraries.

Correct implementations of cryptographic primitives are essential for modern security. These implementations often contain arithmetic operations involving non-linear computations that are infamously hard to verify. We present llvm2CryptoLine, an automated formal verification tool for arithmetic operations in cryptographic C programs. llvm2CryptoLine successfully verifies 51 arithmetic C programs from industrial cryptographic libraries OpenSSL, wolfSSL and NaCl. Most of the programs are verified fully automatically and efficiently. A screencast that showcases llvm2CryptoLine can be found at https://youtu.be/QXuSmja45VA. Source code is available at https://github.com/fmlab-iis/llvm2cryptoline.

Abstract We present a certified SMT QF_BV solver CoqQFBV built from a verified bit blasting algorithm, Kissat, and the verified SAT certificate checker GratChk in this paper. Our verified bit blasting algorithm supports the full QF_BV logic of SMT-LIB; it is specified and formally verified in the proof assistant Coq . We compare CoqQFBV with CVC4, Bitwuzla, and Boolector on benchmarks from the QF_BV division of the single query track in the 2020 SMT Competition, and real-world cryptographic program verification problems. CoqQFBV surprisingly solves more program verification problems with certification than the 2020 SMT QF_BV division winner Bitwuzla without certification.

We develop an automated formal technique to specify and verify signed computation in cryptographic programs. In addition to new instructions, we introduce a type system to detect type errors in programs. A type inference algorithm is also provided to deduce types and instruction variants in cryptographic programs. In order to verify signed cryptographic C programs, we develop a translator from the GCC intermediate representation to our language. Using our technique, we have verified 82 C functions in cryptography libraries including NaCl, wolfSSL, bitcoin, OpenSSL, and BoringSSL.

Cryptographic primitives are ubiquitous for modern security. The correctness of their implementations is crucial to resist malicious attacks. Typical arithmetic computation of these C programs contains large numbers of non-linear operations, hence is challenging existing automatic C verification tools. We present an automated approach to verify cryptographic C programs. Our approach successfully verifies C implementations of various arithmetic operations used in NIST P-224, P-256, P-521 and Curve25519 in OpenSSL. During verification, we expose a bug and a few anomalies that have been existing for a long time. They have been reported to and confirmed by the OpenSSL community. Our results establish the functional correctness of these C implementations for the first time.

Arithmetic over large finite fields is indispensable in modern cryptography. For efficienty, these operations are often implemented in manually optimized assembly programs. Since these arithmetic assembly programs necessarily perform lots of non-linear computation, checking their correctness is a challenging verification problem. We develop techniques to verify such programs automatically in this paper. Using our techniques, we have successfully verified a number of assembly programs in OpenSSL. Moreover, our tool verifies the boringSSL Montgomery Ladderstep (about 1400 assembly instructions) in 1 hour. This is by far the fastest verification technique for such programs.

In ISSAC 2017, van der Hoeven and Larrieu showed that evaluating a polynomial P ın Fq [x] of degree <n at all n -th roots of unity in Fqd can essentially be computed d times faster than evaluating Q ın Fqd x at all these roots, assuming Fqd contains a primitive n -th root of unity. Termed the Frobenius FFT, this discovery has a profound impact on polynomial multiplication, especially for multiplying binary polynomials, which finds ample application in coding theory and cryptography. In this paper, we show that the theory of Frobenius FFT beautifully generalizes to a class of additive FFT developed by Cantor and Gao-Mateer. Furthermore, we demonstrate the power of Frobenius additive FFT for q=2: to multiply two binary polynomials whose product is of degree <256, the new technique requires only 29,005 bit operations, while the best result previously reported was 33,397. To the best of our knowledge, this is the first time that FFT-based multiplication outperforms Karatsuba and the like at such a low degree in terms of bit-operation count.

Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly language and optimized manually for efficiency. We develop a certified technique to verify low-level mathematical constructs in X25519, the default elliptic curve Diffie-Hellman key exchange protocol used in OpenSSH. Our technique translates an algebraic specification of mathematical constructs into an algebraic problem. The algebraic problem in turn is solved by the computer algebra system Singular. The proof assistant Coq certifies the translation and solution to algebraic problems. Specifications about output ranges and potential program overflows are translated to SMT problems and verified by SMT solvers. We report our case studies on verifying arithmetic computation over a large finite field and the Montgomery Ladderstep, a crucial loop in X25519.

This paper presents results on formal verification of high-speed cryptographic software. We consider speed-record-setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. Two versions for different microarchitectures are available. We successfully verify the core part of the computation, and reproduce detection of a bug in a previously published edition. An SMT solver supporting array and bit-vector theories is used to establish almost all properties. Remaining properties are verified in a proof assistant with simple rewrite tactics. We also exploit the compositionality of Hoare logic to address the scalability issue. Essential differences between both versions of the software are discussed from a formal-verification perspective.

Establishing trust between a group of individuals remains a difficult problem. Prior works assume trusted infrastructure, require an individual to trust unknown entities, or provide relatively low probabilistic guarantees of authenticity (95 percent for realistic settings). This work presents SPATE, a primitive that allows users to establish trust via mobile devices and physical interaction. Once the SPATE protocol runs to completion, its participants' mobile devices have authentic data that their applications can use to interact securely (i.e., the probability of a successful attack is 2-24). For this work, we leverage SPATE as part of a larger system to facilitate efficient, secure, and user-friendly collaboration via e-mail, file-sharing, and text messaging services. Our implementation of SPATE on Nokia N70 smartphones allows users to establish trust in small groups of up to eight users in less than one minute. The example SPATE applications provide increased security with little overhead noticeable to users once keys are established.

Several security protocols require a human to compare two hash values to ensure successful completion. When the hash values are represented as long sequences of numbers, humans may make a mistake or require significant time and patience to accurately compare the hash values. To improve usability during comparison, a number of researchers have proposed various hash representations that use words, sentences, or images rather than numbers. This is the first work to perform a comparative study of these hash comparison schemes to determine which scheme allows the fastest and most accurate comparison. To evaluate the schemes, we performed an online user study with more than 400 participants. Our findings indicate that only a small number of schemes allow quick and accurate comparison across a wide range of subjects from varying backgrounds.

Establishing trust between a group of individuals remains a difficult problem. Prior works assume trusted infrastructure, require an individual to trust unknown entities, or provide relatively low probabilistic guarantees of authenticity (95% for realistic settings). This work presents SPATE, a primitive that allows users to establish trust via device mobility and physical interaction. Once the SPATE protocol runs to completion, its participants' mobile devices have authentic data that their applications can use to interact securely (i.e., the probability of a successful attack is 2-24). For this work, we leverage SPATE as part of a larger system to facilitate efficient, secure, and user-friendly collaboration via email and file-sharing services. Our implementation of SPATE on Nokia N70 smartphones allows users to establish trust in small groups of up to eight users in less than one minute. The two example SPATE applications provide increased security with no overhead noticeable to users once keys are established.

Establishing secure communication among a group of physically collocated people is a challenge. This problem can be reduced to establishing authentic public keys among all the participants - these public keys then serve to establish a shared secret symmetric key for encryption and authentication of messages. Unfortunately, in most real-world settings, public key infrastructures (PKI) are uncommon and distributing a secret in a public space is difficult. Thus, it is a challenge to exchange authentic public keys in a scalable, secure, and easy to use fashion.