4 ms·
SEL4 found the opposite. They could formally verify away run time checks. Algorithmic invariants: Many optimizations rely on certain properties being always tr
by CalChris 7y ago
SEL4 found the opposite. They could formally verify away run time checks.
Algorithmic invariants: Many optimizations rely on certain properties being always true, so specific checks can be left out or can be replaced by other, more efficient checks. A simple example is that the distinguished idle thread is always in thread state idle and therefore can never be blocked or otherwise waiting for I/O. This can be used to remove checks in the code paths that deal with the idle thread.
https://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verification-of-an-operating-system-kernel/fulltext https://cacm.acm.org/magazines/2010/6/92498-sel4-formal-veri...
- tptacek 7y agoDifferent meanings of "slow". I like L4 a lot though. But, I mean, you're generally attacking the things running on top of it.
- CalChris 7y agoI see your point.
- CalChris 7y agoI still see your point but quoting the How Amazon Web Services Uses Formal Methods paper: In each, TLA+ has added significant value, either finding subtle bugs we are sure we would not have found by other means, or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness. Type checking, borrow checking and unit testing are similar albeit weaker tools that allow rapid development by providing a safety net.
- tptacek 7y agoI'm on the "yes type checking" side of the perennial "which is more efficient" programming language debate, but when we talk about "formal methods" in the context of eradicating security vulnerabilities, the subtext is "formally proving correctness", not simply any tool that increases rigor. I agree, boringly, that there are PL tools that apply rigor to increase development speed.
- pron 7y agoThe belief that software could be affordably proven correct was pervasive in the 70s, it led to a research winter, and now formal methods is very much about adding rigor and catching more bugs (some of the most promising directions in contemporary formal methods research revolve around reducing soundness to help find more bugs more quickly). There is a small subdiscipline of formal methods that comes from programming language theory (judging by conferences, it makes up no more than 10-20%) that does still have this 1970s "subtext", but actual researchers or practitioners are usually careful with what they actually say, and you'll most often find such claims explicitly made only by fans.