This repository contains implementations of Ascon-128 and Ascon-128A in Jasmin, and provides a high level interface to these implementations via Rust. The goal is to show that Jasmin is a viable platform to derive an efficient implementation of Ascon's authenticated encryption scheme and evaluate the current state of the Arm version of Jasmin's compiler. The Jasmin code is based on the reference implementations in C found at ascon/ascon-c. The test and benchmarking setup is adapted from the Rust implementation of Ascon found at sebastinas/ascon-aead.
Note: At the time of working on this project the Arm version of the Jasmin compiler was not in a stable state, therefore all implementations are based on the x86_64 version.
See Documentation.
Notes:
- Prefer to install a released version.
See Documentation.
Notes:
- If installed via opam enter environment via
eval $(opam env) - There are two configuration files
why3.confandeasycrypt.conf why3.confholds information about available SMT solverseasycrypt.confseveral parameters for easycrypt- library directories (specific:
idirs, recursive:rdirs) - important when used with emacs / proof-general
- e.g. specify location of jasmin theories
- library directories (specific:
- Can be found at
XDG_CONFIG_HOME; e.g.~/.config/easycrypt)
Example: easycrypt.conf
[general]
pp-width = 120
idirs = Jasmin:/path/to/jasmin/eclib
Compilation, testing, benchmarking and analysis for both implementations can be triggered via a Makefile.
The following general targets exist:
run-rust: compile and execute the demo, comparing the Jasmin implementation with ascon-aead on a fixed input.test-rust: compile and execute the test suite, containing KAT and random input tests. All KAT files taken from ascon-c.bench-rust: compile and execute the benchmark suite. (Requires criterion).
The directory src/x64 contains an implementation of Ascon-128 and Ascon-128A on the x86_64 platform
based on the reference implementation written in C.
The directory src/x64_bi contains an implementation of Ascon-128 and Ascon-128A on the x86_64 platform
with the goal of emulating a 32-bit bit interleaved implementation as good as possible.
The implementation is based on the reference implementation (bi32_armv7m) written in C.
The main goal of this implementation is, to enable an relatively easy port to 32-bit arm versions once the compiler reaches a stable state.
The following constraints apply:
- Only pointers to memory addresses are represented by 64-bit registers.
- Instructions which are only available on the Arm platform are simulated by (one or multiple) available instructions.
The directory src/armv7_bi contains an implementation of Ascon-128 and Ascon-128A on the armv7-m platform
based on the reference implementation written in C and inline assembly.
Note: The assembly generated by the Jasmin compiler is currently not valid, and therefore this implementation is not tested! It should demonstrate the changes required, with respect to the x86_64 32-bit implementation, to enable the arm platform.
At the pointer of writing the following instructions are not implemented:
ornrev
Constant-time evaluation of both implementations is based on the example
of the Jasmin developers and can be found in the proof folder for both implementations.
The model generation and proof execution can be triggered via the make target proof-ct.
Note: The make target expects a path to the eclib folder of the Jasmin installation via the variable JECLIB.
This variable can be specified in the respective Makefile.
The Jasmin compiler has a built-in tool to evaluate the memory safety of an implementation.
This tool takes a configuration file (range_config.json) as input, which can define the ranges for certain values.
The check can be triggered via the make target proof-safety.
Based on the work by "Drunen, Juriaan: Calling Jasmin from Rust" both implementations provide a high level interface in rust.
The thesis can be found in the library folder of the repository.
Main takeaways:
- Jasmin follows the System V AMD64 ABI calling convention (same as Rust on x86_64).
- Jasmin is restricted to function arguments via registers (Maximum 6: RDI, RSI, RDX, RCX, R8, R9 + floating point).
- If more arguments are required, provide pointer to memory region (e.g. this implementation provides one pointer to the key and nonce).
- Jasmin does not mangle its symbols.
Tests and benchmarks are implemented within Rust and are heavily based on the work in ascon-aead.
Both implementations are tested against the KATs generated by the reference implementation ascon-c, as well as random value tests for several scenarios. The KAT tests are based on the implemenation in Rust ascon-aead.
Benchmarks are implemented via the criterion package, with the additional extension criterion-cycle-per-byte. The benchmarks are heavily reliant on the general load of the system and should only be seen as a point of reference!
As of working on this project we found some minor errors in the Arm assembly output of the Jasmin compiler.
- Return from function via
b lr. lr(Link Register R13) is used as a "General Purpose" register..global fooannotation missing.- Certain invalid modifications to the stack pointer (e.g.
and sp sp #-4)
-
Christoph Dobraunig, Maria Eichlseder, Florian Mendel, Martin Schläffer: Ascon v1.2: Lightweight Authenticated Encryption and Hashing. Journal of Cryptology 34(3):33, 2021. https://doi.org/10.1007/s00145-021-09398-9
-
Juriaan Drunen: Calling Jasmin from Rust. Master Thesis Eindhoven University of Technology, 2021. https://pure.tue.nl/ws/portalfiles/portal/199766729/Drunen_Jl.pdf
-
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub: The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy 2020. https://doi.org/10.1109/SP40000.2020.00028