The CBE series #4 - Video "A Linux VM on a CBE device"
There is now an online video of the tutorial "The CBE series #3 - A Linux VM on a CBE device" available on Youtube. It goes through the whole tutorial starting with a fresh Sculpt 20.02 installation until the rekeying of the CBE device while rebooting the Linux VM on top of it.
This series of articles describes the features and integration of the Consistent Block Encrypter (CBE) in detail. The CBE is a block-device encryption component with its core logic entirely written in SPARK. It combines multiple techniques to ensure confidentiality, integrity, consistency, and freshness of the block data efficiently. Furthermore, the whole core logic so far passes gnatprove in mode "flow".
In case you are not familiar with the basic structure of the CBE, I'd recommend you this introduction before reading on:
The other articles in this series so far:
The source code on GitHub:
Note that the above branches are not the ones used for the packages in this tutorial. They mark the CBE mainline based on most recent Genode 20.05 while the packages in this tutorial had to be built for Genode 20.02 to be compatible with the most recent Sculpt version.