Modern operating systems strive to reduce the size of the TCB[not verified in body] so that an exhaustive examination of its code base (by means of manual or computer-assisted software audit or program verification) becomes feasible.
[4] As a consequence of the above Orange Book definition, the boundaries of the TCB depend closely upon the specifics of how the security policy is fleshed out.
This obviously includes operations that would be deemed contrary to all but the simplest security policies, such as divulging an email or password that should be kept secret; however, barring special provisions in the architecture of the system, there is no denying that the computer could be programmed to perform these undesirable tasks.
These special provisions that aim at preventing certain kinds of actions from being executed, in essence, constitute the trusted computing base.
As outlined by the aforementioned Orange Book, software portions of the trusted computing base need to protect themselves against tampering to be of any effect.
This is due to the von Neumann architecture implemented by virtually all modern computers: since machine code can be processed as just another kind of data, it can be read and overwritten by any program.
[8] This makes seL4 the first operating-system kernel which closes the gap between trust and trustworthiness, assuming the mathematical proof is free from error.