formosa-crypto / libjade Goto Github PK
View Code? Open in Web Editor NEWCrypto library
Home Page: https://formosa-crypto.org
License: Other
Crypto library
Home Page: https://formosa-crypto.org
License: Other
Make sure that the jasmin safety checker checks all implementations through CI tests.
Figure out the safetyparams string for the different functionalities to ensure memory
safety also for external memory
In the section Properties guaranteed through interactive proofs, there are two links about proofs, functional-correctness and security proofs, that are not working:
Reported via internal communication channels, thanks @karthikbhargavan
Dear Team,
I am trying to utilise the SHAKE256 in the libjade library. Is there an extracted SHAKE256 file and would like to know about .jinc extension files. Can you provide any documentation on how I can include jinc files with my C code.
Looking forward to your reply.
Regards
Samyuktha
Hi,
I'm getting the following error
root@fc8f5c17d6fa:~/jasmin/libjade/src/crypto_scalarmult/curve25519/amd64/mulx# make
"/root/jasmin/libjade/src/crypto_scalarmult/curve25519/amd64/common/bit.jinc", line 11 (2-17)
from "curve25519.jinc", line 76 (2-26)
from "curve25519.jinc", line 113 (4) to line 114 (70)
from "curve25519.jinc", line 138 (2-40)
from "curve25519.jinc", line 173 (2-39)
from "scalarmult.jazz", line 14 (2-31):
compilation error in function jade_scalarmult_curve25519_amd64_mulx_base:
asmgen: invalid rexpr for oprd (RSI & ((64u) 63))
invalid rexpr for word
make: *** [../../../../Makefile.common:68: scalarmult.s] Error 1
I feel its line 11 in bit.jinc
which states
bit >>= p & 63;
I am no expert, but when I change it to
bit >>= p;
bit &= 63;
the compilation works.
It feels correct, because p &= 7;
just before, so bit >>= (p&63)
does not make much sense.
Dear Jasmin/LibJade/Easycrypt team.
I am trying to build the Docker image for the artefacts that accompany the CHES'23 "Formally verifying Cyber" paper.
I am using Docker version 20.10.17, build 100c701 on an Intel-baed Mac, running macOS 13.3.1
Following the README.md file, I get
docker build -t hakyber .
[+] Building 1406.8s (20/22)
=> [internal] load build definition from Dockerfile 0.0s
=> => transferring dockerfile: 1.16kB 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 2B 0.0s
=> [internal] load metadata for docker.io/library/debian:latest 1.7s
=> [ 1/18] FROM docker.io/library/debian:latest@sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b85 11.7s
=> => resolve docker.io/library/debian:latest@sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b8511c 0.0s
=> => sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b8511cc89ee09 1.85kB / 1.85kB 0.0s
=> => sha256:32888a3c745e38e72a5f49161afc7bb52a263b8f5ea1b3b4a6af537678f29491 529B / 529B 0.0s
=> => sha256:34b4fa67dc04381e908b662ed69b3dbe8015fa723a746c66cc870a5330520981 1.46kB / 1.46kB 0.0s
=> => sha256:918547b9432687b1e1d238e82dc1e0ea0b736aafbf3c402eea98c6db81a9cb65 55.05MB / 55.05MB 9.7s
=> => extracting sha256:918547b9432687b1e1d238e82dc1e0ea0b736aafbf3c402eea98c6db81a9cb65 1.8s
=> [internal] load build context 0.4s
=> => transferring context: 14.51MB 0.4s
=> [ 2/18] WORKDIR /root 0.2s
=> [ 3/18] RUN apt update && apt install -y --force-yes opam cvc4 vim gcc clang 99.6s
=> [ 4/18] RUN opam init --auto-setup -y --disable-sandboxing -c ocaml-base-compiler.4.12.0 123.9s
=> [ 5/18] RUN eval $(opam env) 0.2s
=> [ 6/18] COPY ./ /root/ 0.2s
=> [ 7/18] RUN opam pin -yn add easycrypt /root/easycrypt 0.9s
=> [ 8/18] RUN opam pin -yn add jasmin /root/jasmin 0.9s
=> [ 9/18] RUN opam repo add coq-released https://coq.inria.fr/opam/released && opam pin -yn add coq-mathcomp- 3.7s
=> [10/18] RUN opam install -y depext 6.2s
=> [11/18] RUN opam depext -y easycrypt && opam install -y easycrypt 137.8s
=> [12/18] RUN opam depext -y alt-ergo.2.4.1 z3.4.8.14 9.9s
=> [13/18] RUN opam install -y alt-ergo.2.4.1 z3.4.8.14 602.0s
=> [14/18] RUN eval $(opam env) && easycrypt why3config 0.4s
=> [15/18] RUN opam depext -y jasmin && opam install -y --deps-only jasmin 405.5s
=> ERROR [16/18] RUN eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make instal 2.1s
------
> [16/18] RUN eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make install:
#20 0.345 [WARNING] Running as root is not recommended
#20 0.351 rm -f CIL/*.ml CIL/*.mli ../proofs/extraction.vo
#20 0.352 make -C ../proofs extraction
#20 0.353 make[1]: Entering directory '/root/jasmin/proofs'
#20 0.353 coq_makefile -f _CoqProject -o Makefile.coq
#20 0.356 rm -f lang/ocaml/*.ml lang/ocaml/*.mli
#20 0.358 rm -f lang/extraction.vo
#20 0.359 make -f Makefile.coq lang/extraction.vo
#20 0.360 make[2]: Entering directory '/root/jasmin/proofs'
#20 0.407 COQDEP VFILES
#20 0.465 *** Warning: in file 3rdparty/ssrring.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.465 *** Warning: in file arch/arch_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.466 *** Warning: in file arch/arch_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.466 *** Warning: in file arch/arch_sem.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.468 *** Warning: in file arch/spp_arch_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.468 *** Warning: in file compiler/allocation.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.470 *** Warning: in file compiler/arm_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.470 *** Warning: in file compiler/arm_instr_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.473 *** Warning: in file compiler/arm_instr_decl_lemmas.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.473 *** Warning: in file compiler/arm_lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.474 *** Warning: in file compiler/arm_lowering_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.475 *** Warning: in file compiler/arm_params_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.476 *** Warning: in file compiler/array_expansion.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.476 *** Warning: in file compiler/array_expansion_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.477 *** Warning: in file compiler/array_copy_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.480 *** Warning: in file compiler/constant_prop.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.483 *** Warning: in file compiler/lea.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.485 *** Warning: in file compiler/lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.488 *** Warning: in file compiler/propagate_inline.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.489 *** Warning: in file compiler/remove_globals.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.489 *** Warning: in file compiler/remove_globals_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.490 *** Warning: in file compiler/stack_alloc.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.491 *** Warning: in file compiler/stack_alloc_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.493 *** Warning: in file compiler/stack_alloc_proof_2.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.497 *** Warning: in file compiler/x86_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.497 *** Warning: in file compiler/x86_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.498 *** Warning: in file compiler/x86_instr_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.499 *** Warning: in file compiler/x86_lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.500 *** Warning: in file compiler/x86_lowering_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.502 *** Warning: in file compiler/x86_params.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.502 *** Warning: in file compiler/x86_params_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.503 *** Warning: in file lang/array.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.503 *** Warning: in file lang/expr.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.505 *** Warning: in file lang/gen_map.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.505 *** Warning: in file lang/global.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.506 *** Warning: in file lang/low_memory.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.507 *** Warning: in file lang/memory_model.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.509 *** Warning: in file lang/sem.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.510 *** Warning: in file lang/sem_op_typed.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.511 *** Warning: in file lang/sem_type.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.511 *** Warning: in file lang/utils.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.512 *** Warning: in file lang/values.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.514 *** Warning: in file lang/warray_.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.515 *** Warning: in file lang/word.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.568 COQC 3rdparty/xseq.v
#20 0.569 COQC ssrmisc/oseq.v
#20 1.252 COQC 3rdparty/ssrring.v
#20 1.279 COQC lang/shift_kind.v
#20 1.363 COQC lang/utils.v
#20 1.649 File "./3rdparty/ssrring.v", line 10, characters 0-39:
#20 1.649 Error: Cannot find a physical path bound to logical path
#20 1.649 ssrZ with prefix mathcomp.word.
#20 1.649
#20 1.704 make[2]: *** [Makefile.coq:793: 3rdparty/ssrring.vo] Error 1
#20 1.704 make[2]: *** Waiting for unfinished jobs....
#20 1.977 File "./lang/utils.v", line 7, characters 0-39:
#20 1.977 Error: Cannot find a physical path bound to logical path
#20 1.977 ssrZ with prefix mathcomp.word.
#20 1.977
#20 2.049 make[2]: Leaving directory '/root/jasmin/proofs'
#20 2.049 make[2]: *** [Makefile.coq:793: lang/utils.vo] Error 1
#20 2.049 make[1]: *** [Makefile:20: extraction] Error 2
#20 2.049 make[1]: Leaving directory '/root/jasmin/proofs'
#20 2.050 make: *** [Makefile:70: CIL] Error 2
------
executor failed running [/bin/sh -c eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make install]: exit code: 2
Add API documentation for all functionalities in Libjade in doc/api.md
The (S)CT checking in Jasmin is now done via the jazzct
standalone checker (jasmin-lang/jasmin#766).
Thus, Makefile.checksct
should use that (it is currently broken, AFAICT).
The blockers are:
-I
include paths in the jazzct
binary, only via JASMINPATH
.-lea
, -lazy-regalloc
or -noinsertarraycopy
in jazzct
, as these matter when checking is done after many compiler passes (and some primitives do not compile without them).Libjade release 2023.05-1 is tested against Jasmin release 2022.09.3 (as per README) --- that works fine. For Jasmin release 2023.06.1 and main, each produce compilation errors ("linearization: assign remains") for scalar multiplication (and for falcon512).
Add reference and AVX2 implementations of Kyber1024
I think the following assignment is dead code and can be removed:
Add (reference and AVX2) implementations of Dilithium2, Dilithium3, and Dilithium5.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.