Merge pull request #114 from formosa-crypto/feature/hakyber_mlkem

formosa-mlkem + sct
formosa-crypto · Apr 16, 2024 · 040279b · 040279b
2 parents bc15608 + edffd1c
commit 040279b
Show file tree

Hide file tree

Showing 51 changed files with 136,274 additions and 25 deletions.
diff --git a/.github/workflows/amd64-linux-main-build-instructions.yml.0 b/.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
diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.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
 
       - name: extract and check
         run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make -j$JOBS -C proof/ CI=1 default
@@ -31,14 +31,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

diff --git a/.github/workflows/amd64-linux-main-safety.yml.0 b/.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
 
       - name: compile
         run: (timeout 4300m make -j$JOBS -C src/ CI=1 SAFETY_TIMEOUT=2880m safety) || true
@@ -22,7 +22,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

diff --git a/.github/workflows/amd64-linux-main.yml b/.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
 
       - name: compile
         run: JASMIN=$(which_jasminc) make -j$JOBS -C src/ CI=1 default
@@ -26,7 +26,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
@@ -38,7 +38,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: compile and run
         run: JASMIN=$(which_jasminc) make -j$JOBS -C test/ CI=1 default
@@ -49,7 +49,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
@@ -61,7 +61,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: compile
         run: JASMIN=$(which_jasminc) make -j$JOBS -C src/   CI=1 default
@@ -77,7 +77,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
@@ -89,7 +89,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: compile
         run: JASMIN=$(which_jasminc) make -j$JOBS -C src/   CI=1 default
@@ -105,7 +105,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
@@ -117,7 +117,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: extract and check
         run: JASMIN=$(which_jasminc) EASYCRYPT=$(which_easycrypt) ECARGS=$(which_eclib) make -j$JOBS -C proof/ CI=1 check-extracted
@@ -130,14 +130,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
@@ -149,7 +149,7 @@ jobs:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: compile amd64
         run: JASMIN=$(which_jasminc) make -j$JOBS -C src/ CI=1 default
@@ -162,7 +162,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

diff --git a/bench/Makefile b/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)
 

diff --git a/scripts/ci/config/easycrypt b/scripts/ci/config/easycrypt
@@ -1 +1 @@
-eaba09c215c28b292259bd61aaf575bf7d21dbfe
+2b3bbadffa084466fd3450f367b2102e032c1301
diff --git a/scripts/ci/config/jasmin b/scripts/ci/config/jasmin
@@ -1 +1 @@
-252e602bd76606942d6e1b2aa7d44eb4d09f1712
+7be631a8da1dc3f7c966681028138ae56d8e4610
diff --git a/src/.gitignore b/src/.gitignore
@@ -1,6 +1,8 @@
 *.s
 *.safety
 *.safety_*
+*.sct
+*.sct_*
 *.o
 *.a
 _build/

diff --git a/src/Makefile b/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')
@@ -68,6 +69,14 @@ safety: $(SAFETY)
 $(SAFETY):
 	$(MAKE) -C $(@D) $(@F) || true
 
+# --------------------------------------------------------------------
+
+.PHONY: sct
+sct: $(SCT)
+
+$(SCT):
+	$(MAKE) -C $(@D) $(@F) || true
+
 # --------------------------------------------------------------------
 ifeq ($(CI),1)
 
@@ -83,6 +92,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)
 

diff --git a/src/Makefile.checksct b/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
diff --git a/src/Makefile.common b/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

diff --git a/src/crypto_kem/mlkem/mlkem768/META.yml b/src/crypto_kem/mlkem/mlkem768/META.yml
@@ -0,0 +1,4 @@
+name: MLKEM768
+type: kem
+checksumsmall: 37a3f3e30152b677a3605fbbba9760326a741344edc64df2e9ba23135d745beb
+checksumbig: 5f8345a7632ed05c25db5c3400127242dd187cb2c4ada5cc9dcd581f8b3d81de
diff --git a/src/crypto_kem/mlkem/mlkem768/amd64/avx2/Makefile b/src/crypto_kem/mlkem/mlkem768/amd64/avx2/Makefile
@@ -0,0 +1,3 @@
+SRCS := kem.jazz
+include ../../../../../Makefile.common
+