3 ms·
> It's impossible to determine whether software is malicious or not (Rice's theorem). Which is why proof-carrying code [https://en.wikipedia.org/wiki/Proof-car
by catnaroek 11y ago
> It's impossible to determine whether software is malicious or not (Rice's theorem).
Which is why proof-carrying code [https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code] is a good idea: the onus ought to be on the programmer to provide (machine-checkable) evidence that their program is safe to use, for whatever notion of “safe” might make sense in your system.
- nickpsecurity 11y agoThat's still in its infancy. Future results might counter what we figured out. The certified compilers are nice for subversion-resistant development but not running untrustworthy code. There's significant difference between their models and the software/hardware combo actually running. Better route was started in Burrough's where you pick a language good at correct programs and carefully design a safe machine around it. Same with System/38, SAFE (crash-safe.org) for functional, and Cambrige's CHERI for C language. The fundamentals work as advertised along with ability to enforce arbitrary security policies. Then design and security stuff are built on that. Only thing known to work consistently to any degree of success. On COTS hardware, separation kernels and compiler transforms on legacy code are about best that we can do.