Invariant
makes sure that there is no information
leaks through the register files.
GoodAlgs
makes sure that there are no information leaks through
the shared memory.
GoodAlgs
as an assumption, the proof of
CondSeparation
is valid even if memory protection is
removed from the chip. This opens up for some design choices...