- Untrusted apps need to access/reference protected resources - TCB must “monitor” such references - No reference should be able to bypass the TCB ### TCB Requirements #### Tamper-proof Untrusted code should not be able to alter it #### Complete mediation It cannot be bypassed, and every app/service should need to go through it to access hardware resources #### Correctness No vulnerabilities "Complete formal verification is the only known way to guarantee that a system is free of programming errors." [ref](https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf)