> SeL4 or proof assistant are not panacea. They do not help if assumptions about the task are wrong. And correctly formulating the task in real world is very messy.

Nobody said sel4 was a panacea.

My claim is that doing this kind of computer security is possible. It's just expensive and inconvenient. We know how to make computers a lot more secure than they are today. The limiting factor isn't humanity's knowledge. The limit is that barely anyone wants to pay the bill.

▲

mentalgear 17 hours ago | parent | next [-]

The main issue is that market evolution will always surfaces the most cost-efficient entities within the ecosystem pressures.

That means designing the ecosystem pressures is crucial: things more meaningful than just pure capitalist private-profit logic must by enforced by thoughtful regulation or otherwise the ecosystem converges for private-profit of a small sliver of individuals (billionaires) to the detriment of all other ecosystem members (99% of the world population).

This holds for anything broader than pure private gain, may it be security, social fairness or ecological topics. Sole monetary-value optimization for private gain must be properly constrained or else it results in pure predatory capitalism that implodes society from within, may it be through leaky security, poisoned environments or social unrest.

	▲	lanstin 12 hours ago \| parent [-]
		Yeah this is an interesting argument with respect to why we keep burning carbon. For both software and systems security and rapid climate change, we know the solution. But we haven’t been able to sway the incentives and the system keeps churning out bad results.

▲

alt227 18 hours ago | parent | prev | next [-]

> The limit is that barely anyone wants to pay the bill

Do you even have any experience with how most companies work? SMEs barely have the cashflow to cover their daily expenses, let alone suddenly pay thousands for regular professional security audits and overhauls of their code. This is why security is an afterthought.

▲

josephg 12 hours ago | parent | next [-]

If restaurants can't make sure their food is safe to eat, they shouldn't be allowed to be in business.

If builders can't build houses to code, and the buildings fall down, they shouldn't be allowed to stay in business.

If civil engineers build bridges that fail. Or doctors hurt patients. Or police officers shoot innocent people, they shouldn't keep their jobs.

Software engineers are no different. If you collect my user data and it's at high risk of leaking on the dark web, either clean up your act or close shop.

▲

thephyber 18 hours ago | parent | prev [-]

> This is why security is an afterthought.

Security is always a cost center and rarely a profit center. That's the only thing that needs to be said.

	▲	alt227 17 hours ago \| parent [-]
		Security is defence, it is never a profit center unless your business is providing security services!

▲

tremon 7 hours ago | parent | prev | next [-]

> My claim is that doing this kind of computer security is possible.

But your evidence does not support that claim. SeL4 has proven that it is possible to design a secure microkernel and prove its security guarantees. It does not prove that you can build entire systems (filesystem+database+web server+browser) on top of that kernel while maintaining the same security guarantees.

I'm all for improving the state of computer security, and I'd love for capability systems like SeL4 to become more prevalent. But it's only a microkernel, and it's by no means certain that the PeopleSoft vulnerability exploited here required a kernel-level compromise.

	▲	josephg 2 hours ago \| parent [-]
		I don’t expect every piece of software written to be proven correct like SeL4. But I don’t think we don’t need to do that to get big improvements in the security of a lot of systems. Honestly the biggest insight I take from sel4 is that we can get improvements in security by breaking up a large program into isolated pieces. Give each piece as few permissions as possible, so a compromise of one part doesn’t lead to a whole system compromise. And give them a way to talk. This has big benefits for reliability - since you can fail and restart individual processes. And it has benefits for security, since a system compromise should require an attack of multiple systems simultaneously. And it has benefits for debuggability, since you can add tracing at the comms layer or isolate modules for testing. Wasm does this. Erlang does this. SeL4 does this. Chrome is built this way. The windows driver model is moving this way. And so on. You want a solid core to build around - which is what SeL4 and beam try to be. Then it’s up to us to use those primitives and build good software. Combine that with a memory safe language (rust, go, c#, etc) to protect against buffer overruns and use after frees. And a picture starts to form of how you can build software that is a lot more secure by default. I don’t think perfect security is worth the cost for many companies. But so many security leaks happen because of amateur hour somewhere. Bugs happen - I get that. But a single bug in a C++ program shouldn’t immediately lead to RCE with system level privileges. This stuff isn’t rocket science.

▲

close04 15 hours ago | parent | prev [-]

> just expensive and inconvenient

You mean something is theoretically possible, but in practice only works at small scale and is otherwise effectively impossible. You only have so many resources for all those big topics.

And after you spent all the world's resources on the "perfect", formally bug-free software, you get hacked via social engineering or malicious insider.