Merge branch 'main' into feature/nix

.github/workflows/amd64-linux-main-build-instructions.yml.0

@@ -12,7 +12,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-instructions]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: build
         run: sh scripts/ci/misc/jasmin-build-instructions0
@@ -21,7 +21,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-instructions]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: build
         run: sh scripts/ci/misc/jasmin-build-instructions1

.github/workflows/amd64-linux-main-proof.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -38,14 +38,14 @@ jobs:
 
       - name: libjade-logs-proof.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-proof.tar.gz
           path: proof/libjade-logs-proof.tar.gz
 
       - name: libjade-dist-proof.tar.gz - contains all EasyCrypt files and test.config
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-dist-proof.tar.gz
           path: libjade-dist-proof.tar.gz

.github/workflows/amd64-linux-main-safety.yml.0

@@ -12,7 +12,7 @@ jobs:
     timeout-minutes: 4320
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -27,7 +27,7 @@ jobs:
 
       - name: libjade-logs-safety.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-safety.tar.gz
           path: src/libjade-logs-src.tar.gz

.github/workflows/amd64-linux-main.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -33,7 +33,7 @@ jobs:
 
       - name: libjade-logs-src.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-src.tar.gz
           path: src/libjade-logs-src.tar.gz
@@ -45,7 +45,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -63,7 +63,7 @@ jobs:
 
       - name: libjade-logs-test.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-test.tar.gz
           path: test/libjade-logs-test.tar.gz
@@ -75,7 +75,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -97,7 +97,7 @@ jobs:
 
       - name: libjade-logs-bench.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-bench1.tar.gz
           path: bench/libjade-logs-bench.tar.gz
@@ -109,7 +109,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -131,7 +131,7 @@ jobs:
 
       - name: libjade-logs-bench.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-bench2.tar.gz
           path: bench/libjade-logs-bench.tar.gz
@@ -143,7 +143,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -166,14 +166,14 @@ jobs:
 
       - name: libjade-logs-proof.tar.gz - contains non-empty logs and errors
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-logs-proof.tar.gz
           path: proof/libjade-logs-proof.tar.gz
 
       - name: libjade-dist-proof.tar.gz - contains all EasyCrypt files and test.config
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-dist-proof.tar.gz
           path: libjade-dist-proof.tar.gz
@@ -185,7 +185,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - uses: DeterminateSystems/magic-nix-cache-action@v4
 
@@ -204,7 +204,7 @@ jobs:
 
       - name: libjade-dist-src-amd64.tar.gz - contains assembly, Jasmin, and how-to-use code
         if: always()
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: libjade-dist-src-amd64.tar.gz
           path: libjade-dist-src-amd64.tar.gz

.gitignore

@@ -2,3 +2,4 @@
 *.tar.gz
 libjade-*
 result
+.vscode

bench/Makefile

@@ -71,7 +71,7 @@ RDIR        = $(subst $(BIN)/,,$(@D))
 
 OPERATION   = $(subst crypto_,,$(word 1, $(subst /, ,$(RDIR))))
 OPERATION1  = $(shell echo $(OPERATION) | tr a-z A-Z)
-NAMESPACE0  = $(subst $(OPERATION)_,,$(subst crypto_,,$(subst -,_,$(subst /,_,$(RDIR)))))
+NAMESPACE0  = $(subst crypto_$(OPERATION)_,,$(subst -,_,$(subst /,_,$(RDIR))))
 NAMESPACE   = jade_$(OPERATION)_$(NAMESPACE0)
 NAMESPACE1  = JADE_$(OPERATION1)_$(NAMESPACE0)
 

scripts/ci/config/easycrypt

@@ -1 +1 @@
-eaba09c215c28b292259bd61aaf575bf7d21dbfe
+2b3bbadffa084466fd3450f367b2102e032c1301

scripts/ci/config/jasmin

