4 ms·
The article is light on details, but based on the way they talked about it ("impossible to hack in principle") it's likely that they actually can _prove_ that i
by mmalone 10y ago
The article is light on details, but based on the way they talked about it ("impossible to hack in principle") it's likely that they actually can _prove_ that it's more secure than a Linux distro dedicated to security insofar as they're able to prove anything at all. Since the Linux APIs are not formally specified, or verified, it's essentially impossible to _prove_ anything at all (again, in a formal sense). Formal verification can get esoteric quickly, but the state of the art is very impressive (see CompCert, seL4, Agda, Idris).
As someone who has been paying attention to this space for some time I welcome anything new that increases exposure. It's cool stuff, and it's probably the future. However, there's a long way to go. Security doesn't stop at the operating system. In fact, the vast majority of security breaches occur due to misconfiguration, bugs, or good old fashioned social engineering. To really build a system that's "secure in principle" you can't stop at the operating system: you need to build a toolchain that makes it easy to build user space applications that are also "secure in principal" and you need to work on the HCI so the security model makes sense / isn't defeated by users. That's going to be a lot of work!
- btown 10y agoThere's a difference between "we show you the proof, and you trust us as a service provider that the assumptions are correct" - namely that non-OSS software is loaded in the form it is shown in the proof - and "we show you the proof, and give you all information needed to audit it." Some people will buy based on only the first statement and the brand of the company. Now, we're looking at a top-notch team of OS programmers; presumably, they all have access to do that audit themselves, and at least some of them must be ethical and proficient enough to notice and refuse to ship a backdoor, right? But the influence of a state actor given 14 years to compromise a team shouldn't be dismissed out of hand. https://en.wikipedia.org/wiki/Kaspersky_Lab#Controversy https://en.wikipedia.org/wiki/Kaspersky_Lab#Controversy
- jodrellblank 10y agoNow, we're looking at a top-notch team of OS programmers Kaspersky AV hobbles my core i7 to the point where it can't even respond to keypresses. I have no view on its anti-virus abilities, but my every experience of it (the client and the management tools) is that it's shoddy enterprise churnware. And, of course, they also promote it as if it's the best thing ever. I guess the OS team could be the best ever. But my starting position is "ha ha, as if".
- kbenson 10y ago> Since the Linux APIs are not formally specified, or verified That said, they are apparently stable enough to emulate enough of Linux that from another OS that you can simulate a Linux OS as a container and run software as if it's on Linux.[1] So, to my mind that implies that while they may not be formally specified, it's not too hard to look at what's actually implemented and treat that as a sort of loose spec. 1: http://www.slideshare.net/bcantrill/illumos-lx http://www.slideshare.net/bcantrill/illumos-lx
- nickpsecurity 10y agoA formal spec would be great but you're right. Plenty of people have done working layers of Linux in user-mode, etc. The only thing I know with formal specifications was filesystem API's for testing them. There have also been selective ones for things like robust drivers. Personally, I'd love to see one just to document all the state and covert channels. Especially visually. I bet it would be one, big-ass, messy graph. :)