The best quote illustrating why things are so difficult in OS security:
“The problem is innately difficult because from the
beginning (ENIAC, 1944), due to the high cost of
components, computers were built to share resources
(memory, processors, buses, etc.). If you look for a
one-word synopsis of computer design philosophy, it
was and is SHARING. In the security realm, the one
word synopsis is SEPARATION: keeping the bad
guys away from the good guys’ stuff!
So today, making a computer secure requires
imposing a “separation paradigm” on top of an
architecture built to share. That is tough! Even when
partially successful, the residual problem is going to
be covert channels. We really need to focus on
making a secure computer, not on making a computer
secure – the point of view changes your beginning
assumptions and requirements! "
His 10 year predictions turned out right, too. Fortunately, we have groups such as CHERI producing secure CPU’s with open hardware. The popularity of Rust, better automation for SPARK proofs, availability of tools such as Cap n' Proto, and increasing use of TLA+ is an improvement in others. Formal verification results in imperative and functional styles have also been pretty incredible. Also still a niche of people building higher quality or security software in both FOSS and commercial sectors.
Far from hope being lost point. Unless we’re talking about what will get mass adoption. ;)
The best quote illustrating why things are so difficult in OS security:
“The problem is innately difficult because from the beginning (ENIAC, 1944), due to the high cost of
components, computers were built to share resources
(memory, processors, buses, etc.). If you look for a
one-word synopsis of computer design philosophy, it
was and is SHARING. In the security realm, the one
word synopsis is SEPARATION: keeping the bad
guys away from the good guys’ stuff!
So today, making a computer secure requires
imposing a “separation paradigm” on top of an
architecture built to share. That is tough! Even when partially successful, the residual problem is going to
be covert channels. We really need to focus on
making a secure computer, not on making a computer secure – the point of view changes your beginning
assumptions and requirements! "
His 10 year predictions turned out right, too. Fortunately, we have groups such as CHERI producing secure CPU’s with open hardware. The popularity of Rust, better automation for SPARK proofs, availability of tools such as Cap n' Proto, and increasing use of TLA+ is an improvement in others. Formal verification results in imperative and functional styles have also been pretty incredible. Also still a niche of people building higher quality or security software in both FOSS and commercial sectors.
Far from hope being lost point. Unless we’re talking about what will get mass adoption. ;)