Tim Taubert

Part one gave a short introduction of bitslicing as a concept, talked aboutits use cases, truth tables, software multiplexers, LUTs, and manual optimization.
The second covered Karnaugh mapping,a visual method to simplify Boolean algebra expressions that takes advantage ofhumans’ pattern-recognition capability, but is unfortunately limited to at mostfour inputs in its original variant....

Bitslicing, in cryptography, is the technique of converting arbitraryfunctions into logic circuits, thereby enabling fast, constant-timeimplementations of cryptographic algorithms immune to cache andtiming-related side channel attacks.
My last post Bitslicing, An Introductionshowed how to convert an S-box function into truth tables, then into a tree ofmultiplexers, and finally how to find the lowest possible gate count throughmanual optimization....

Bitslicing (in software) is an implementation strategy enabling fast,constant-time implementations of cryptographic algorithms immune to cache andtiming-related side channel attacks.
This post intends to give a brief overview of the general technique, not requiringmuch of a cryptographic background. It will demonstrate bitslicing a small S-box,talk about multiplexers, LUTs, Boolean functions, and minimal forms....

Previously I introduced some very basic Cryptol and SAWScript, and explained how to reason about the correctness of constant-time integer multiplication written in C/C++.
In this post I will touch on using formal verification as part of the code review process, in particular show how, by using the Software Analysis Workbench, we saved ourselves hours of debugging when rewriting the GHASH implementation for NSS....