SIMPLE-Crypto's Masked AES in Hardware (SMAesH)

An optimized masked hardware implementation of AES using HPC.

This repository contains the masked AES hardware implementation published by SIMPLE-Crypto.

Main features:

• Supports the three AES variants (i.e., using 128-, 192- or 256-bit key), chosen at run-time.
• Both the encryption and decryption are supported, chosen at run-time.
• The security of the masked architecture is formally proven, and analyzed using the MATCHI tool.
• Implements an optimised architecture of the Sbox, automatically generated using the COMPRESS tool.
• The core performs a single AES execution at a time.
• The required randomness is generated on-the-fly internally to the core, using an embedded PRNG.
• The core stores the long-term key shares, and refreshes the latter at each execution.

See PDF technical documentation and preliminary evaluation report for additional details.

Contents

• hdl: Verilog implementation, apart from the sbox module.
• sbox-compress: Scripts used to generate the sbox module using COMPRESS.
• func_tests: Scripts for functionnal verification, using the cocotb framework and the Verilator simulator.
• formal_verif: Scripts for formal security analysis using MATCHI.
• synth: Script to perform the synsthesis using Yosys and the nangate45 PDK.
• docs: Sources of the technical documentation.

Usage

Clone this repository with its submodules:

git clone https://github.com/simple-crypto/SMAesH.git --recursive

A top-level Makefile is provided in order to easily perform useful operations. The main useful variables to configure the workflows are:

• NSHARES: The amount of shares the consider (default: 2).
• DIR_MATCHI_ROOT: The absolute path to the MATCHI tool repository on your computer (only required in order to run the formal verification checks).
• YOSYS: Path to the yosys's binary installed on your machine (by default, we consider that you have yosys in your PATH).
• WORK: Working directory of the workflow.

The Makefile enables the following commands:

• make sbox: Generate the sbox module using COMPRESS.
• make hdl: Generate the HDL files of the design (in $WORK/hdl).
• make func-tests: Perform the functional tests of the architecture.
• make formal-tests: Perform the formal security verification with MATCHI (requires DIR_MATCHI_ROOT to be set: root directory of the MATCHI repository).

Contact

You are welcome to open issues or discussions on the github repository. You may also contact us privately at [email protected].

License

See LICENSE.txt and COPYRIGHT.txt. See also the SIMPLE-Crypto licensing policy.

Acknowledgements

This work has been funded in part by the Belgian Fund for Scientific Research (F.R.S.-FNRS) through individual researchers' grants, by the European Union (EU) through the ERC project 724725 (acronym SWORD) and the ERC project 101096871 (acronym BRIDGE), and by the Walloon Region through the Win2Wal project PIRATE (convention number 1910082).