Hacker News new | past | comments | ask | show | jobs | submit login

Yes, https://news.ycombinator.com/item?id=39315585

" Why Bloat Is Still Software’s Biggest Vulnerability > A 2024 plea for lean software "

The problem involves so many dependencies that it is impossible for an individual and maybe even megacorporations to fully audit the code base and prove the software behaves as intended. Everything these days is best effort.

We _need_ a native interface that portable software can target, to at LEAST get to the level where 'If you trust the OS, then the rest of the software is known to behave as expected' is a statement that can be made to have a plausibly secure environment for End to End Encryption on anything.

This __has__ to ship, in a DEFAULT install of Windows AND OSX AND mobile computing devices (so iOS and Android too). It absolutely has to be a baseline target, otherwise we'll never get past shipping the browser, again, out of band as yet another thing that must have it's entire monstrosity of libraries updated for every security patch.




> The problem involves so many dependencies that it is impossible for an individual and maybe even megacorporations to fully audit the code base and prove the software behaves as intended. Everything these days is best effort.

Everything has always been best effort, there was no point in time that formally verified software was mainstream. Even attempts at that have turned out broken later on (e.g. KRACK attack on wpa2) so its not a pancea.

> We _need_ a native interface that portable software can target, to at LEAST get to the level where 'If you trust the OS, then the rest of the software is known to behave as expected' is a statement that can be made to have a plausibly secure environment for End to End Encryption on anything.

This doesn't really make sense unless this portable interface contains the entire App. Like how do you imagine such a system would work? What would such an interface do or contain that would bring this dream even remotely close to reality?


> there was no point in time that formally verified software was mainstream. Even attempts at that have turned out broken later on (e.g. KRACK attack on wpa2)

In what ways was wpa2 an attempt at formally verified software? The KRACK attack exploited an issue in the standard itself. Were notable implementations of it formally verified? Was the spec itself verified in some flawed ways? I read the Wikipedia page and couldn't find anything relevant.


See section 6.4 of https://papers.mathyvanhoef.com/ccs2017.pdf

Essentially the spec was formally verified, but it turned out that the formal definition of "secure" they used wasn't sufficient. Formal verification only works if you properly define all the security relavent properties that need to be proven, and the process of defining them can have errors itself.


It shouldn't even be as hard as it appears. If the business logic is designed as a generic library made to be portable to different platforms then you can call into it from a native application built using whatever the native UI toolkits and conventions for that platform are.

Libtorrent is a shining example of this architecture. It runs everywhere, even on mobile platforms. Rust being more popular with makes this even more accessible than it used to be. There's even libraries like PyO3 to make writing bindings to other languages easier.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: