Technically, you'll have to formalize and assert the correctness of (at least) the following components: - All ICs having direct (unlimited) access to memory a

Technically, you'll have to formalize and assert the correctness of (at least) the following components: - All ICs having direct (unlimited) access to memory and/or computation (CPU/DMA/GPU/BIOS) - Boot loader - Operating system - Encryption algorithm - Encryption implementation - User-program used to interface with encryption implementation - Input/output peripherals used for encryption and display - Probably a dozen things I'm forgetting here But that's only the system itself. Obviously, you will need to formalize the relationship of the system with the environment. This means: side-channel attacks, such as timing, electro-magnetic radiation, sound and temperature. Finally, you need to formalize the relationship of the user and whatever is encrypted. The user needs to have an understanding of the limitations of the encrypted channel, the used keys and the algorithms involved: what is the availability, the loss of entropy to attackers and the limitations to what can safely be encrypted?