Skip to content

Commit

Permalink
Merge pull request formosa-crypto#68 from formosa-crypto/sliced_safety
Browse files Browse the repository at this point in the history
sliced_safety: safety checking with slices and safety params
  • Loading branch information
tfaoliveira authored Apr 25, 2023
2 parents 8d6e54b + 9bbdf94 commit 7a5548a
Show file tree
Hide file tree
Showing 23 changed files with 683 additions and 373 deletions.
1 change: 1 addition & 0 deletions src/.gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
*.s
*.safety
*.safety_*
*.o
*.a
_build/
Expand Down
34 changes: 34 additions & 0 deletions src/Makefile.checksafety
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
# Notes:
# - this file defines fine-grained targets that allow checking the safety of individual exported
# functions
# - it is meant to be included by Makefile.common, right before the 'generic' safety targets

SAFETY_FLAGS ?=
SAFETY_TIMEOUT ?= 4320m
SAFETY_DIR := .safety
CHECK_SAFETY_S = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -slice $* -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$*.safetyparam) $< 2> $@) $(CIT)
CHECK_SAFETY = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$(OP).safetyparam) $< 2> $@) $(CIT)

SAFETY_TARGETS = $(addsuffix .safety, $(FUNCTIONS))

checksafety-all: $(SAFETY_TARGETS)

$(OP).safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/$(OP).safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR)
$(DEPS)
$(CHECK_SAFETY)

$(SAFETY_TARGETS):
%.safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/%.safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR)
$(DEPS)
$(CHECK_SAFETY_S)

DEPFILES := \
$(DEPFILES) \
$(addprefix $(DEPS_DIR)/, $(addsuffix .safety.d, $(FUNCTIONS) $(OP)))

$(SAFETY_DIR)/$(OP).safetyparam: $(SAFETY_DIR)
$(MAKE) -C $(TEST) bin/$(RDIR)/safetyparams
(cd $(SAFETY_DIR) && $(TDIR)/safetyparams)

$(SAFETY_DIR): ; @mkdir -p $@

87 changes: 42 additions & 45 deletions src/Makefile.common
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,27 @@ PROOF = $(TOP)/proof/

CDIR = $(abspath $(dir $(abspath $(firstword $(MAKEFILE_LIST)))))
RDIR = $(subst $(SRC),,$(CDIR))
TDIR = $(TEST)/bin/$(RDIR)
PDIR = $(PROOF)/$(RDIR)
TDIR = $(TEST)bin/$(RDIR)
PDIR = $(PROOF)$(RDIR)

OPERATION = $(word 1, $(subst /, ,$(RDIR)))
# OPERATION: kem, hash, ...; OP is a shorthand for OPERATION
OPERATION = $(word 2, $(subst _, , $(word 1, $(subst /, ,$(RDIR)))))
OP = $(OPERATION)
NAMESPACE = $(subst crypto_,jade_, $(subst -,_,$(subst /,_,$(RDIR))))

# --------------------------------------------------------------------
CIDIR =

include $(SRC)/Makefile.functions

# --------------------------------------------------------------------
CI_DIR =
CIT =
ifeq ($(CI),1)
CIDIR := .ci
CIT = 2> $(CIDIR)/$(@F).log && rm -f $(CIDIR)/$(@F).error || \
(echo $$? > $(CIDIR)/$(@F).error && \
cat $(CIDIR)/$(@F).log >> $(CIDIR)/$(@F).error && \
rm $(CIDIR)/$(@F).log && \
CI_DIR := .ci
CIT = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \
(echo $$? > $(CI_DIR)/$(@F).error && \
cat $(CI_DIR)/$(@F).log >> $(CI_DIR)/$(@F).error && \
rm $(CI_DIR)/$(@F).log && \
exit 127)
endif

Expand All @@ -34,16 +40,20 @@ JASMINC := $(JASMIN) $(JFLAGS) $(JINCLUDE)
COMPILE = ($(JASMINC) -o $@ $<) $(CIT)

# --------------------------------------------------------------------
include $(SRC)/$(OPERATION)/EcFlags.mk
include $(SRC)/crypto_$(OPERATION)/EcFlags.mk

ECDIR := $(PDIR)
EC_DIR := $(PDIR)
ECFLAGS = $(subst namespace,$(NAMESPACE),$(ECFN)) -oec $(notdir $@)
EXTRACT_S = (cd $(ECDIR) && $(JASMINC) $(ECFLAGS) $(CDIR)/$<) $(CIT)
EXTRACT_CT = (cd $(ECDIR) && $(JASMINC) -CT $(ECFLAGS) $(CDIR)/$<) $(CIT)
EXTRACT_S = (cd $(EC_DIR) && $(JASMINC) $(ECFLAGS) $(CDIR)/$<) $(CIT)
EXTRACT_CT = (cd $(EC_DIR) && $(JASMINC) -CT $(ECFLAGS) $(CDIR)/$<) $(CIT)

# --------------------------------------------------------------------
CHECKS_DIR := checks

# --------------------------------------------------------------------
DEPSDIR := .deps
DEPS = ((printf "$@: "; printf "$(basename $(abspath $*)).$(JEXT) "; $(JASMINC) -print-dependencies $<) > $(DEPSDIR)/$(@F).d) $(CIT)
DEPS_DIR := .deps
DEPS = ((printf "$@: "; printf "$< "; $(JASMINC) -print-dependencies $<) > $(DEPS_DIR)/$(@F).d) $(CIT)
DEPFILES :=

# --------------------------------------------------------------------
compile: $(SRCS:%.$(JEXT)=%.s)
Expand All @@ -52,56 +62,43 @@ compile: $(SRCS:%.$(JEXT)=%.s)
extract: extract_s extract_ct
@true

extract_s: $(SRCS:%.$(JEXT)=$(ECDIR)/%_s.ec)
extract_s: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_s.ec)
@true