@@ -1 +1 @@
-27e45d4aabbedd5c1da1aa8a2d2532f4892baaef
+7be631a8da1dc3f7c966681028138ae56d8e4610

src/.gitignore

@@ -1,6 +1,8 @@
 *.s
 *.safety
 *.safety_*
+*.sct
+*.sct_*
 *.o
 *.a
 _build/

src/Makefile

@@ -22,6 +22,7 @@ SRC     := .
 FILTER  ?= $(SRC)/crypto_%
 JAZZ    ?=  $(filter $(FILTER), $(filter-out $(addprefix ./,$(EXCLUDE)), $(sort $(dir $(shell find $(SRC) -name '*.jazz')))))
 SAFETY  ?= $(addsuffix safety, $(JAZZ))
+SCT     ?= $(addsuffix sct, $(JAZZ))
 
 SOURCES ?= $(filter-out ./, $(sort $(dir $(shell find $(SRC) -name 'Makefile'))))
 ASM     := $(shell find $(SRC) -name '*.s')
@@ -70,6 +71,14 @@ safety: $(SAFETY)
 $(SAFETY):
 	$(MAKE) -C $(@D) $(@F) || true
 
+# --------------------------------------------------------------------
+
+.PHONY: sct
+sct: $(SCT)
+
+$(SCT):
+	$(MAKE) -C $(@D) $(@F) || true
+
 # --------------------------------------------------------------------
 ifeq ($(CI),1)
 
@@ -85,6 +94,9 @@ reporter_safety:
 	./../scripts/ci/reporter/jlog "Safety status" src/ *.safety $(CICL)
 	$(MAKE) $(LOGS)
 
+reporter_sct:
+	./../scripts/ci/reporter/jlog "Speculative constant-time status" src/ *.sct $(CICL)
+
 ERR := $(shell find $(BIN) -name '*.error')
 CIR := $(shell find $(BIN) -name '*.log') $(ERR)
 

src/Makefile.checksct

@@ -0,0 +1,32 @@
+# Notes:
+# - this file defines fine-grained targets that allow checking the speculative constant-time of individual exported
+#   functions
+# - it is meant to be included by Makefile.common
+
+ifneq ($(OP),)
+
+SCT_FLAGS  ?= 
+
+CHECK_SCT_S = ($(JASMINC) -slice $* -checkSCT $(SCT_FLAGS) $< > $@ 2>&1) $(CIT)
+CHECK_SCT   = ($(JASMINC)           -checkSCT $(SCT_FLAGS) $< > $@ 2>&1) $(CIT)
+
+SCT_TARGETS  = $(addsuffix .sct, $(FUNCTIONS))
+
+sct: $(SCT_TARGETS)
+
+$(OP).sct : $(OP).jazz $(DEPS_DIR)/$(OP).sct.d | $(DEPS_DIR) $(CI_DIR)
+	$(DEPS)
+	$(CHECK_SCT)
+
+$(SCT_TARGETS):
+%.sct : $(OP).jazz $(DEPS_DIR)/%.sct.d | $(DEPS_DIR) $(CI_DIR)
+	$(DEPS)
+	$(CHECK_SCT_S)
+
+DEPFILES := \
+ $(DEPFILES) \
+ $(addprefix $(DEPS_DIR)/, $(addsuffix .sct.d, $(FUNCTIONS) $(OP)))
+
+$(SCT_DIR): ; @mkdir -p $@
+
+endif

src/Makefile.common

@@ -100,6 +100,10 @@ $(EC_DIR)/%_ct.ec : %.$(JEXT) $(DEPS_DIR)/%_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI
 
 include $(SRC)/Makefile.checksafety
 
+# --------------------------------------------------------------------
+
+include $(SRC)/Makefile.checksct
+
 # --------------------------------------------------------------------
 $(CHECKSDIR): ; @mkdir -p $@
 $(DEPS_DIR): ; @mkdir -p $@
