New Vulnerability Announcement on Variable Time Kyber Implementations

4,455 views
Skip to first unread message

Prasanna Ravi

unread,
Dec 30, 2023, 3:24:05 AM12/30/23
to pqc-...@list.nist.gov, Matthias J. Kannwischer, Peter Schwabe

Hello all,

 

Myself and Matthias Kannwischer (in cc) were recently working together on developing an attack to exploit the recently discovered timing vulnerability due to division operation ("/KYBER_Q") in the message decoding procedure (poly_tomsg) used in the decryption procedure. During our analysis, we stumbled upon another another source of timing variability in several patched implementations of Kyber, and thus would like to report this as a new vulnerability disclosure. Unfortunately, the same division vulnerability ("/KYBER_Q") is also present in the compression functions (poly_compress and polyvec_compress) used in the encryption procedure.

 

Refer to https://godbolt.org/z/6anbaK44v for a compiled x86-64 assembly code (with -Os option) of the poly_compress function that contains the division vulnerability. Similarly, refer to https://godbolt.org/z/zG7r7E9a4 for a compiled ARM Cortex-M4 assembly code (with -Os option).

 

We believe, the aforementioned division operations were not considered to be problematic since they were present in the encryption procedure whose ciphertext output is considered to be public. However, the encryption procedure is also used for re-encryption in the FO transformed decapsulation procedure, where the ciphertext output is considered to be sensitive.

 

This bug results in timing variability in the decapsulation procedure, which can be easily exploited through maliciously crafted skewed chosen ciphertexts exploiting a Plaintext Checking (PC) oracle, as shown in [1,2] among several related works. This new bug results in a much higher timing variability compared to the same bug in the decryption procedure, that can be exploited through attacks exploiting side-channel information as a PC oracle.

 

Impact:

 

We have observed this vulnerability in several libraries that are listed in the recently created website by Dr. Daniel J Bernstein (Thank you for creating this nice summary website). This calls for another patch of several Kyber implementations.

https://kyberslash.cr.yp.to/libraries.html

 

With the help of Peter Schwabe (Special Thanks!), we have reached out to several of these teams/projects with this vulnerability disclosure, and hope that a patch will be made soon. We are more than glad to receive feedback on the same.

 

With Thanks and Regards,

Prasanna Ravi.

 

References:

[1] Ravi, Prasanna, Sujoy Sinha Roy, Anupam Chattopadhyay, and Shivam Bhasin. "Generic side-channel attacks on CCA-secure lattice-based PKE and KEMs." IACR transactions on cryptographic hardware and embedded systems (2020): 307-335.

[2] Ueno, Rei, Keita Xagawa, Yutaro Tanaka, Akira Ito, Junko Takahashi, and Naofumi Homma. "Curse of re-encryption: A generic power/EM analysis on post-quantum KEMs." IACR Transactions on Cryptographic Hardware and Embedded Systems (2022): 296-322.

 


CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.

D. J. Bernstein

unread,
Dec 30, 2023, 5:05:25 AM12/30/23
to pqc-...@list.nist.gov
1. Terminology proposal: KyberSlash1 for the division in poly_tomsg;
KyberSlash2 for the divisions in poly_compress and polyvec_compress;
KyberSlash for the general issue.

2. I have a demo exploiting KyberSlash1 to often recover Kyber's
complete secret key from dec timings of the end-of-November-2023 Kyber
reference code running under Raspbian (gcc 8.3.0) on a Raspberry Pi 2.
This has succeeded twice in three experiments: one success was in
399m3.953s, and one success was in 178m40.159s.

To try the demo on your own Raspberry Pi 2, first install

https://github.com/thoughtpolice/enable_arm_pmu

to enable access to the ARM cycle counter. (Probably the demo would also
work with lower-precision timings, or timings collected on another
machine, with minor code changes.) Then run the following:

git clone https://github.com/pq-crystals/kyber
cd kyber
git checkout a621b8dde405cc507cbcfc5f794570a4f98d69cc
cd ref
wget https://cr.yp.to/2023/kyberslash-pi2-20231229.c
gcc \
-Os -g \
-Wall -Wextra -Wpedantic -Wmissing-prototypes -Wredundant-decls -Wshadow -Wpointer-arith \
-DKYBER_K=2 \
kex.c kem.c indcpa.c polyvec.c poly.c ntt.c cbd.c reduce.c verify.c fips202.c symmetric-shake.c randombytes.c \
kyberslash-pi2-20231229.c -o kyberslash
time ./kyberslash > kyberslash.out