extract_ct: $(SRCS:%.$(JEXT)=$(ECDIR)/%_ct.ec)
@true

safety: $(SRCS:%.$(JEXT)=%.safety)
extract_ct: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_ct.ec)
@true

# --------------------------------------------------------------------
%.s : %.$(JEXT)
%.s : %.$(JEXT) $(DEPSDIR)/%.s.d | $(DEPSDIR) $(CIDIR)
%.s : %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR)
@$(DEPS)
@$(COMPILE)

$(ECDIR)/%_s.ec : %.$(JEXT)
$(ECDIR)/%_s.ec : %.$(JEXT) $(DEPSDIR)/%_s.ec.d | $(DEPSDIR) $(ECDIR) $(CIDIR)
$(EC_DIR)/%_s.ec : %.$(JEXT) $(DEPS_DIR)/%_s.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
@$(DEPS)
@$(EXTRACT_S)

$(ECDIR)/%_ct.ec : %.$(JEXT)
$(ECDIR)/%_ct.ec : %.$(JEXT) $(DEPSDIR)/%_ct.ec.d | $(DEPSDIR) $(ECDIR) $(CIDIR)
$(EC_DIR)/%_ct.ec : %.$(JEXT) $(DEPS_DIR)/%_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
@$(DEPS)
@$(EXTRACT_CT)

# --------------------------------------------------------------------
SAFETY_TIMEOUT ?= 1440m
SAFETY_FLAGS_FILE = $(TDIR)/safetyflags.out
SAFETY_FLAGS_ALL = $(SAFETY_FLAGS) $(shell cat $(SAFETY_FLAGS_FILE))

%.safety : %.$(JEXT)
%.safety : %.$(JEXT) $(SAFETY_FLAGS_FILE) $(DEPSDIR)/%.safety.d | $(DEPSDIR) $(CIDIR)
@$(DEPS)
(time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -checksafety $(SAFETY_FLAGS_ALL) $< 2> $@) $(CIT)

$(SAFETY_FLAGS_FILE):
$(MAKE) -C $(TEST) bin/$(RDIR)/$(@F)
include $(SRC)/Makefile.checksafety

# --------------------------------------------------------------------
$(DEPSDIR): ; @mkdir -p $@
$(ECDIR): ; @mkdir -p $@; touch $@/.gitkeep
$(CHECKSDIR): ; @mkdir -p $@
$(DEPS_DIR): ; @mkdir -p $@
$(EC_DIR): ; @mkdir -p $@; touch $@/.gitkeep
ifeq ($(CI),1)
$(CIDIR): ; @mkdir -p $@
$(CI_DIR): ; @mkdir -p $@
endif

DEPFILES := \
$(SRCS:%.$(JEXT)=$(DEPSDIR)/%.s.d) \
$(SRCS:%.$(JEXT)=$(DEPSDIR)/%_s.ec.d) \
$(SRCS:%.$(JEXT)=$(DEPSDIR)/%_ct.ec.d) \
$(SRCS:%.$(JEXT)=$(DEPSDIR)/%.safety.d)
$(DEPFILES) \
$(SRCS:%.$(JEXT)=$(DEPS_DIR)/%.s.d) \
$(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_s.ec.d) \
$(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_ct.ec.d) \
$(SRCS:%.$(JEXT)=$(DEPS_DIR)/%.safety_all.d)

