4 ms·

Formal verification (what this seems to be about) can be a nice tool to verify something adheres to a specification or that it has no e.g. buffer overflows. Bu

Formal verification (what this seems to be about) can be a nice tool to verify something adheres to a specification or that it has no e.g. buffer overflows. But I think that is not really the big problem we have. I think it is operating system interfaces. By default a process is in its own address space and cannot do anything dangerous. It is only with the operating system API (which is the syscalls or an C API that uses syscalls) that it can do dangerous things like writing in the filesystem. Posix defines such an API which allows every program to do the same as the user running it. Windows does the same. This would be fine in a world where we can trust each program we run to not be malicious and to not be exploitable. Now we are trying to make those inherently unsafe APIs safe via sandboxing, but I guess that it is much easier to create a new API that is safe from the beginning.

jojo3000 10y ago
This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big problem! But lets assume this is solved. Then a API can be checked for certain properties. You can specify what it means that something is read-only in an environment etc. And ensure that it is enforced by the operating system. As example: the verification of seL4 not only guarantees avoidance of classical security holes (buffer overflows etc.) but also certain non-interference properties.
IshKebab 10y ago
> But I think that is not really the big problem we have. It is a really big problem and it needs to be solved. Did you miss this recent news? http://www.theregister.co.uk/2016/10/21/linux_privilege_escalation_hole/ http://www.theregister.co.uk/2016/10/21/linux_privilege_esca...
nickpsecurity 10y ago
Formal verification isn't as limited as you suggest. The original use of formal verification for security in high-assurance security was analysis of security kernels for OS's showing that every state the system could be in was secure or fail-safe. Early attempts like UCLA Secure UNIX showed UNIX was impossible to secure because the API's inherently leaked and/or gave attackers opportunities. That's why high-assurance projects abandoned them in favor of security kernels with user-mode version of UNIX isolating those apps from others. Or did entirely new architectures. Mainstream IT and INFOSEC ignored these lessons with most of the failures you've seen resulting. They still argue even though one model worked consistently and one they build on didn't. ;) Here's a summary of security kernel approach: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf Unfortunately, the secure UNIX papers are paywalled. Here's another high-assurance project with sections illustrating issues with UNIX API and changes they had to make. That's back when it had dozens of sys calls. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.1667&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.... After a while, the formal verification people got the tools working well enough to prove absence of certain types of problems in code itself rather than an abstract model of it. So, now you see them showing absence of buffer overflows, etc. There's also tools to do similar stuff for assembly and hardware languages. I saw one proof that went down to the gates. Capabilities gradually expanded from system-level properties to lowest-level properties.

jojo3000 10y ago

This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big problem! But lets assume this is solved. Then a API can be checked for certain properties. You can specify what it means that something is read-only in an environment etc. And ensure that it is enforced by the operating system. As example: the verification of seL4 not only guarantees avoidance of classical security holes (buffer overflows etc.) but also certain non-interference properties.

IshKebab 10y ago

> But I think that is not really the big problem we have. It is a really big problem and it needs to be solved. Did you miss this recent news? http://www.theregister.co.uk/2016/10/21/linux_privilege_escalation_hole/ http://www.theregister.co.uk/2016/10/21/linux_privilege_esca...

nickpsecurity 10y ago

Formal verification isn't as limited as you suggest. The original use of formal verification for security in high-assurance security was analysis of security kernels for OS's showing that every state the system could be in was secure or fail-safe. Early attempts like UCLA Secure UNIX showed UNIX was impossible to secure because the API's inherently leaked and/or gave attackers opportunities. That's why high-assurance projects abandoned them in favor of security kernels with user-mode version of UNIX isolating those apps from others. Or did entirely new architectures. Mainstream IT and INFOSEC ignored these lessons with most of the failures you've seen resulting. They still argue even though one model worked consistently and one they build on didn't. ;) Here's a summary of security kernel approach: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf Unfortunately, the secure UNIX papers are paywalled. Here's another high-assurance project with sections illustrating issues with UNIX API and changes they had to make. That's back when it had dozens of sys calls. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.1667&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.... After a while, the formal verification people got the tools working well enough to prove absence of certain types of problems in code itself rather than an abstract model of it. So, now you see them showing absence of buffer overflows, etc. There's also tools to do similar stuff for assembly and hardware languages. I saw one proof that went down to the gates. Capabilities gradually expanded from system-level properties to lowest-level properties.