Skip to content

Commit 122dfaa

Browse files
mkannwischermkannwischer
committed
Change API of signature_internal and verify_internal to match FIPS204
According to FIPS204, the internal functions take a formated message as input defined as BytesToBits(IntegerToBytes(0, 1) | IntegerToBytes(|ctxlen|, 1) | ctx) | msg However, our current API takes ctx and message separately. This makes it impossible to pass the ACVP tests which only contain one field for the formates message (even worse: those tests apparently do not follow the encoding above making it impossible to parse it and split it into ctx and msg. This commit changes the APIs to match FIPS204, and adds the ACVP tests for the internal functions. It also adjusts the CBMC proofs accordingly. Resolves #40 Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 41cd6f9 commit 122dfaa

File tree

10 files changed

+310
-108
lines changed

10 files changed

+310
-108
lines changed

‎mldsa/sign.c‎

Lines changed: 22 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -453,7 +453,6 @@ MLD_MUST_CHECK_RETURN_VALUE
453453
MLD_EXTERNAL_API
454454
int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
455455
const uint8_t *m, size_t mlen,
456-
const uint8_t *pre, size_t prelen,
457456
const uint8_t rnd[MLDSA_RNDBYTES],
458457
const uint8_t *sk, int externalmu)
459458
{
@@ -474,7 +473,7 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
474473
if (!externalmu)
475474
{
476475
/* Compute mu = CRH(tr, pre, msg) */
477-
mld_H(mu, MLDSA_CRHBYTES, tr, MLDSA_TRBYTES, pre, prelen, m, mlen);
476+
mld_H(mu, MLDSA_CRHBYTES, tr, MLDSA_TRBYTES, m, mlen, NULL, 0);
478477
}
479478
else
480479
{
@@ -550,9 +549,9 @@ int crypto_sign_signature(uint8_t *sig, size_t *siglen, const uint8_t *m,
550549
size_t mlen, const uint8_t *ctx, size_t ctxlen,
551550
const uint8_t *sk)
552551
{
553-
size_t i;
554552
uint8_t pre[257];
555553
uint8_t rnd[MLDSA_RNDBYTES];
554+
uint8_t mu[MLDSA_CRHBYTES];
556555
int result;
557556

558557
if (ctxlen > 255)
@@ -566,26 +565,23 @@ int crypto_sign_signature(uint8_t *sig, size_t *siglen, const uint8_t *m,
566565
/* Prepare pre = (0, ctxlen, ctx) */
567566
pre[0] = 0;
568567
pre[1] = ctxlen;
569-
for (i = 0; i < ctxlen; i++)
570-
__loop__(
571-
assigns(i, object_whole(pre))
572-
invariant(i <= ctxlen)
573-
invariant(ctxlen <= 255)
574-
)
568+
if (ctx != NULL && ctxlen != 0)
575569
{
576-
pre[2 + i] = ctx[i];
570+
mld_memcpy(pre + 2, ctx, ctxlen);
577571
}
578572

573+
mld_H(mu, MLDSA_CRHBYTES, sk + 2 * MLDSA_SEEDBYTES, MLDSA_TRBYTES, pre,
574+
ctxlen + 2, m, mlen);
575+
579576
#ifdef MLD_RANDOMIZED_SIGNING
580577
mld_randombytes(rnd, MLDSA_RNDBYTES);
581578
MLD_CT_TESTING_SECRET(rnd, sizeof(rnd));
582579
#else
583580
mld_memset(rnd, 0, MLDSA_RNDBYTES);
584581
#endif
585582

586-
587-
result = crypto_sign_signature_internal(sig, siglen, m, mlen, pre, 2 + ctxlen,
588-
rnd, sk, 0);
583+
result = crypto_sign_signature_internal(sig, siglen, mu, MLDSA_CRHBYTES, rnd,
584+
sk, 1);
589585

590586
/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
591587
mld_zeroize(pre, sizeof(pre));
@@ -610,8 +606,8 @@ int crypto_sign_signature_extmu(uint8_t *sig, size_t *siglen,
610606
mld_memset(rnd, 0, MLDSA_RNDBYTES);
611607
#endif
612608

613-
result = crypto_sign_signature_internal(sig, siglen, mu, MLDSA_CRHBYTES, NULL,
614-
0, rnd, sk, 1);
609+
result = crypto_sign_signature_internal(sig, siglen, mu, MLDSA_CRHBYTES, rnd,
610+
sk, 1);
615611

616612
/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
617613
mld_zeroize(rnd, sizeof(rnd));
@@ -645,7 +641,6 @@ MLD_MUST_CHECK_RETURN_VALUE
645641
MLD_EXTERNAL_API
646642
int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
647643
const uint8_t *m, size_t mlen,
648-
const uint8_t *pre, size_t prelen,
649644
const uint8_t *pk, int externalmu)
650645
{
651646
unsigned int i;
@@ -678,7 +673,7 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
678673
/* Compute CRH(H(rho, t1), pre, msg) */
679674
uint8_t hpk[MLDSA_CRHBYTES];
680675
mld_H(hpk, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES, NULL, 0, NULL, 0);
681-
mld_H(mu, MLDSA_CRHBYTES, hpk, MLDSA_TRBYTES, pre, prelen, m, mlen);
676+
mld_H(mu, MLDSA_CRHBYTES, hpk, MLDSA_TRBYTES, m, mlen, NULL, 0);
682677

683678
/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
684679
mld_zeroize(hpk, sizeof(hpk));
@@ -756,8 +751,9 @@ int crypto_sign_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
756751
size_t mlen, const uint8_t *ctx, size_t ctxlen,
757752
const uint8_t *pk)
758753
{
759-
size_t i;
760754
uint8_t pre[257];
755+
uint8_t mu[MLDSA_CRHBYTES];
756+
uint8_t hpk[MLDSA_CRHBYTES];
761757
int result;
762758

763759
if (ctxlen > 255)
@@ -767,16 +763,16 @@ int crypto_sign_verify(const uint8_t *sig, size_t siglen, const uint8_t *m,
767763

768764
pre[0] = 0;
769765
pre[1] = ctxlen;
770-
for (i = 0; i < ctxlen; i++)
771-
__loop__(
772-
invariant(i <= ctxlen)
773-
)
766+
if (ctx != NULL && ctxlen != 0)
774767
{
775-
pre[2 + i] = ctx[i];
768+
mld_memcpy(pre + 2, ctx, ctxlen);
776769
}
777770

778-
result =
779-
crypto_sign_verify_internal(sig, siglen, m, mlen, pre, 2 + ctxlen, pk, 0);
771+
/* Compute CRH(H(rho, t1), pre, msg) */
772+
mld_H(hpk, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES, NULL, 0, NULL, 0);
773+
mld_H(mu, MLDSA_CRHBYTES, hpk, MLDSA_TRBYTES, pre, ctxlen + 2, m, mlen);
774+
775+
result = crypto_sign_verify_internal(sig, siglen, mu, MLDSA_CRHBYTES, pk, 1);
780776

781777
/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
782778
mld_zeroize(pre, sizeof(pre));
@@ -790,8 +786,7 @@ int crypto_sign_verify_extmu(const uint8_t *sig, size_t siglen,
790786
const uint8_t mu[MLDSA_CRHBYTES],
791787
const uint8_t *pk)
792788
{
793-
return crypto_sign_verify_internal(sig, siglen, mu, MLDSA_CRHBYTES, NULL, 0,
794-
pk, 1);
789+
return crypto_sign_verify_internal(sig, siglen, mu, MLDSA_CRHBYTES, pk, 1);
795790
}
796791

797792
MLD_MUST_CHECK_RETURN_VALUE

‎mldsa/sign.h‎

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,6 @@ __contract__(
8282
* - size_t *siglen: pointer to output length of signature
8383
* - uint8_t *m: pointer to message to be signed
8484
* - size_t mlen: length of message
85-
* - uint8_t *pre: pointer to prefix string
86-
* - size_t prelen: length of prefix string
8785
* - uint8_t *rnd: pointer to random seed
8886
* - uint8_t *sk: pointer to bit-packed secret key
8987
* - int externalmu: indicates input message m is processed as mu
@@ -101,19 +99,16 @@ MLD_MUST_CHECK_RETURN_VALUE
10199
MLD_EXTERNAL_API
102100
int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
103101
const uint8_t *m, size_t mlen,
104-
const uint8_t *pre, size_t prelen,
105102
const uint8_t rnd[MLDSA_RNDBYTES],
106103
const uint8_t *sk, int externalmu)
107104
__contract__(
108105
requires(mlen <= MLD_MAX_BUFFER_SIZE)
109-
requires(prelen <= MLD_MAX_BUFFER_SIZE)
110106
requires(memory_no_alias(sig, CRYPTO_BYTES))
111107
requires(memory_no_alias(siglen, sizeof(size_t)))
112108
requires(memory_no_alias(m, mlen))
113109
requires(memory_no_alias(rnd, MLDSA_RNDBYTES))
114110
requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
115-
requires((externalmu == 0 && pre != NULL && prelen >= 2 && memory_no_alias(pre, prelen)) ||
116-
(externalmu == 1 && mlen == MLDSA_CRHBYTES))
111+
requires(externalmu == 0 || (externalmu == 1 && mlen == MLDSA_CRHBYTES))
117112
assigns(memory_slice(sig, CRYPTO_BYTES))
118113
assigns(object_whole(siglen))
119114
ensures((return_value == 0 && *siglen == CRYPTO_BYTES) ||
@@ -236,8 +231,6 @@ __contract__(
236231
* - size_t siglen: length of signature
237232
* - const uint8_t *m: pointer to message
238233
* - size_t mlen: length of message
239-
* - const uint8_t *pre: pointer to prefix string
240-
* - size_t prelen: length of prefix string
241234
* - const uint8_t *pk: pointer to bit-packed public key
242235
* - int externalmu: indicates input message m is processed as mu
243236
*
@@ -247,16 +240,13 @@ MLD_MUST_CHECK_RETURN_VALUE
247240
MLD_EXTERNAL_API
248241
int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
249242
const uint8_t *m, size_t mlen,
250-
const uint8_t *pre, size_t prelen,
251243
const uint8_t *pk, int externalmu)
252244
__contract__(
253-
requires(prelen <= MLD_MAX_BUFFER_SIZE)
254245
requires(mlen <= MLD_MAX_BUFFER_SIZE)
255246
requires(siglen <= MLD_MAX_BUFFER_SIZE)
256247
requires(memory_no_alias(sig, siglen))
257248
requires(memory_no_alias(m, mlen))
258249
requires(externalmu == 0 || (externalmu == 1 && mlen == MLDSA_CRHBYTES))
259-
requires(externalmu == 1 || memory_no_alias(pre, prelen))
260250
requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
261251
ensures(return_value == 0 || return_value == -1)
262252
);

‎proofs/cbmc/crypto_sign_signature/Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature
23-
USE_FUNCTION_CONTRACTS=mld_randombytes \
24-
$(MLD_NAMESPACE)signature_internal
23+
USE_FUNCTION_CONTRACTS=mld_randombytes mld_H
24+
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)signature_internal
2525

2626
APPLY_LOOP_CONTRACTS=on
2727
USE_DYNAMIC_FRAMES=1

‎proofs/cbmc/crypto_sign_signature_internal/crypto_sign_signature_internal_harness.c‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,9 @@ void harness(void)
99
size_t *siglen;
1010
uint8_t *m;
1111
size_t mlen;
12-
uint8_t *pre;
13-
size_t prelen;
1412
uint8_t *rnd;
1513
uint8_t *sk;
1614
int externalmu;
1715
int r;
18-
r = crypto_sign_signature_internal(sig, siglen, m, mlen, pre, prelen, rnd, sk,
19-
externalmu);
16+
r = crypto_sign_signature_internal(sig, siglen, m, mlen, rnd, sk, externalmu);
2017
}

‎proofs/cbmc/crypto_sign_verify/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify
2323
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal
24-
USE_FUNCTION_CONTRACTS+=mld_zeroize
24+
USE_FUNCTION_CONTRACTS+=mld_zeroize mld_H
2525

2626
APPLY_LOOP_CONTRACTS=on
2727
USE_DYNAMIC_FRAMES=1

‎proofs/cbmc/crypto_sign_verify_internal/crypto_sign_verify_internal_harness.c‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,8 @@ void harness(void)
99
size_t siglen;
1010
const uint8_t *m;
1111
size_t mlen;
12-
const uint8_t *pre;
13-
size_t prelen;
1412
const uint8_t *pk;
1513
int externalmu;
1614

17-
crypto_sign_verify_internal(sig, siglen, m, mlen, pre, prelen, pk,
18-
externalmu);
15+
crypto_sign_verify_internal(sig, siglen, m, mlen, pk, externalmu);
1916
}

‎test/acvp_client.py‎

Lines changed: 64 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -136,36 +136,48 @@ def run_sigGen_test(tg, tc):
136136
assert tg["testType"] == "AFT"
137137

138138
# TODO: implement pre-hashing mode
139-
if tg["preHash"] != "pure":
139+
if tg["preHash"] == "preHash":
140140
info("SKIP preHash")
141141
return
142142

143-
# TODO: implement internal interface
144-
if tg["signatureInterface"] != "external":
145-
info("SKIP internal")
146-
return
147-
148-
# TODO: implement external-mu mode
149-
if tg["externalMu"] is True:
150-
info("SKIP externalMu")
151-
return
152-
153143
# TODO: probably we want to handle handle the deterministic case differently
154144
if tg["deterministic"] is True:
155145
tc["rnd"] = "0" * 64
156146

157147
assert tc["hashAlg"] == "none"
158-
assert len(tc["context"]) <= 2 * 255
159-
assert len(tc["message"]) <= 2 * 65536
160148

161-
acvp_call = exec_prefix + [
162-
acvp_bin,
163-
"sigGen",
164-
f"message={tc['message']}",
165-
f"rnd={tc['rnd']}",
166-
f"sk={tc['sk']}",
167-
f"context={tc['context']}",
168-
]
149+
if tg["signatureInterface"] == "external":
150+
151+
assert len(tc["context"]) <= 2 * 255
152+
assert len(tc["message"]) <= 2 * 65536
153+
154+
acvp_call = exec_prefix + [
155+
acvp_bin,
156+
"sigGen",
157+
f"message={tc['message']}",
158+
f"rnd={tc['rnd']}",
159+
f"sk={tc['sk']}",
160+
f"context={tc['context']}",
161+
]
162+
else: # signatureInterface=internal
163+
externalMu = 0
164+
if tg["externalMu"] is True:
165+
externalMu = 1
166+
assert len(tc["mu"]) == 2 * 64
167+
msg = tc["mu"]
168+
else:
169+
assert len(tc["message"]) <= 2 * 65536
170+
msg = tc["message"]
171+
172+
acvp_call = exec_prefix + [
173+
acvp_bin,
174+
"sigGenInternal",
175+
f"message={msg}",
176+
f"rnd={tc['rnd']}",
177+
f"sk={tc['sk']}",
178+
f"externalMu={externalMu}",
179+
]
180+
169181
result = subprocess.run(acvp_call, encoding="utf-8", capture_output=True)
170182
if result.returncode != 0:
171183
err("FAIL!")
@@ -187,32 +199,42 @@ def run_sigVer_test(tg, tc):
187199
acvp_bin = get_acvp_binary(tg)
188200

189201
# TODO: implement pre-hashing mode
190-
if tg["preHash"] != "pure":
202+
if tg["preHash"] == "preHash":
191203
info("SKIP preHash")
192204
return
193205

194-
# TODO: implement internal interface
195-
if tg["signatureInterface"] != "external":
196-
info("SKIP internal")
197-
return
198-
199-
# TODO: implement external-mu mode
200-
if tg["externalMu"] is True:
201-
info("SKIP externalMu")
202-
return
203-
204206
assert tc["hashAlg"] == "none"
205-
assert len(tc["context"]) <= 2 * 255
206-
assert len(tc["message"]) <= 2 * 65536
207+
if tg["signatureInterface"] == "external":
208+
assert len(tc["context"]) <= 2 * 255
209+
assert len(tc["message"]) <= 2 * 65536
210+
211+
acvp_call = exec_prefix + [
212+
acvp_bin,
213+
"sigVer",
214+
f"message={tc['message']}",
215+
f"context={tc['context']}",
216+
f"signature={tc['signature']}",
217+
f"pk={tc['pk']}",
218+
]
219+
else: # signatureInterface=internal
220+
externalMu = 0
221+
if tg["externalMu"] is True:
222+
externalMu = 1
223+
assert len(tc["mu"]) == 2 * 64
224+
msg = tc["mu"]
225+
else:
226+
assert len(tc["message"]) <= 2 * 65536
227+
msg = tc["message"]
228+
229+
acvp_call = exec_prefix + [
230+
acvp_bin,
231+
"sigVerInternal",
232+
f"message={msg}",
233+
f"signature={tc['signature']}",
234+
f"pk={tc['pk']}",
235+
f"externalMu={externalMu}",
236+
]
207237

208-
acvp_call = exec_prefix + [
209-
acvp_bin,
210-
"sigVer",
211-
f"message={tc['message']}",
212-
f"context={tc['context']}",
213-
f"signature={tc['signature']}",
214-
f"pk={tc['pk']}",
215-
]
216238
result = subprocess.run(acvp_call, encoding="utf-8", capture_output=True)
217239

218240
if (result.returncode == 0) != tc["testPassed"]:

0 commit comments

Comments
 (0)