$(DEPFILES):

Expand All @@ -116,8 +113,8 @@ include $(wildcard $(DEPFILES))
.PHONY: clean

clean:
@rm -fr $(DEPSDIR) *.s *.safety *.o *.a .jflags
@rm -fr $(DEPS_DIR) $(CHECKS_DIR) $(SAFETY_DIR) *.s *.safety* *.o *.a .jflags *.out
ifeq ($(CI),1)
@rm -fr $(CIDIR)
@rm -fr $(CI_DIR)
endif

41 changes: 41 additions & 0 deletions src/Makefile.functions
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
ifeq ($(OP),kem)
ifeq ($(SRCS),kem.jazz)
FUNCTIONS = $(addprefix $(NAMESPACE)_, keypair_derand keypair enc_derand enc dec)
endif
endif

ifeq ($(OP),hash)
ifeq ($(SRCS),hash.jazz)
FUNCTIONS = $(NAMESPACE)
endif
endif

ifeq ($(OP),onetimeauth)
ifeq ($(SRCS),onetimeauth.jazz)
FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_verify
endif
endif

ifeq ($(OP),scalarmult)
ifeq ($(SRCS),scalarmult.jazz)
FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_base
endif
endif

ifeq ($(OP),secretbox)
ifeq ($(SRCS),secretbox.jazz)
FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_open
endif
endif

ifeq ($(OP),sign)
ifeq ($(SRCS),sign.jazz)
FUNCTIONS = $(NAMESPACE)_keypair $(NAMESPACE) $(NAMESPACE)_open
endif
endif

ifeq ($(OP),xof)
ifeq ($(SRCS),xof.jazz)
FUNCTIONS = $(NAMESPACE)
endif
endif
1 change: 0 additions & 1 deletion src/crypto_kem/kyber/kyber768/amd64/ref/Makefile
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
SAFETY_TIMEOUT := 4320m
SAFETY_FLAGS := -nocheckalignment
SRCS := kem.jazz
include ../../../../../Makefile.common
Expand Down
52 changes: 31 additions & 21 deletions test/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -70,14 +70,20 @@ FILTER ?= $(SRC)/crypto_%
JAZZ ?= $(filter $(FILTER), $(filter-out $(addprefix $(SRC)/,$(EXCLUDE)), $(sort $(dir $(shell find $(SRC) -name '*.jazz')))))
TESTDIR := $(subst $(SRC),$(BIN), $(JAZZ))

CHECKSUMSMALL := $(addsuffix checksumsmall, $(TESTDIR))
CHECKSUMBIG := $(addsuffix checksumbig, $(TESTDIR))
PRINTPARAMS := $(addsuffix printparams, $(TESTDIR))
FUNCTEST := $(addsuffix functest, $(TESTDIR))
SAFETYFLAGS := $(addsuffix safetyflags, $(TESTDIR))
CHECKSUMSMALL := $(addsuffix checksumsmall, $(TESTDIR))
CHECKSUMBIG := $(addsuffix checksumbig, $(TESTDIR))
PRINTPARAMS := $(addsuffix printparams, $(TESTDIR))
FUNCTEST := $(addsuffix functest, $(TESTDIR))
SAFETYPARAMS := $(addsuffix safetyparams, $(TESTDIR))

EXEC := $(CHECKSUMSMALL) $(CHECKSUMBIG) $(PRINTPARAMS) $(FUNCTEST) $(SAFETYFLAGS)
OUT := $(addsuffix .out, $(EXEC))
CHECKSUMSMALL_OUT := $(addsuffix .out, $(CHECKSUMSMALL))
CHECKSUMBIG_OUT := $(addsuffix .out, $(CHECKSUMBIG))
PRINTPARAMS_OUT := $(addsuffix .out, $(PRINTPARAMS))
FUNCTEST_OUT := $(addsuffix .out, $(FUNCTEST))
SAFETYPARAMS_OUT := $(addsuffix .out, $(SAFETYPARAMS))

EXEC := $(CHECKSUMSMALL) $(CHECKSUMBIG) $(PRINTPARAMS) $(FUNCTEST) $(SAFETYPARAMS)
OUT := $(CHECKSUMSMALL_OUT) $(CHECKSUMBIG_OUT) $(PRINTPARAMS_OUT) $(FUNCTEST_OUT) $(SAFETYPARAMS_OUT)

# --------------------------------------------------------------------

