formosa-crypto / libjade Goto Github PK

View Code? Open in Web Editor NEW

47.0 15.0 19.0 5.01 MB

Crypto library

Home Page: https://formosa-crypto.org

License: Other

Makefile 0.21% C 97.23% eC 2.36% Shell 0.19% Nix 0.01%

crypto cryptography easycrypt high-speed jasmin postquantumcryptography high-assurance

libjade's People

Contributors

Stargazers

Watchers

Forkers

vbgl dsprenkels tfaoliveira bacelar vincentvbh sitedata haslab qianguo kriskwiatkowski rixxc praveksharma basavesh sarranz cassiersg potsrevennil ruipedro16 joaodiogoduarte j08ny tfaoliveira-sb

libjade's Issues

Extracting SHAKE256

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

Compilation error with Jasmin release 2023.06.1 and main

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).

Failure to build Docker image for CHES23 paper artefacts

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

Use jazzct for (S)CT checking

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:

No support for -I include paths in the jazzct binary, only via JASMINPATH.
For DOIT checking only (jasmin-lang/jasmin#736). No support for -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).

Need fix

libjade/src/crypto_xof/shake256/amd64/avx2/shake256_4x.jinc

Line 21 in 46b86bd

state = __keccakf1600_4x_avx2(state);

Dead assignment

I think the following assignment is dead code and can be removed:

libjade/src/crypto_kem/kyber/common/amd64/ref/reduce.jinc

Line 42 in 0daf13f

r = t;

Fix links in README.md - section 'Properties guaranteed through interactive proofs'

In the section Properties guaranteed through interactive proofs, there are two links about proofs, functional-correctness and security proofs, that are not working:

The corresponding sections need to be written.

Reported via internal communication channels, thanks @karthikbhargavan

Safety checking in CI

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

bit.jinc syntax error

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.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.