References:
$A$: for every path.
$E$: there exists a path.
$\boldsymbol{X}_p$: $p$ holds next time.
$\boldsymbol{F}_p$: $p$ holds sometime in the future.
$\boldsymbol{G}_p$: $p$ holds globally in the future.
$p\boldsymbol{U}q$: $p$ holds until $q$ holds.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?