Expand All @@ -93,6 +99,7 @@ DNAMESPACES = -DJADE_NAMESPACE=$(NAMESPACE1) -DJADE_NAMESPACE_LC=$(NAMESPACE)
INCLUDES = -I$(IDIR)/include/ -I$(COMMON)/ -Iinclude/
PRINT = common/print.c
COMPILE = $(CC) $(CFLAGS) -o $@ $(DEFINE) $(DNAMESPACES) $(INCLUDES) crypto_$(OPERATION)/$(@F).c $(PRINT) $(ASM) $(RANDSRC) $(CIL)
COMPILE_P = $(CC) $(CFLAGS) -o $@ $(DEFINE) $(DNAMESPACES) $(INCLUDES) crypto_$(OPERATION)/$(@F).c $(PRINT) $(RANDSRC) $(CIL)

# --------------------------------------------------------------------
.PHONY: __phony default
Expand All @@ -115,34 +122,37 @@ include Makefile.partial_implementations
$(COMPILE) || true

%/printparams: __phony | %/ %/$(CID)
$(MAKE) -C $(IDIR) || true
$(CIC)
$(COMPILE) || true
$(COMPILE_P) || true

%/functest: __phony | %/ %/$(CID)
$(MAKE) -C $(IDIR) || true
$(CIC)
$(COMPILE) || true

%/safetyflags: __phony | %/ %/$(CID)
$(MAKE) -C $(IDIR) || true
%/safetyparams: __phony | %/ %/$(CID)
$(CIC)
$(COMPILE) || true
$(COMPILE_P) || true

$(OUT):
%.out: %
$(CIC)
./$* > $@ $(CIL) || true
(cd $(dir $*) && ./$(notdir $*) > $(notdir $*).out) $(CIL) || true

# --------------------------------------------------------------------
checksumsmall-all: $(CHECKSUMSMALL)
checksumbig-all: $(CHECKSUMBIG)
printparams-all: $(PRINTPARAMS)
functest-all: $(FUNCTEST)
safetyflags-all: $(SAFETYFLAGS)
checksumsmall-all: $(CHECKSUMSMALL)
checksumbig-all: $(CHECKSUMBIG)
printparams-all: $(PRINTPARAMS)
functest-all: $(FUNCTEST)
safetyparams-all: $(SAFETYPARAMS)

checksumsmall-out-all: $(CHECKSUMSMALL_OUT)
checksumbig-out-all: $(CHECKSUMBIG_OUT)
printparams-out-all: $(PRINTPARAMS_OUT)
functest-out-all: $(FUNCTEST_OUT)
safetyparams-out-all: $(SAFETYPARAMS_OUT)

# --------------------------------------------------------------------

$(TESTDIR): ; @mkdir -p $@
ifeq ($(CI),1)
.PRECIOUS: %/$(CID)
Expand All @@ -161,12 +171,12 @@ reporter:
$(MAKE) $(LOGS)

reporter_compilation:
@for type in checksumsmall checksumbig printparams functest safetyflags; do \
@for type in checksumsmall checksumbig printparams functest safetyparams; do \
./../scripts/ci/reporter/jlog "Compilation status - $$type" test/$(BIN) $$type $(CICL); \
done

reporter_execution:
@for type in checksumsmall checksumbig printparams functest safetyflags; do \
@for type in checksumsmall checksumbig printparams functest safetyparams; do \
./../scripts/ci/reporter/jlog "Execution status - $$type" test/$(BIN) $$type.out $(CICL); \
done

Expand Down
46 changes: 46 additions & 0 deletions test/common/files.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
#ifndef TEST_COMMON_FILES_C
#define TEST_COMMON_FILES_C

#include <stdio.h>
#include <stdint.h>
#include <assert.h>
#include <stdarg.h>

static void f_map_fopen(FILE **files, char **filenames, size_t length, char *mode)
{
size_t i;
for(i=0; i<length; i++)
{ files[i] = fopen(filenames[i], mode);
assert(files[i] != NULL);
}
}

static void f_map_fclose(FILE **files, size_t length)
{
int r;
size_t i;
for(i=0; i<length; i++)
{ r = fclose(files[i]);
assert(r == 0);
}
}

static void f_map_fopen_write(FILE **files, char **filenames, size_t length)
{
f_map_fopen(files, filenames, length, "w");
}

static void f_fprintf2(FILE *stream1, FILE *stream2, const char *format, ...)
{
va_list arguments;

va_start(arguments, format);
vfprintf(stream1, format, arguments);
va_end(arguments);

va_start(arguments, format);
vfprintf(stream2, format, arguments);
va_end(arguments);
}

#endif
Loading

0 comments on commit 7a5548a

Please sign in to comment.