@@ -129,7 +133,7 @@ include $(wildcard $(DEPFILES))
 .PHONY: clean
 
 clean:
-	@rm -fr $(DEPS_DIR) $(CHECKS_DIR) $(SAFETY_DIR) *.s *.safety* *.o *.a .jflags *.out
+	@rm -fr $(DEPS_DIR) $(CHECKS_DIR) $(SAFETY_DIR) *.s *.safety* *.sct* *.o *.a .jflags *.out
 ifeq ($(CI),1)
 	@rm -fr $(CI_DIR)
 endif

src/common/keccak/common/fips202_DIRTY.jinc

@@ -84,6 +84,63 @@ fn _sha3_256_32(reg ptr u8[32] out, reg ptr u8[KYBER_SYMBYTES] in) -> reg ptr u8
   return out;
 }
 
+#[returnaddress="stack"]
+fn _sha3_256_134(reg ptr u8[32] out, reg ptr u8[134] in) -> reg ptr u8[32]
+{
+  reg u256[7] state;
+  stack u64[28] s_state;
+  stack u64[25] a_jagged_p;
+  reg u64 t l;
+  reg u8 c;
+  inline int i;
+
+  a_jagged_p = KECCAK_A_JAGGED;
+  s_state = __init_s_state_avx2();
+
+  state[0] = #VPBROADCAST_4u64(in[u64 0]);
+
+  for i=1 to 16
+  {
+    t = in[u64 i];
+    l = a_jagged_p[i];
+    s_state[(int) l] = t;
+  }
+
+  c = in[u8 128];
+  l = a_jagged_p[(int) 16];
+  l <<= 3;
+  s_state[u8 (int)l] = c;
+
+  for i = 129 to 134{
+    c = in[i];
+    l += 1;
+    s_state[u8 (int)l] = c;
+  }
+
+  l += 1;
+  s_state[u8 (int)l] = 0x06;
+
+  l = a_jagged_p[(SHA3_256_RATE-1)/8];
+  l <<= 3;
+  t = SHA3_256_RATE - 1; t &= 0x7;
+  l += t;
+  s_state[u8 (int)l] ^= 0x80;
+
+  for i=1 to 7 { state[i] = s_state[u256 i]; }
+
+  state = __keccakf1600_avx2(state);
+
+  for i=0 to 7 { s_state[u256 i] = state[i]; }
+
+  for i=0 to 4
+  {
+    l = a_jagged_p[i];
+    t = s_state[(int)l];
+    out[u64 i] = t;
+  }
+
+  return out;
+}
 
 #[returnaddress="stack"]
 fn _shake256_64(reg u64 out outlen, reg const ptr u8[64] in)

src/common/keccak/common/fips202_ref_DIRTY.jinc

@@ -235,6 +235,40 @@ fn _sha3_256_32(reg ptr u8[32] out, reg ptr u8[KYBER_SYMBYTES] in) -> reg ptr u8
   return out;
 }
 
+
+#[returnaddress="stack"]
+fn _sha3_256_134(reg ptr u8[32] out, reg ptr u8[134] in) -> reg ptr u8[32]
+{
+  stack u64[25] state;
+  stack ptr u8[32] s_out;
+  reg u64 t64;
+  inline int i;
+
+  s_out = out;
+
+  state = __keccak_init_ref1(state);
+
+  for i=0 to 134
+  {
+    state[u8 i] = in[i];
+  }
+
+  state[u8 134] ^= 0x06;
+  state[u8 SHA3_256_RATE - 1] = 0x80;
+
+  state = __keccakf1600_ref1(state);
+
+  out = s_out;
+
+  for i=0 to 4
+  {
+    t64 = state[i];
+    out[u64 i] = t64;
+  }
+
+  return out;
+}
+
 #[returnaddress="stack"]
 fn _sha3_512_64(reg ptr u8[64] out, reg const ptr u8[64] in) -> stack u8[64]
 {