paioli

The paioli (Power Analysis Immunity by Offsetting Leakage Intensity) tool is being developed as part of my PhD work. Its goal is to protect assembly code against power analysis attacks such as DPA (differential power analysis) and CPA (correlation power analysis), and to formally prove the efficiency of the protection. To this end, it implements the automatic insertion of a balancing countermeasure, namely DPL (dual-rail with precharge logic), in assembly code (for now limited to bitsliced block-cipher type of algorithms). Independently, it is able to statically verify if the power consumption of a given assembly code is correctly balanced with regard to a leakage model (e.g., the Hamming weight of values, or the Hamming distance of values updates).

The source code is released under CeCILL license and is available here.

Installation and usage instructions can be found in the README file.

Results

The original work which lead to the developement of paioli has been described in my paper Formally Proved Security of Assembly Code Against Power Analysis, which was presented at PROOFS 2014; an extended version was published in the Journal of Cryptographic Engineering.