Jasmin 2024.07.0

This is a major release of Jasmin.

For a complete list of changes, please have a look at the CHANGELOG. Below are a few highlights.

Arrays in the arguments and results of functions

A long-awaited feature has landed! Export functions can have reg ptr arrays as arguments and results.

Another improvement has been made regarding functions and arrays. Local functions can have reg arrays and sub-arrays as arguments and results.

Selective Speculative Load Hardening support

The compiler supports SLH operators, and a speculative constant-time checker is available. It can be called with jasmin-ct --sct.

Easy spills and unspills

Spilling and unspilling of reg and reg ptr can now be done without introducing stack variables, thanks to the #spill and #unspill operators.

More flexible parameters

The definition of parameters can now use arbitrary expressions and depend on other parameters.

Stack zeroization support

The compiler can introduce code that zeroizes the stack at the end of export functions. The user can enable the feature with an annotation or a compiler flag.

Help for debugging

Option -g adds source-code positions in the generated assembly files, which can help for debugging.

Enhancements to the support of the ARMv7 architecture

The support for the ARMv7 instruction set has been polished. In particular, some issues with large immediates have been fixed. The support for ARMv7 is still marked as experimental, but this is expected to change in the next releases.

Other noteworthy changes

Extraction to EasyCrypt for safety verification is deprecated.

The deprecated legacy interface to the CT checker has been removed.

Jasmin 2023.06.4

This is a minor release of Jasmin.

It has better compatibility with recent versions of GNU binutils.

It brings support for a few x86 instructions from the VAES and BMI2 extensions.

The command line interface to the constant-time checker has been renamed to jasmin-ct. The pretty-printer of Jasmin programs has been renamed to jasmin2tex.

Relevant details can be found through the CHANGELOG.

Jasmin 2023.06.3

This is a minor release of Jasmin. Here is a brief description of a few of the changes it features.

Programmers no longer need to prove that memory accesses and (direct) array accesses are properly aligned. Jasmin programs have a well-defined semantics even if unaligned accesses occur.

The checker for Constant-Time security is now available as a separate jazzct tool. It also ensures that division and modulo operators may only be used with public arguments.

To better understand register-allocation issues, the new command-line option -pliveness displays the program annotated with liveness information.

The compiler now warns when some variable declarations are not used or shadow any earlier declaration.

Namespaces allow reusing names: two things may have the same name, as long as they belong to different namespaces. This feature can also be abused to reuse implementations, but it is not advised to do so.

Many smaller fixes and additions have also been incorporated in this minor release. Relevant details can be found through the CHANGELOG.

Jasmin 2023.06.2

This is a minor release of Jasmin,featuring:

• fixes and improvements to the (still experimental) support for ARMv7 architecture (more intrinsics, better instruction selection, added support for flag combinations);
• array indexing expressions no longer need to be explicitly cast to the int type.

Find out more details in the CHANGELOG.

Jasmin 2023.06.1

This is a minor release of Jasmin,featuring:

• a few improvements to the (still experimental) support for ARMv7 architecture;
• fixes to the semantics description of the target architectures;
• literal strings to define global arrays of bytes.

Find out more details in the CHANGELOG.

Jasmin 2023.06.0

This is a major release of Jasmin. It contains a few noteworthy changes:

• local functions now use call and ret instructions;
• experimental support for the ARMv7 (i.e., Cortex-M4) architecture;
• a few aspects of the safety checker can be finely controlled through annotations or command-line flags;
• shift and rotation operators have a simpler semantics.

As usual, it also brings in various fixes and improvements, such as bit rotation operators and automatic slicing of the input program.

More details can be found in the CHANGELOG.

Jasmin 2022.09.3

This is a minor release of Jasmin. It features a few fixes (e.g., to the semantics of a few x86 instructions) and additions (e.g., x86 instructions for carry-less multiplications). Moreover, it provides improved compatibility with the future major release of the Jasmin compiler (e.g., shift amounts can be explicitly truncated to the word size).

More details can be found in the CHANGELOG.

Jasmin 2022.09.2

This is a minor release of Jasmin. It brings in the support of new x86 instructions, of new compound assignments (modulo and division), and, most importantly, many fixes, especially to the safety checker.

(Jasmin 2022.09.2 fixes an oversight in Jasmin 2022.09.1's AUTHORS file.)

More details can be found in the CHANGELOG.

Jasmin 2022.09.0

This is the third stable release of Jasmin. It contains the following major improvements:

• a new instruction #randombytes to fill an array with “random” data;
• access to mmx registers;
• support for Windows calling convention, in addition to Linux, with -call-conv {windows|linux};
• else if blocks for readability;
• strict preservation of source-level intrinsics;
• an option to extract all the functions of a file to EasyCrypt;
• many fixes to the extraction to EasyCrypt.

It also brings in other new features, as well as new contributors, many fixes, and various improvements.

More details can be found in the CHANGELOG.

Jasmin 2022.04.0

This is the second stable release of Jasmin. It capitalizes on more than two years of active development, so it contains a lot of new features, including breaking ones. Please beware of these breaking changes if you want to upgrade from an older version.

Here is a list of the most salient new features. Please take a look at the changelog for a more detailed and exhaustive list.

• Jasmin features proper internal functions, called subroutines, that are neither inline or export. Breaking change: using fn alone in a function declaration declares a subroutine, not an inline function anymore.
• Two storage modifiers, reg ptr and stack ptr, were introduced to store the address of an array in a register and on the stack, respectively. The main use of reg ptr arrays is to pass stack arrays as arguments to subroutines, since they do not accept stack arrays as arguments directly.
• Global immutable arrays are now supported. A global array must be initialized at the same time it is declared.
• It is now possible to manipulate slices of arrays, called sub-arrays. The concrete syntax is a[pos:len] to specify the slice of array a starting at index pos and of length len. pos and len must be compile-time constants.
• It is now possible to attach annotations to functions and instructions, using #[annotation] or #[annotation=value]. The compiler takes into account the ones that it knows about, and ignores the others.
• Including a Jasmin file in another one is now a native feature of Jasmin. The concrete syntax is require "file.jazz" or from ident require "file.jazz" for more complex use cases.
• Boolean flags and some combinations thereof can now be referred to by their names, improving readability.
• Variable declarations don't have to be at the start of the function body anymore, they can now appear anywhere in the body.
• The compiler includes a type-checker for cryptographic constant time that infers security types for functions, based on the security annotations given by the user. This is an alternative to using the constant time extraction to EasyCrypt. The type-checker should be easier to use in most cases.

If you are not interested in the Coq part of Jasmin, you can download the archive jasmin-compiler-v2022.04.0.tar.bz2 below which contains only OCaml code. See the installation instructions for more details.