The last line of output is "yes, eve succeeded" for successful recovery
of a complete Kyber-512 key. The demo automatically gives up if it
hasn't found the key after 512 loops. I wouldn't be surprised if the
demo also works for Kyber-768 and Kyber-1024 (and then reducing slist to
just -2...2 should give a speedup) but haven't tested that.

In this environment, gcc -Os calls divsi3 for soft division (since gcc
is compiling for an ABI that doesn't guarantee division instructions),
and there's a jump of about 20 cycles for numerators >=3329, plus two
cycles at 4096 and another cycle at 8192. (This isn't the biggest jump
I've observed: the division instruction on a SiFive U74 seems to take
about 60 _more_ cycles for small numerators.) The demo includes some
automatic template collection but obviously can still use improvements.

---D. J. Bernstein
signature.asc

Nadim Kobeissi

unread,
Dec 30, 2023, 5:55:05 AM12/30/23
to Prasanna Ravi, pqc-...@list.nist.gov, Matthias J. Kannwischer, Peter Schwabe

Hi everyone,

Thanks Prasanna and Matthias for the great additional research and thanks to DJB for the practical demo!

This new finding is now also patched in Kyber-K2SO:

https://github.com/symbolicsoft/kyber-k2so/commit/2d16efee71ae195a6aef2fb36f5ed60768d78c98

Of some concern is the fact that these patches in the Kyber reference implementation are leading to a lot of new constants being thrown into the code with little documentation. Between "KyberSlash1" and "KyberSlash2", we can see the following constants added to the reference implementation code:

- 1665 and 80635 in KyberSlash1: https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220

- 40318, 1664, 645084 and 1290167 in KyberSlash2: https://github.com/pq-crystals/kyber/commit/272125f6acc8e8b6850fd68ceb901a660ff48196

I've done some guesswork to try to understand where these values come from:

  • 1665 appears to be math.Ceil(KYBER_Q / 2).
  • 1664 appears to be math.Floor(KYBER_Q / 2).
  • 80635 has unclear origins, I'll call it X.
  • 40318 appears to be math.Ceil(X / 2).
  • 645084 appears to be roughly (X * 8)? Maybe? Something in that region?
  • 1290167 appears to be roughly (X * 16) but again not quite.

It would be clear to get a cleanup of the reference implementations that gives names to these constants. My theory is that they were identified simply as workaround values that allow us to do what the division by KYBER_Q did without messing anything else up, but nevertheless it would be good to have that explained.

Thanks again,

--
You received this message because you are subscribed to the Google Groups "pqc-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pqc-forum+...@list.nist.gov.
To view this discussion on the web visit https://groups.google.com/a/list.nist.gov/d/msgid/pqc-forum/TYZPR01MB411585C4A63FF131FFA02004C79CA%40TYZPR01MB4115.apcprd01.prod.exchangelabs.com.
-- 
Nadim Kobeissi
Symbolic Software - https://symbolic.software

Bas Westerbaan

unread,
Dec 30, 2023, 6:48:14 AM12/30/23
to Nadim Kobeissi, Prasanna Ravi, pqc-...@list.nist.gov, Matthias J. Kannwischer, Peter Schwabe

I've done some guesswork to try to understand where these values come from:

  • 1665 appears to be math.Ceil(KYBER_Q / 2).
  • 1664 appears to be math.Floor(KYBER_Q / 2).
  • 80635 has unclear origins, I'll call it X.
80635 = round(2^28/KYBER_Q)
40318 = round(2^27/KYBER_Q)
645084 = round(2^31/KYBER_Q)
1290167 = round(2^32/KYBER_Q)

The result of a/q can be approximated by computing (a*x) >> s with x/(2^s) close to 1/q. If close enough the results are exact. Same trick is used in Barrett reduction.

D. J. Bernstein

unread,
Dec 30, 2023, 7:46:17 AM12/30/23
to pqc-...@list.nist.gov
I've updated

https://kyberslash.cr.yp.to/libraries.html
https://kyberslash.cr.yp.to/faq.html

for KyberSlash2.

Regarding the documentation question about how to divide in time that
doesn't depend on the numerator, I'd suggest changing the Kyber ref code
to use a single centralized division function with detailed comments. As
an analogy, supercop/crypto_kem/sntrup761/ref/uint32.c includes the code
shown below for unsigned division. I'd also advise Kyber implementors to
test all possible inputs to the division function.

---D. J. Bernstein


/*
CPU division instruction typically takes time depending on x.
This software is designed to take time independent of x.
Time still varies depending on m; user must ensure that m is constant.
Time also varies on CPUs where multiplication is variable-time.
There could be more CPU issues.
There could also be compiler issues.
*/

void uint32_divmod_uint14(uint32 *q,uint16 *r,uint32 x,uint16 m)
{
uint32 v = 0x80000000;
uint32 qpart;
uint32 mask;

v /= m;

/* caller guarantees m > 0 */
/* caller guarantees m < 16384 */
/* vm <= 2^31 <= vm+m-1 */
/* xvm <= 2^31 x <= xvm+x(m-1) */

*q = 0;

qpart = (x*(uint64)v)>>31;
/* 2^31 qpart <= xv <= 2^31 qpart + 2^31-1 */
/* 2^31 qpart m <= xvm <= 2^31 qpart m + (2^31-1)m */
/* 2^31 qpart m <= 2^31 x <= 2^31 qpart m + (2^31-1)m + x(m-1) */
/* 0 <= 2^31 newx <= (2^31-1)m + x(m-1) */
/* 0 <= newx <= (1-1/2^31)m + x(m-1)/2^31 */
/* 0 <= newx <= (1-1/2^31)(2^14-1) + (2^32-1)((2^14-1)-1)/2^31 */

x -= qpart*m; *q += qpart;
/* x <= 49146 */

qpart = (x*(uint64)v)>>31;
/* 0 <= newx <= (1-1/2^31)m + x(m-1)/2^31 */
/* 0 <= newx <= m + 49146(2^14-1)/2^31 */
/* 0 <= newx <= m + 0.4 */
/* 0 <= newx <= m */

x -= qpart*m; *q += qpart;
/* x <= m */

x -= m; *q += 1;
mask = -(x>>31);
x += mask&(uint32)m; *q += mask;
/* x < m */

*r = x;
}
signature.asc

Nadim Kobeissi

unread,
Jan 1, 2024, 4:33:17 AMJan 1
to Bas Westerbaan, Prasanna Ravi, pqc-...@list.nist.gov, Matthias J. Kannwischer, Peter Schwabe

Thank you, Bas! I've updated the code with clearer naming for these new constants:

https://github.com/symbolicsoft/kyber-k2so/commit/f97c7356b2eeca1d3672effe2aca05acd4c4d473

It could be useful for Peter to update the Kyber reference implementation with similar clarifying naming.

--
You received this message because you are subscribed to the Google Groups "pqc-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pqc-forum+...@list.nist.gov.

Rod Chapman

unread,
Jan 2, 2024, 4:03:02 AMJan 2
to pqc-forum, Prasanna Ravi, Matthias J. Kannwischer, Peter Schwabe
I've been reading this thread with some interest, so I've done a little
investigation here of my own implementation.

My code is a completely new reference implementation, written from scratch
without any re-use (or, for that matter, knowledge...) of any existing
Kyber implementation.

It is written in SPARK (the Ada subset, not Apache SPARK, SPARC(tm), or
anything else called SPARK), and verified memory-safe, type-safe, and
free from UB using the FSF release of the SPARK verification tools.

The source is written in the "constant time style" although, as we
have seen, compilers cannot be trusted to preserve such efforts.

I am in the final throes of seeking approval to make the code
available under a suitable permissive licence. I will send a note
separately when that happens.

My experiments have been done with GCC 13.1.0 on AArch64/macOS
and on Intel x86_64/Linux (Ubuntu Focal).

On AArch64/MacOS

1. Compilation of the entire library at -O0, -O1, -O2, -O3 and -Og
results in no divide instructions at all, although the analysis is
somewhat simple-minded... essentially:

  gcc -S -O3 -gnatp mlkem.adb
  grep -i "div" mlkem.s

At these levels, the compiler is always deploying the Barrett/Montgomery
trick to transform division by Q into a multiply/shift sequence.

2. At -Os and -Oz, it generates 12 "udiv" instructions, as follows

 * 1 each in the functions
     Compress1
     CompressDV
     CompressDU
     ByteDecode12
     NTT
     NTT_Inv
     The "*" operator with type signature Poly_Zq x Zq -> Poly_Zq

 * 5 in the function MultiplyNTTs, arising from lines 1 and 2 of
   Algorithm 11 (BaseCaseMultiply) in FIPS 203.

On Intel

As above, but additionally, at -O0,  I get exactly 1 "divq" instruction
in MLKEM_KeyGen(). No idea why that's there.

That's all for now...
 - Rod

Rod Chapman

unread,
Jan 2, 2024, 4:07:57 AMJan 2
to pqc-forum, Prasanna Ravi, Matthias J. Kannwischer, Peter Schwabe
I am also concerned by the presence of an explicit "if" statement
in Algorithm 17 (ML-KEM.Decaps) in the spec.

I originally fell into the trap of implementing this
exactly as written, but Peter S was kind enough to point
out that this really needs to be constant-time as well,
so I refactored it with a CT conditional swap.

In our comments to NIST, we wrote:

"Line 1038, Algorithm 17. Line 7. We note that K__Bar is always computed even though the value may not be needed. We assume this is in order to achieve implicit rejection. A well-meaning implementor might be tempted to move that assignment inside the “if” statement on line 10 in order to improve efficiency. An explicit note here to forbid that optimization might be wise. If both branches of this code are intended to be executed in constant-time, them this should also be stated, or the “if” statement should be replaced with a conditional move or swap procedure."

 - Rod

On Saturday 30 December 2023 at 08:24:05 UTC Prasanna Ravi wrote:

bruno

unread,
Jan 6, 2024, 3:32:34 AMJan 6
to D. J. Bernstein, pqc-...@list.nist.gov
Hi Dan

since you look at the ARM PMU to count the cycle for the non constant
time implementation,  we did that already with XKCP few years ago with
may be more support with ARM V8 and the 64 bits OS cycle counts.

I personally (speaking to myself) found the PMU method pretty painfull
to implement since it requires the Kernel headers (To manage with your
distro) and i did not found (from what I saw) so many differences
compared to methods estimating the cycle from time2freq strategy
(assuming the freq do not vary much on the board like during a burn).  I
guess it depends on the number of iterations for the estimation but the
second strategy appears to me more user friendly for the same results to
bench an algo.

I let the link here if it can be helpful. https://github.com/XKCP/Kernel-PMU

Happy to dig back in time on some ARM from what i remember... if guys
thinks there is a topic with ARM PMU and side channel attack that can't
be solve with Time to Cycle happy...Just drop me an email.

Cheers

Rod Chapman

unread,
Jan 9, 2024, 5:05:30 AMJan 9
to pqc-forum, Prasanna Ravi, Matthias J. Kannwischer, Peter Schwabe
Another question re: constant time in MLKEM.

In NTT and NTT_Inv, the spec tells me to compute (Zeta ** (BitRev7 (K)) mod Q

If I naively write that as an integer exponentiation operator, then the compiler generates a call to
a runtime library routine, which I'd rather not have, and is definitely not constant-time with respect
to the value of the right hand argument anyway.

So... I'm tempted to replace the whole thing by a lookup table, but that leaks the value 
of K via the address bus. On the other hand, the sequence of values of K is predictable
and not a secret, right?

So... am I OK to use a lookup table here?

Thanks,
 Rod



On Saturday 30 December 2023 at 08:24:05 UTC Prasanna Ravi wrote:

Francisco

unread,
Jan 9, 2024, 5:18:23 AMJan 9
to Rod Chapman, pqc-forum, Prasanna Ravi, Matthias J. Kannwischer, Peter Schwabe
Indeed, the way a ZETAS table (e.g. the list ζ^{bit-reversal(i)} / 2¹⁶ mod KYBER_Q) is accessed, is constant for NTT and NTT_inv.
And it should not be used in other algorithms (I don't see why one would), so if context allows, I would make that table accessible only for these algorithms.

Cheers,
--Francisco Vial-Prado

--
You received this message because you are subscribed to the Google Groups "pqc-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pqc-forum+...@list.nist.gov.

Filippo Valsorda

unread,
Jan 9, 2024, 5:22:05 AMJan 9
to Rod Chapman, pqc-...@list.nist.gov
2024-01-09 11:05 GMT+01:00 'Rod Chapman' via pqc-forum <pqc-...@list.nist.gov>:
Another question re: constant time in MLKEM.

In NTT and NTT_Inv, the spec tells me to compute (Zeta ** (BitRev7 (K)) mod Q

If I naively write that as an integer exponentiation operator, then the compiler generates a call to
a runtime library routine, which I'd rather not have, and is definitely not constant-time with respect
to the value of the right hand argument anyway.

So... I'm tempted to replace the whole thing by a lookup table, but that leaks the value 
of K via the address bus. On the other hand, the sequence of values of K is predictable
and not a secret, right?

So... am I OK to use a lookup table here?

Yes, both the values of ζ^BitRev7(k) in NTT/NTT⁻¹ and the values of ζ^2BitRev7(i)+1 in MultiplyNTTs are used in fixed order (in fact, they are used sequentially), so retrieving them naively from a lookup table has no side channel concerns as far as I know.

Even computing them with a variable time function would be fine, since ζ, k, and i are all public, but it's a lot of complexity that's neatly replaced by two 256-byte lookup tables.

Thanks,
 Rod


On Saturday 30 December 2023 at 08:24:05 UTC Prasanna Ravi wrote:

Hello all,

 

Myself and Matthias Kannwischer (in cc) were recently working together on developing an attack to exploit the recently discovered timing vulnerability due to division operation ("/KYBER_Q") in the message decoding procedure (poly_tomsg) used in the decryption procedure. During our analysis, we stumbled upon another another source of timing variability in several patched implementations of Kyber, and thus would like to report this as a new vulnerability disclosure. Unfortunately, the same division vulnerability ("/KYBER_Q") is also present in the compression functions (poly_compress and polyvec_compress) used in the encryption procedure.

 

Refer to https://godbolt.org/z/6anbaK44v for a compiled x86-64 assembly code (with -Os option) of the poly_compress function that contains the division vulnerability. Similarly, refer to https://godbolt.org/z/zG7r7E9a4 for a compiled ARM Cortex-M4 assembly code (with -Os option).

 

We believe, the aforementioned division operations were not considered to be problematic since they were present in the encryption procedure whose ciphertext output is considered to be public. However, the encryption procedure is also used for re-encryption in the FO transformed decapsulation procedure, where the ciphertext output is considered to be sensitive.

 

This bug results in timing variability in the decapsulation procedure, which can be easily exploited through maliciously crafted skewed chosen ciphertexts exploiting a Plaintext Checking (PC) oracle, as shown in [1,2] among several related works. This new bug results in a much higher timing variability compared to the same bug in the decryption procedure, that can be exploited through attacks exploiting side-channel information as a PC oracle.

 

Impact:

 

We have observed this vulnerability in several libraries that are listed in the recently created website by Dr. Daniel J Bernstein (Thank you for creating this nice summary website). This calls for another patch of several Kyber implementations.


https://kyberslash.cr.yp.to/libraries.html

 

With the help of Peter Schwabe (Special Thanks!), we have reached out to several of these teams/projects with this vulnerability disclosure, and hope that a patch will be made soon. We are more than glad to receive feedback on the same.

 

With Thanks and Regards,

Prasanna Ravi.

 

References:


[1] Ravi, Prasanna, Sujoy Sinha Roy, Anupam Chattopadhyay, and Shivam Bhasin. "Generic side-channel attacks on CCA-secure lattice-based PKE and KEMs." IACR transactions on cryptographic hardware and embedded systems (2020): 307-335.

[2] Ueno, Rei, Keita Xagawa, Yutaro Tanaka, Akira Ito, Junko Takahashi, and Naofumi Homma. "Curse of re-encryption: A generic power/EM analysis on post-quantum KEMs." IACR Transactions on Cryptographic Hardware and Embedded Systems (2022): 296-322.

 



CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.


Rod Chapman

unread,
Jan 10, 2024, 7:39:47 AMJan 10
to pqc-forum, Filippo Valsorda, Rod Chapman
One more CT question... hopefully the last...

In the implementation of MLKEM_Decaps (line 9 of Algorithm 17), is the comparison
of C with C_Tick required to be constant-time, or can it terminate early on the first bytes that doesn't match?

My compiler (GCC 13.1.0) currently calls libc's memcmp() for that. OK - or should I write
an explicitly CT comparison function of my own?
 Cheers,
  Rod

Prasanna Ravi

unread,
Jan 10, 2024, 7:53:42 AMJan 10
to Rod Chapman, pqc-forum, Filippo Valsorda, Rod Chapman

Hello Rod,

    Regarding the CT comparison question, the CT comparison should not abort prematurely upon mismatch. It should definitely be constant time. This timing difference can be used as a Decryption Failure oracle when the attacker queries the decapsulation device with crafted ciphertexts. This exact timing vulnerability was exploited in an older implementation of Frodo in the following paper by Guo, Johansson and Nilsson published at Crypto 2020.

 

https://eprint.iacr.org/2020/743.pdf

 

This attack can be easily adapted to Kyber, and the technique used in the following paper by Bhasin et al. can be used to exploit the timing vulnerability:

 

https://eprint.iacr.org/2021/104

 

With Thanks and Regards,

Prasanna Ravi.

 

From: 'Rod Chapman' via pqc-forum <pqc-...@list.nist.gov>
Date: Wednesday, 10 January 2024 at 8:40 PM
To: pqc-forum <pqc-...@list.nist.gov>
Cc: Filippo Valsorda <fil...@ml.filippo.io>, Rod Chapman <roderick...@googlemail.com>
Subject: Re: [pqc-forum] Re: New Vulnerability Announcement on Variable Time Kyber Implementations

[Alert: Non-NTU Email] Be cautious before clicking any link or attachment.

Tommaso Gagliardoni (Kudelski Security)

unread,
Jan 16, 2024, 2:36:04 PMJan 16
to pqc-forum, Prasanna Ravi, Filippo Valsorda, Rod Chapman
Hello from Kudelski Security. We got notified that our crystals-go library ( https://github.com/kudelskisecurity/crystals-go ) was affected by KyberSlash. I would like to announce the following:

1) crystals-go is actually *unmaintained* from our side. This library was written as part of a MsC student project in the Cybersecurity Team at Kudelski Security a few years ago. It is only intended for research and testing, and we discourage its use in any production environment. We apologize for forgetting to mark it as such, the README has been now updated to reflect this, and the repository archived. Feel free to fork if you have interest in continuing the development!

2) Despite this, out of an abundance of caution, we have implemented the necessary fixes for KyberSlash. The library crystals-go has now been patched for both KyberSlash1 and KyberSlash2 as in https://github.com/kudelskisecurity/crystals-go/pull/21 and a security advisory can be found at https://github.com/kudelskisecurity/crystals-go/security/advisories/GHSA-f6jh-hvg2-9525 .

3) Kudelski Security does not use, and has never used, crystals-go as part of their commercial offering or products.

Thanks for reporting this and all the best!
Tommaso

Peter Schwabe

unread,
Jan 18, 2024, 8:05:19 AMJan 18
to Rod Chapman, pqc-forum, Filippo Valsorda
'Rod Chapman' via pqc-forum <pqc-...@list.nist.gov> wrote:

Dear Rod, dear all,

> One more CT question... hopefully the last...
>
> In the implementation of MLKEM_Decaps (line 9 of Algorithm 17), is the
> comparison
> of C with C_Tick required to be constant-time, or can it terminate early on
> the first bytes that doesn't match?
>
> My compiler (GCC 13.1.0) currently calls libc's memcmp() for that. OK - or
> should I write
> an explicitly CT comparison function of my own?

As others have already very nicely answered this question, let me follow
up with another question: Will the implementation that you're working on
be public? I think you mentioned before that it's an Ada implementation
and it sounds like something that would be very useful to have
available.

All the best,

Peter

Roderick Chapman

unread,
Jan 18, 2024, 8:24:40 AMJan 18
to Peter Schwabe, Rod Chapman, pqc-forum, Filippo Valsorda

On 18/01/2024 13:05, Peter Schwabe wrote:

Will the implementation that you're working on
be public? I think you mentioned before that it's an Ada implementation
and it sounds like something that would be very useful to have
available.

It's SPARK (the Ada subset, supported by the its proof tools). The code currently has proofs of memory-safety, type-safety, absence of undefined behaviour, and a few other properties, all purely "auto-active" in that it's all done entirely automatically and based only on the types and contracts in the code.

I am in the final throes of gaining approval from AWS to release this under a suitably permissive licence.

 All the best,

  Rod


Reply all
Reply to author
Forward
0 new messages