diff --git a/examples/Cargo.toml b/examples/Cargo.toml index 4aea4b684..a77a06f5b 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -1,5 +1,6 @@ [workspace] members = [ + "bip-340", "chacha20", "limited-order-book", "sha256", diff --git a/examples/Makefile b/examples/Makefile index 6bcdc2bc7..2cecd8b06 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -1,6 +1,7 @@ .PHONY: default default: make -C limited-order-book + make -C bip-340 make -C chacha20 make -C sha256 make -C barrett @@ -9,6 +10,7 @@ default: clean: make -C limited-order-book clean + make -C bip-340 clean make -C chacha20 clean make -C sha256 clean make -C barrett clean diff --git a/examples/bip-340/Cargo.toml b/examples/bip-340/Cargo.toml new file mode 100644 index 000000000..73823870a --- /dev/null +++ b/examples/bip-340/Cargo.toml @@ -0,0 +1,24 @@ +[package] +name = "bip-340" +version = "0.1.0" +authors = ["Jonas Nick ", "Fabian Jahr "] +edition = "2021" +description = "A BIP 340 implementation compatible with https://github.com/bitcoin/bips/blob/master/bip-0340.mediawiki." + +[lib] +path = "src/bip-340.rs" + +[dependencies] +hax-lib.workspace = true +sha256 = { path = "../sha256" } +num-bigint = "0.4" +num-traits = "0.2" + +[dev-dependencies] +quickcheck = "1.0" +serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" +hex = "0.4" + +[package.metadata.hax] +include = ["*"] diff --git a/examples/bip-340/Makefile b/examples/bip-340/Makefile new file mode 100644 index 000000000..212cda6e4 --- /dev/null +++ b/examples/bip-340/Makefile @@ -0,0 +1,7 @@ +.PHONY: default clean +default: + make -C proofs/fstar/extraction + +clean: + rm -f proofs/fstar/extraction/.depend + rm -f proofs/fstar/extraction/*.fst diff --git a/examples/bip-340/proofs/fstar/extraction/Makefile b/examples/bip-340/proofs/fstar/extraction/Makefile new file mode 100644 index 000000000..e6d1a21e9 --- /dev/null +++ b/examples/bip-340/proofs/fstar/extraction/Makefile @@ -0,0 +1,153 @@ +# This is a generically useful Makefile for F* that is self-contained +# +# It is tempting to factor this out into multiple Makefiles but that +# makes it less portable, so resist temptation, or move to a more +# sophisticated build system. +# +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. +# +# ROOTS contains all the top-level F* files you wish to verify +# The default target `verify` verified ROOTS and its dependencies +# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line +# +# To make F* emacs mode use the settings in this file, you need to +# add the following lines to your .emacs +# +# (setq-default fstar-executable "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/bin/z3") +# +# (defun my-fstar-compute-prover-args-using-make () +# "Construct arguments to pass to F* by calling make." +# (with-demoted-errors "Error when constructing arg string: %S" +# (let* ((fname (file-name-nondirectory buffer-file-name)) +# (target (concat fname "-in")) +# (argstr (car (process-lines "make" "--quiet" target)))) +# (split-string argstr)))) +# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) +# + +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") + +CACHE_DIR ?= .cache +HINT_DIR ?= .hints + +SHELL ?= /usr/bin/env bash + +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) + +.PHONY: all verify clean + +all: + rm -f .depend && $(MAKE) .depend + $(MAKE) verify + +HAX_CLI = "cargo hax into fstar --z3rlimit 100" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") + +FSTAR_FLAGS = --cmi \ + --warn_error -331 \ + --cache_checked_modules --cache_dir $(CACHE_DIR) \ + --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \ + $(addprefix --include ,$(FSTAR_INCLUDE_DIRS)) + +FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + +.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) + $(info $(ROOTS)) + $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ + +include .depend + +$(HINT_DIR): + mkdir -p $@ + +$(CACHE_DIR): + mkdir -p $@ + +$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) + $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints + +verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) + +# Targets for interactive mode + +%.fst-in: + $(info $(FSTAR_FLAGS) \ + $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints) + +%.fsti-in: + $(info $(FSTAR_FLAGS) \ + $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints) + + +# Clean targets + +clean: + rm -rf $(CACHE_DIR)/* + rm *.fst diff --git a/examples/bip-340/src/bip-340.rs b/examples/bip-340/src/bip-340.rs new file mode 100644 index 000000000..67ad7b5b8 --- /dev/null +++ b/examples/bip-340/src/bip-340.rs @@ -0,0 +1,464 @@ +//! This crate is an INSECURE prototype implementation of BIP-340 (). +//! It is vulnerable against timing attacks. + +use sha256::sha256; +use num_bigint::{self, Sign}; +use num_traits::Euclid; +use hax_lib::int::*; +use hax_lib::Abstraction; + +#[derive(Debug, PartialEq)] +pub enum Error { + InvalidSecretKey, + InvalidNonceGenerated, + InvalidPublicKey, + InvalidXCoordinate, + InvalidSignature, +} + +pub trait ModularArithmetic: Clone + PartialEq + Sized { + fn modulus() -> Int; + + fn new(value: Int) -> Self; + + fn get_value(&self) -> ∬ + + fn mod_reduce(value: Int, modulus: Int) -> Int { + let result = value.get().rem_euclid(&modulus.get()); + Int::new(result) + } + + fn from_byte_seq_be(bytes: &[u8; 32]) -> Self { + let bigint = num_bigint::BigInt::from_bytes_be(Sign::Plus, bytes); + Self::new(Int::new(bigint)) + } + + fn to_byte_seq_be(&self) -> [u8; 32] { + let bigint = self.get_value().get(); + let (_, bytes) = bigint.to_bytes_be(); + + let mut result = [0u8; 32]; + if bytes.len() <= 32 { + let start_idx = 32 - bytes.len(); + result[start_idx..].copy_from_slice(&bytes); + } else { + result.copy_from_slice(&bytes[bytes.len() - 32..]); + } + result + } + + fn bit(&self, index: usize) -> bool { + let byte_index = index / 8; + let bit_index = index % 8; + let bytes = self.to_byte_seq_be(); + if byte_index < 32 { + (bytes[31 - byte_index] >> bit_index) & 1 == 1 + } else { + false + } + } + + #[allow(non_snake_case)] + fn ZERO() -> Self { + Self::new(0u8.lift()) + } + + #[allow(non_snake_case)] + fn ONE() -> Self { + Self::new(1u8.lift()) + } + + #[allow(non_snake_case)] + fn TWO() -> Self { + Self::new(2u8.lift()) + } + + fn mod_add(self, other: Self) -> Self { + let modulus = Self::modulus().get(); + let result = (self.get_value().get() + other.get_value().get()).rem_euclid(&modulus); + Self::new(Int::new(result)) + } + + fn mod_sub(self, other: Self) -> Self { + let modulus = Self::modulus().get(); + let result = (self.get_value().get() + &modulus - other.get_value().get()).rem_euclid(&modulus); + Self::new(Int::new(result)) + } + + fn mod_mul(self, other: Self) -> Self { + let modulus = Self::modulus().get(); + let result = (self.get_value().get() * other.get_value().get()).rem_euclid(&modulus); + Self::new(Int::new(result)) + } + + fn from_bytes_strict(b: [u8; 32]) -> Option { + let s = num_bigint::BigInt::from_bytes_be(Sign::Plus, &b); + let max_value = Self::modulus().get(); + + if s >= max_value { + None + } else { + Some(Self::new(Int::new(s))) + } + } +} + +#[derive(Clone, PartialEq)] +pub struct FieldElement { + value: Int, +} + +impl ModularArithmetic for FieldElement { + fn modulus() -> Int { + int!(0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F) + } + + fn new(value: Int) -> Self { + let reduced = Self::mod_reduce(value, Self::modulus()); + Self { value: reduced } + } + + fn get_value(&self) -> &Int { + &self.value + } +} + +impl FieldElement { + pub fn pow_self(&self, exp: FieldElement) -> FieldElement { + let modulus = Self::modulus().get(); + let base = self.value.get(); + let exponent = exp.value.get(); + let result = base.modpow(&exponent, &modulus); + Self { + value: Int::new(result), + } + } +} + +macro_rules! impl_arithmetic_ops { + ($type:ty) => { + impl std::ops::Add for $type { + type Output = Self; + fn add(self, other: Self) -> Self { + self.mod_add(other) + } + } + + impl std::ops::Sub for $type { + type Output = Self; + fn sub(self, other: Self) -> Self { + self.mod_sub(other) + } + } + + impl std::ops::Mul for $type { + type Output = Self; + fn mul(self, other: Self) -> Self { + self.mod_mul(other) + } + } + }; +} + +impl_arithmetic_ops!(FieldElement); + +impl std::ops::Rem for FieldElement { + type Output = Self; + fn rem(self, other: Self) -> Self { + let result = self.value.get().rem_euclid(&other.value.get()); + FieldElement { value: Int::new(result) } + } +} + +#[derive(Clone, PartialEq)] +pub struct Scalar { + value: Int, +} + +impl ModularArithmetic for Scalar { + fn modulus() -> Int { + int!(0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141) + } + + fn new(value: Int) -> Self { + let reduced = Self::mod_reduce(value, Self::modulus()); + Self { value: reduced } + } + + fn get_value(&self) -> &Int { + &self.value + } +} + +impl_arithmetic_ops!(Scalar); + +fn bytes_to_hex(bytes: &[u8]) -> String { + let mut result = String::new(); + for byte in bytes { + result.push_str(&format!("{:02x}", byte)); + } + result +} + +macro_rules! impl_debug { + ($type:ty, $name:expr) => { + impl std::fmt::Debug for $type { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}({})", $name, bytes_to_hex(&self.to_byte_seq_be())) + } + } + }; +} + +impl_debug!(FieldElement, "FieldElement"); +impl_debug!(Scalar, "Scalar"); + +pub type AffinePoint = (FieldElement, FieldElement); + +#[derive(Debug, Clone)] +pub enum Point { + Affine(AffinePoint), + AtInfinity, +} + +pub fn finite(p: Point) -> Option { + match p { + Point::Affine(p) => Some(p), + Point::AtInfinity => None, + } +} + +pub fn x(p: &AffinePoint) -> FieldElement { + let (x, _) = p; + x.clone() +} + +pub fn y(p: &AffinePoint) -> FieldElement { + let (_, y) = p; + y.clone() +} + +pub fn has_even_y(p: AffinePoint) -> bool { + y(&p) % FieldElement::TWO() == FieldElement::ZERO() +} + +fn sqrt(y: FieldElement) -> Option { + // This is the field element equal to (p+1)/4. + let p1_4_bytes = [ + 0x3Fu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, + 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, + 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, + 0xFFu8, 0xFFu8, 0xFFu8, 0xFFu8, 0xBFu8, 0xFFu8, 0xFFu8, 0x0Cu8 + ]; + let p1_4 = FieldElement::from_byte_seq_be(&p1_4_bytes); + let x = y.pow_self(p1_4); + if x.pow_self(FieldElement::TWO()) == y { + Some(x) + } else { + None + } +} + +pub fn lift_x(x: FieldElement) -> Result { + let one = FieldElement::ONE(); + let two = FieldElement::TWO(); + let three = FieldElement::new(3u128.lift()); + let seven = FieldElement::new(7u128.lift()); + let y_sq = x.pow_self(three) + seven; + let mut y = sqrt(y_sq).ok_or(Error::InvalidXCoordinate)?; + if y.clone() % two == one { + y = FieldElement::ZERO() - y; + } + Ok((x, y)) +} + +fn compute_lam(p1: AffinePoint, p2: AffinePoint) -> FieldElement { + let three = FieldElement::new(3u128.lift()); + if p1 != p2 { + (y(&p2) - y(&p1)) * (x(&p2) - x(&p1)).pow_self(FieldElement::ZERO() - FieldElement::TWO()) + } else { + three * x(&p1) * x(&p1) * (FieldElement::TWO() * y(&p1)).pow_self(FieldElement::ZERO() - FieldElement::TWO()) + } +} + +pub fn point_add(p1: Point, p2: Point) -> Point { + if finite(p1.clone()).is_none() { return p2 } + if finite(p2.clone()).is_none() { return p1 } + + let p1_affine = finite(p1).unwrap(); + let p2_affine = finite(p2).unwrap(); + if !((x(&p1_affine) == x(&p2_affine)) && (y(&p1_affine) != y(&p2_affine))) { + let lam = compute_lam(p1_affine.clone(), p2_affine.clone()); + let x3 = lam.clone() * lam.clone() - x(&p1_affine) - x(&p2_affine); + return Point::Affine((x3.clone(), lam * (x(&p1_affine) - x3) - y(&p1_affine))); + } + Point::AtInfinity +} + +pub fn point_mul(s: Scalar, p: Point) -> Point { + let mut p = p; + let mut q = Point::AtInfinity; + for i in 0..256 { + if s.bit(i) { + q = point_add(q, p.clone()); + } + p = point_add(p.clone(), p); + } + q +} + +pub fn point_mul_base(s: Scalar) -> Point { + let gx_bytes = [ + 0x79u8, 0xBEu8, 0x66u8, 0x7Eu8, 0xF9u8, 0xDCu8, 0xBBu8, 0xACu8, + 0x55u8, 0xA0u8, 0x62u8, 0x95u8, 0xCEu8, 0x87u8, 0x0Bu8, 0x07u8, + 0x02u8, 0x9Bu8, 0xFCu8, 0xDBu8, 0x2Du8, 0xCEu8, 0x28u8, 0xD9u8, + 0x59u8, 0xF2u8, 0x81u8, 0x5Bu8, 0x16u8, 0xF8u8, 0x17u8, 0x98u8 + ]; + let gy_bytes = [ + 0x48u8, 0x3Au8, 0xDAu8, 0x77u8, 0x26u8, 0xA3u8, 0xC4u8, 0x65u8, + 0x5Du8, 0xA4u8, 0xFBu8, 0xFCu8, 0x0Eu8, 0x11u8, 0x08u8, 0xA8u8, + 0xFDu8, 0x17u8, 0xB4u8, 0x48u8, 0xA6u8, 0x85u8, 0x54u8, 0x19u8, + 0x9Cu8, 0x47u8, 0xD0u8, 0x8Fu8, 0xFBu8, 0x10u8, 0xD4u8, 0xB8u8 + ]; + let g = Point::Affine(( + FieldElement::from_byte_seq_be(&gx_bytes), + FieldElement::from_byte_seq_be(&gy_bytes), + )); + point_mul(s, g) +} + +pub type Bytes32 = [u8; 32]; +pub type SecretKey = Bytes32; +pub type PublicKey = Bytes32; +pub type Message = Bytes32; +pub type AuxRand = Bytes32; +pub type Signature = [u8; 64]; + +pub fn tagged_hash(tag: &[u8], msg: &[u8]) -> Bytes32 { + let tag_hash = sha256(tag); + let mut combined = Vec::new(); + combined.extend_from_slice(&tag_hash); + combined.extend_from_slice(&tag_hash); + combined.extend_from_slice(msg); + sha256(&combined) +} + +// "BIP0340/aux" +const BIP0340_AUX: &[u8] = &[ + 0x42u8, 0x49u8, 0x50u8, 0x30u8, 0x33u8, 0x34u8, 0x30u8, 0x2fu8, 0x61u8, 0x75u8, 0x78u8, +]; + +pub fn hash_aux(aux_rand: AuxRand) -> Bytes32 { + tagged_hash(BIP0340_AUX, &aux_rand) +} + +// "BIP0340/nonce" +const BIP0340_NONCE: &[u8] = &[ + 0x42u8, 0x49u8, 0x50u8, 0x30u8, 0x33u8, 0x34u8, 0x30u8, 0x2fu8, 0x6eu8, 0x6fu8, 0x6eu8, 0x63u8, + 0x65u8, +]; + +pub fn hash_nonce(rand: Bytes32, pubkey: Bytes32, msg: Message) -> Bytes32 { + let mut c = Vec::new(); + c.extend_from_slice(&rand); + c.extend_from_slice(&pubkey); + c.extend_from_slice(&msg); + tagged_hash(BIP0340_NONCE, &c) +} + +// "BIP0340/challenge" +const BIP0340_CHALLENGE: &[u8] = &[ + 0x42u8, 0x49u8, 0x50u8, 0x30u8, 0x33u8, 0x34u8, 0x30u8, 0x2fu8, 0x63u8, 0x68u8, 0x61u8, 0x6cu8, + 0x6cu8, 0x65u8, 0x6eu8, 0x67u8, 0x65u8, +]; + +pub fn hash_challenge(rx: Bytes32, pubkey: Bytes32, msg: Bytes32) -> Bytes32 { + let mut c = Vec::new(); + c.extend_from_slice(&rx); + c.extend_from_slice(&pubkey); + c.extend_from_slice(&msg); + tagged_hash(BIP0340_CHALLENGE, &c) +} + +pub fn seckey_scalar_from_bytes(b: Bytes32) -> Option { + let s = Scalar::from_bytes_strict(b)?; + if s == Scalar::ZERO() { + None + } else { + Some(s) + } +} + +fn xor_bytes(b0: Bytes32, b1: Bytes32) -> Bytes32 { + let mut result = [0u8; 32]; + for i in 0..32 { + result[i] = b0[i] ^ b1[i]; + } + result +} + +pub type PubkeyGenResult = Result; +pub fn pubkey_gen(seckey: SecretKey) -> PubkeyGenResult { + let d0 = seckey_scalar_from_bytes(seckey).ok_or(Error::InvalidSecretKey)?; + let p = finite(point_mul_base(d0)).unwrap(); + Ok(x(&p).to_byte_seq_be()) +} + +pub type SignResult = Result; +pub fn sign(msg: Message, seckey: SecretKey, aux_rand: AuxRand) -> SignResult { + let d0 = seckey_scalar_from_bytes(seckey).ok_or(Error::InvalidSecretKey)?; + let p = finite(point_mul_base(d0.clone())).unwrap(); + let d = if has_even_y(p.clone()) { + d0 + } else { + Scalar::ZERO() - d0 + }; + let t = xor_bytes(d.to_byte_seq_be(), hash_aux(aux_rand)); + let k0 = Scalar::from_byte_seq_be(&hash_nonce(t, x(&p).to_byte_seq_be(), msg)); + if k0 == Scalar::ZERO() { + // This happens only with negligible probability + return Err(Error::InvalidNonceGenerated); + } + let r = finite(point_mul_base(k0.clone())).unwrap(); + let k = if has_even_y(r.clone()) { + k0 + } else { + Scalar::ZERO() - k0 + }; + let e = Scalar::from_byte_seq_be(&hash_challenge( + x(&r).to_byte_seq_be(), + x(&p).to_byte_seq_be(), + msg, + )); + let mut sig = [0u8; 64]; + let r_bytes = x(&r).to_byte_seq_be(); + let s_bytes = (k + e * d).to_byte_seq_be(); + sig[0..32].copy_from_slice(&r_bytes); + sig[32..64].copy_from_slice(&s_bytes); + + verify(msg, x(&p).to_byte_seq_be(), sig)?; + Ok(sig) +} + +pub type VerificationResult = Result<(), Error>; +pub fn verify(msg: Message, pubkey: PublicKey, sig: Signature) -> VerificationResult { + let p_x = FieldElement::from_bytes_strict(pubkey).ok_or(Error::InvalidPublicKey)?; + let p = lift_x(p_x)?; + let r_bytes: [u8; 32] = sig[0..32].try_into().unwrap(); + let s_bytes: [u8; 32] = sig[32..64].try_into().unwrap(); + let r = FieldElement::from_bytes_strict(r_bytes).ok_or(Error::InvalidSignature)?; + let s = Scalar::from_bytes_strict(s_bytes).ok_or(Error::InvalidSignature)?; + + let e = Scalar::from_byte_seq_be(&hash_challenge(r_bytes, x(&p).to_byte_seq_be(), msg)); + let r_p = finite(point_add( + point_mul_base(s), + point_mul(Scalar::ZERO() - e, Point::Affine(p)), + )) + .ok_or(Error::InvalidSignature)?; + + if !has_even_y(r_p.clone()) || (x(&r_p) != r) { + Err(Error::InvalidSignature) + } else { + Ok(()) + } +} diff --git a/examples/bip-340/tests/cases.json b/examples/bip-340/tests/cases.json new file mode 100644 index 000000000..64cb6a71f --- /dev/null +++ b/examples/bip-340/tests/cases.json @@ -0,0 +1,152 @@ +[ + { + "index": "0", + "secret_key": "0000000000000000000000000000000000000000000000000000000000000003", + "public_key": "F9308A019258C31049344F85F89D5229B531C845836F99B08601F113BCE036F9", + "aux_rand": "0000000000000000000000000000000000000000000000000000000000000000", + "message": "0000000000000000000000000000000000000000000000000000000000000000", + "signature": "E907831F80848D1069A5371B402410364BDF1C5F8307B0084C55F1CE2DCA821525F66A4A85EA8B71E482A74F382D2CE5EBEEE8FDB2172F477DF4900D310536C0", + "verification_result": "TRUE", + "comment": "" + }, + { + "index": "1", + "secret_key": "B7E151628AED2A6ABF7158809CF4F3C762E7160F38B4DA56A784D9045190CFEF", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "0000000000000000000000000000000000000000000000000000000000000001", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "6896BD60EEAE296DB48A229FF71DFE071BDE413E6D43F917DC8DCF8C78DE33418906D11AC976ABCCB20B091292BFF4EA897EFCB639EA871CFA95F6DE339E4B0A", + "verification_result": "TRUE", + "comment": "" + }, + { + "index": "2", + "secret_key": "C90FDAA22168C234C4C6628B80DC1CD129024E088A67CC74020BBEA63B14E5C9", + "public_key": "DD308AFEC5777E13121FA72B9CC1B7CC0139715309B086C960E18FD969774EB8", + "aux_rand": "C87AA53824B4D7AE2EB035A2B5BBBCCC080E76CDC6D1692C4B0B62D798E6D906", + "message": "7E2D58D8B3BCDF1ABADEC7829054F90DDA9805AAB56C77333024B9D0A508B75C", + "signature": "5831AAEED7B44BB74E5EAB94BA9D4294C49BCF2A60728D8B4C200F50DD313C1BAB745879A5AD954A72C45A91C3A51D3C7ADEA98D82F8481E0E1E03674A6F3FB7", + "verification_result": "TRUE", + "comment": "" + }, + { + "index": "3", + "secret_key": "0B432B2677937381AEF05BB02A66ECD012773062CF3FA2549E44F58ED2401710", + "public_key": "25D1DFF95105F5253C4022F628A996AD3A0D95FBF21D468A1B33F8C160D8F517", + "aux_rand": "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF", + "message": "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF", + "signature": "7EB0509757E246F19449885651611CB965ECC1A187DD51B64FDA1EDC9637D5EC97582B9CB13DB3933705B32BA982AF5AF25FD78881EBB32771FC5922EFC66EA3", + "verification_result": "TRUE", + "comment": "test fails if msg is reduced modulo p or n" + }, + { + "index": "4", + "secret_key": "", + "public_key": "D69C3509BB99E412E68B0FE8544E72837DFA30746D8BE2AA65975F29D22DC7B9", + "aux_rand": "", + "message": "4DF3C3F68FCC83B27E9D42C90431A72499F17875C81A599B566C9889B9696703", + "signature": "00000000000000000000003B78CE563F89A0ED9414F5AA28AD0D96D6795F9C6376AFB1548AF603B3EB45C9F8207DEE1060CB71C04E80F593060B07D28308D7F4", + "verification_result": "TRUE", + "comment": "" + }, + { + "index": "5", + "secret_key": "", + "public_key": "EEFDEA4CDB677750A420FEE807EACF21EB9898AE79B9768766E4FAA04A2D4A34", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "6CFF5C3BA86C69EA4B7376F31A9BCB4F74C1976089B2D9963DA2E5543E17776969E89B4C5564D00349106B8497785DD7D1D713A8AE82B32FA79D5F7FC407D39B", + "verification_result": "FALSE", + "comment": "public_key not on the curve" + }, + { + "index": "6", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "FFF97BD5755EEEA420453A14355235D382F6472F8568A18B2F057A14602975563CC27944640AC607CD107AE10923D9EF7A73C643E166BE5EBEAFA34B1AC553E2", + "verification_result": "FALSE", + "comment": "has_even_y(R) is false" + }, + { + "index": "7", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "1FA62E331EDBC21C394792D2AB1100A7B432B013DF3F6FF4F99FCB33E0E1515F28890B3EDB6E7189B630448B515CE4F8622A954CFE545735AAEA5134FCCDB2BD", + "verification_result": "FALSE", + "comment": "negated message" + }, + { + "index": "8", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "6CFF5C3BA86C69EA4B7376F31A9BCB4F74C1976089B2D9963DA2E5543E177769961764B3AA9B2FFCB6EF947B6887A226E8D7C93E00C5ED0C1834FF0D0C2E6DA6", + "verification_result": "FALSE", + "comment": "negated s value" + }, + { + "index": "9", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "0000000000000000000000000000000000000000000000000000000000000000123DDA8328AF9C23A94C1FEECFD123BA4FB73476F0D594DCB65C6425BD186051", + "verification_result": "FALSE", + "comment": "sG - eP is infinite. Test fails in single verification if has_even_y(inf) is defined as true and x(inf) as 0" + }, + { + "index": "10", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "00000000000000000000000000000000000000000000000000000000000000017615FBAF5AE28864013C099742DEADB4DBA87F11AC6754F93780D5A1837CF197", + "verification_result": "FALSE", + "comment": "sG - eP is infinite. Test fails in single verification if has_even_y(inf) is defined as true and x(inf) as 1" + }, + { + "index": "11", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "4A298DACAE57395A15D0795DDBFD1DCB564DA82B0F269BC70A74F8220429BA1D69E89B4C5564D00349106B8497785DD7D1D713A8AE82B32FA79D5F7FC407D39B", + "verification_result": "FALSE", + "comment": "sig[0:32] is not an X coordinate on the curve" + }, + { + "index": "12", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F69E89B4C5564D00349106B8497785DD7D1D713A8AE82B32FA79D5F7FC407D39B", + "verification_result": "FALSE", + "comment": "sig[0:32] is equal to field size" + }, + { + "index": "13", + "secret_key": "", + "public_key": "DFF1D77F2A671C5F36183726DB2341BE58FEAE1DA2DECED843240F7B502BA659", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "6CFF5C3BA86C69EA4B7376F31A9BCB4F74C1976089B2D9963DA2E5543E177769FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141", + "verification_result": "FALSE", + "comment": "sig[32:64] is equal to curve order" + }, + { + "index": "14", + "secret_key": "", + "public_key": "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC30", + "aux_rand": "", + "message": "243F6A8885A308D313198A2E03707344A4093822299F31D0082EFA98EC4E6C89", + "signature": "6CFF5C3BA86C69EA4B7376F31A9BCB4F74C1976089B2D9963DA2E5543E17776969E89B4C5564D00349106B8497785DD7D1D713A8AE82B32FA79D5F7FC407D39B", + "verification_result": "FALSE", + "comment": "public_key is not a valid X coordinate because it exceeds the field size" + } +] diff --git a/examples/bip-340/tests/tests-bip-340.rs b/examples/bip-340/tests/tests-bip-340.rs new file mode 100644 index 000000000..faf0a5893 --- /dev/null +++ b/examples/bip-340/tests/tests-bip-340.rs @@ -0,0 +1,106 @@ +use bip_340::*; +use serde::{Deserialize, Serialize}; +use quickcheck::QuickCheck; + +/* The cases.json was produced from the test vectors with the following command: + + curl -s https://raw.githubusercontent.com/bitcoin/bips/master/bip-0340/test-vectors.csv \ + | python -c 'import csv, json, sys; print(json.dumps([dict(r) for r in csv.DictReader(sys.stdin)]))' \ + | jq \ + | sed -e 's/secret key/secret_key/' -e 's/public key/public_key/' -e 's/verification result/verification_result/' + + The SHA256 digest of the test vectors produced with + + curl -s https://raw.githubusercontent.com/bitcoin/bips/master/bip-0340/test-vectors.csv \ + | sha256sum + + was a17adbd2c19032ddc12e63b5f35d5224a9295e9f82397d2632a301696b3cac9f. +*/ + +#[derive(Debug, Deserialize, Serialize)] +struct CasesTestVector { + index: String, + secret_key: String, + public_key: String, + aux_rand: String, + message: String, + signature: String, + verification_result: String, +} + +impl CasesTestVector { + fn from_file(path: &str) -> Vec { + let contents = std::fs::read_to_string(path).expect("Failed to read test vector file"); + serde_json::from_str(&contents).expect("Failed to parse test vector JSON") + } +} + +trait FromHex: Sized { + fn from_hex(hex_str: &str) -> Self; +} +impl FromHex for [u8; N] { + fn from_hex(hex_str: &str) -> Self { + hex::decode(hex_str).unwrap().try_into().unwrap() + } +} + +#[test] +fn test_invalid_secret() { + let sk = SecretKey::from_hex("0000000000000000000000000000000000000000000000000000000000000000"); + assert_eq!(pubkey_gen(sk).unwrap_err(), Error::InvalidSecretKey); + let sk = SecretKey::from_hex("FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364140"); + assert!(pubkey_gen(sk).is_ok()); + let sk = SecretKey::from_hex("FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141"); + assert_eq!(pubkey_gen(sk).unwrap_err(), Error::InvalidSecretKey); + let sk = SecretKey::from_hex("FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"); + assert_eq!(pubkey_gen(sk).unwrap_err(), Error::InvalidSecretKey); +} + +#[test] +fn test_vectors() { + let v = CasesTestVector::from_file("tests/cases.json"); + for t in v { + let pk = PublicKey::from_hex(&t.public_key); + let sig = Signature::from_hex(&t.signature); + let msg = Message::from_hex(&t.message); + if !t.secret_key.is_empty() { + let sk = SecretKey::from_hex(&t.secret_key); + let pk2 = pubkey_gen(sk).unwrap(); + assert_eq!(pk, pk2); + let aux_rand = AuxRand::from_hex(&t.aux_rand); + let sig2 = sign(msg, sk, aux_rand).unwrap(); + assert_eq!(sig, sig2); + } + let result = t.verification_result == "TRUE"; + assert_eq!(verify(msg, pk, sig).is_ok(), result); + } +} + +fn to_bytes(val: (u128, u128)) -> [u8; 32] { + let (a, b) = val; + let mut out = [0u8; 32]; + out[..16].copy_from_slice(&b.to_le_bytes()); + out[16..].copy_from_slice(&a.to_le_bytes()); + out +} + +#[test] +fn test_sign_verify() { + fn test_q(msg: (u128, u128), sk: (u128, u128), aux_rand: (u128, u128)) -> bool { + let msg = to_bytes(msg); + let sk = to_bytes(sk); + let pk_res = pubkey_gen(sk); + if pk_res.is_err() { + // if there's an error, the secret key is invalid and we don't need + // to try signing + return true; + } + let aux_rand = to_bytes(aux_rand); + // sign also verifies the resulting signature + sign(msg, sk, aux_rand).unwrap(); + true + } + QuickCheck::new() + .tests(12) + .quickcheck(test_q as fn((u128, u128), (u128, u128), (u128, u128)) -> bool); +} diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs index f92cec2be..aca158233 100644 --- a/hax-lib/src/int/mod.rs +++ b/hax-lib/src/int/mod.rs @@ -23,10 +23,10 @@ impl fmt::Display for Int { } impl Int { - fn new(x: impl Into) -> Self { + pub fn new(x: impl Into) -> Self { Int(BigInt::new(&x.into())) } - fn get(self) -> num_bigint::BigInt { + pub fn get(self) -> num_bigint::BigInt { self.0.get() } }