[schelling42]

>As the foundation for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven secure, with guaranteed confidentiality, integrity, and availability.

>KataOS provides a verifiably-secure platform that protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure.

The wording seems quite confident, maybe it could use some additional "at least according to its specification". This approach doesn't protect against hardware bugs and side-channel attacks.

Especially when one thinks of unexpected attacks like Rowhammer, there is probably no way to include them in a formal systems model beforehand.

[yjftsjthsd-h]

> protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure.

Notice also that they're doing the traditional Google trick of pretending that it respects the user's privacy because it's secure, while ignoring the fact that most of the users privacy will be destroyed by things they designed the operating system to intentionally do in its security model.

[themerone]

I chose Google's mesh routers because I have more trust in their security than any competitor. I would feel pretty safe with PFSense, but my needs are way too simple to bother with that.

I know a lot of techies opt for prosumer, small business gear for their home networks, but most of those vendors have crap security trackrecords. Ubiquiti, seems to be the sole standout in this space, but I don't trust them any more than google to produce secure hardware.

[snotrockets]

Security is not privacy though. If I had a piece of information that could kill, I would trust Google with safeguarding it. What I don't trust them, is not to use information they got. Or rather, I expect them to use it (but safeguard it from others, because that's how they make money: by being the only ones allowed access to private information).

[swozey]

Ubiq has had horrendous security issues

[themerone]

Have you seen Krebs on Security most recent update. He pretty much disavowed his reporting on the Ubiquity breach.

Everybody has security breaches. I'm not out there counting CVEs, but anecdotally, it seems that Netgear, TP-Link, microtik have seem to have much worse reputations.

I don't pay attention to the market for high end networking (Cisco, Juniper).

[swozey]

Ah I had forgotten about the update to that. Last I remembered they were suing him. I only have Ubiq equipment.

[geofft]

It protects the user's privacy against attackers other than Google.

To be fair, this is an entirely reasonable threat model for a lot of people. For instance, if you're a reporter in an authoritarian country, Google is almost certainly not colluding with the attackers who are literally trying to kill you, and using a Chromebook and Gmail is probably the best option out there. Your threat model is "Don't die," not "Don't be subject to surveillance capitalism."

But it's also something we should collectively be pushing back on. The motivating example for these products is "intelligent ambient systems," i.e., things like Nest hubs and doorbells that capture audio/video all the time. These products probably shouldn't exist at all, and to the extent they do, they should process data locally and discard it as soon as they can.

[londons_explore]

Google sucks up a lot of data, and is in a position to do a lot of bad stuff with it, but historically they have never told my spouse about my affair, my government about my accounts in the caymans, or leaked my nude pictures to my grandma. (I don't actually have any of these!)

I really don't care how much data of mine they have while they limit their evil they use it for to deciding if they should show an ad for baseball or football shirts...

And I trust them not to accidentally leak it far more than I trust my government or any smaller/less techy company.

[Mikeb85]

This 100x. Of all the companies/entities that have had some sort of data of mine over the years Google feels by far the most trustworthy.

My country's agencies (Canada) have leaked more data than Google, and MS can claim they're secure all they want, I've had accounts on MS services hacked but never Gmail or Google services...

[tomrod]

There is a tradeoff between hackability and single source of truth.

[petmon]

> historically they have never told my spouse about my affair

Have we forgotten Google Buzz? Google changed GMail to publicly list the people you email most. In one case, this de-anonymized a woman's blog and enabled her abusive ex-husband to stalk her. https://fugitivus.wordpress.com/2010/02/11/fuck-you-google/

This is IMO the most likely way that "bad stuff" will happen: not maliciously, but through privacy-invading misfeatures connected to pushing people to share more.

[londons_explore]

Thats 12 years old... I think it's a real testament to Googles privacy behaviour that amongst their 2 Billon+ users over 11 years, there are no fresher news stories that come to mind.

Compare with facebook/instagram, where it seems every other week someone messes up the privacy settings and posts something to an audience they didn't intend because the product is deliberately designed to encourage accidental oversharing.

[asoberbeck]

> Google sucks up a lot of data, and is in a position to do a lot of bad stuff with it, but historically they have never told my spouse about my affair, my government about my accounts in the caymans, or leaked my nude pictures to my grandma. (I don't actually have any of these!)

You've been lucky, then: https://www.gawker.com/5637234/gcreep-google-engineer-stalke...

"""It's unclear how widespread Barksdale's abuses were, but in at least four cases, Barksdale spied on minors' Google accounts without their consent, according to a source close to the incidents. In an incident this[2010] spring involving a 15-year-old boy who he'd befriended, Barksdale tapped into call logs from Google Voice, Google's Internet phone service, after the boy refused to tell him the name of his new girlfriend, according to our source. After accessing the kid's account to retrieve her name and phone number, Barksdale then taunted the boy and threatened to call her. [...]"""

[esprehn]

Fwiw that was 12 years ago, and a lot of the Google infra has changed quite a bit since then to make looking at user data much harder and track access more explicitly.

[londons_explore]

I really want Google to advertise this...

Ie. I want them to commit to "No human who works at Google will ever see your email or photos without you knowing about it". And then splash that statement all over TV ads.

Set up some system so every time an engineer sees user data, the owner of that data is sent a notification (and there are legit reasons for that, like investigating a bug a user has reported). It doesn't need to be for every kind of user data, just the super sensitive ones like the text of emails.

[pkulak]

But it's still better to not have to trust a giant, multi-national corporation at all.

[geofft]

Absolutely agree, but how do you do that in practice?

Do you self-host your services on some Linux distro? How many FAANG employees have upload access to that distro or maintain its infrastructure?

(Or maybe you audited everything yourself and you're 100% confident in your audit, somehow, and you've turned off automatic updates. How many FAANG employees are working on fuzzers to automatically find new exploitable security vulnerabilities and scale out those fuzzers on their employers' infrastructure?)

[GTP]

This is true now, but once they have those data you can't know what they will use them for in the future. Maybe they will keep using them in the same way as now, maybe not. Also don't forget the recent case of users that got reported to the police by Google because they took pictures of their children for medical reasons.

[amf12]

> This is true now, but once they have those data you can't know what they will use them for in the future.

You can set up auto-deletion of data every 3 months.

[arcanemachiner]

It's actually spelled '"Auto-Deletion" of data' since you can't prove it's been deleted.

Google and other US tech companies have no right to be trusted after PRISM. Not to mention the US government's complete abdication of public oversight under the guise of national security, with secret courts, secret rulings, and national security letters compelling silence from these same organizations while complying with whatever demands they make.

[water-your-self]

Until governments approach them and demand that data or force Google to leave.

[Mikeb85]

Google has refused to cooperate with authoritarian governments and even left China over it. Unlike Apple and MS...

[steelframe]

Apple's "cooperation" with authoritarian governments tends to only go so far as it needs to in order for the next iPhone to come out on time and in sufficient supply. Otherwise Apple bends heaven and earth to engineer their devices to be as secure as they can make them, even against state authorities.

That said, if you live in China, you probably don't want to sync your stuff to iCloud. Not because Apple doesn't want to protect your data, but more because you can't trust anything in any data centers that are physically on Chinese soil.

But let's get real. If you're in mainland China and the authorities decide they need to confiscate your phone, you're already fscked.

[Shugyousha]

AFAIK they have been back in China for a few years again though ...

[gloryjulio]

This. Now iOS is starting to turning to ads business. Apple is officially worse than Google.

[trasz]

Google, being US-based company, is legally obliged to provide all the data they have to three letter agencies, without any real oversight. They can’t refuse even if they wanted.

[webmobdev]

Lol. Selling your data to the government is one of the ways they make money. BigTech and BigBrother have been in cahoots for more than 2-3 decades now. Read https://en.wikipedia.org/wiki/PRISM for more info.

[skybrian]

This is a research project. There are no users and probably won’t be in this form. If it makes it into a real product, it might not even be done by Google (since they’re open sourcing it.)

So nobody is being tricked. It just too early to say what real products will do.

[whoopdedo]

Not to mention protecting the privacy of the applications and operating system from the users themselves.

[rodgerd]

Google's fundamental definition of security and privacy is to expand your privacy to Google, so yes.

[zahllos]

Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

> and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML.

I mean, it does also claim to be "almost entirely written in Rust", which is true if you ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

[jtgans]

TL from the project here: you're right, the changes to the kernel are not yet formally verified, but that's on the roadmap -- there's quite a lot of work that has been done here, and tons more to come. The vast majority of changes we have made have involved lots of conversations with folks on the seL4 mailing list including Gernot Heiser and video conferences to work out the best way to do what we're doing.

I realize the blog post comes out pretty strongly on this topic, and that's my oversight -- I let my aspirations leak out instead of tempering them (this is not your typical PM-driven project) properly.

Please understand that this is an engineer-driven project in Research with a very small team where we're doing our hardest to do the right thing, so please bear with us.

[SkyMarshal]

Don't sweat it, this is just a blip. I for one have wanted an SEL4 + Rust based OS for a long time, really cool that someone is finally doing it. It's clear what the aspiration is, just keep working toward it.

[Veserv]

Okay, then you should fix your mistake and edit the post or issue a new post that does not call or imply that “KataOS provides a verifiably-secure platform” since it does not. You have achieved that when any new readers of the post do not mistakenly believe that it is currently verifiably-secure.

[jtgans]

TL from the project here: yeah, I should have done more work on the wording -- we locked the content too fast, and I pushed a tad too hard at getting the post out. :P

Side-channel attacks are out of scope for the security model of both seL4 and our KataOS project, so bear that in mind for sure.

[ArtWomb]

XMAS comes early as far as I'm concerned... A rust os & risc-v implementation is sorely needed & I expect to begin experimenting on private cloud frankenwulfs immediately. I can see why you rushed, this in my humble opinion is bigger than the release of the go programming lang ;)

[schelling42]

Thank you very much for putting all the effort into this project. It is a great step towards more secure computing in general, and you earned respect for that.

[doublepg23]

“Beware of bugs in the above code; I have only proved it correct, not tried it.” - Knuth.

[Zigurd]

It's either verifiably secure or it isn't, and that makes an enormous difference. Also, the issue of hardware bugs purports to be addressed by verifiably secure CPU designs.

Of course that leaves the multitude of programmable peripheral devices. But starting with hardware and software that are implemented to be provably secure is a big change. It is table stakes for systems to be vastly harder to penetrate.

[jtgans]

Absolutely, and this is specifically why I chose to start with seL4 and use Rust for the userland we built. seL4 has a verification framework already in place, so we can use it to ensure our system design and implementation is good. We've spent this time working with the seL4 guys to find a good middle ground in these changes, and we're going to see about verifying the design as we go, but we wanted to get these things out sooner rather than waiting because it affords more chances for feedback and collaboration. My only regret is not being able to open the entire source tree at once yet. We'll get there, but this is a good start in the meantime.

We do not have our changes formally verified yet, but that is definitely on our roadmap -- otherwise, what's the point of starting from this set of options? Likewise, this is why we chose Rust -- there are several projects already in progress to produce formal verification tools for Rust, so we can hopefully use those as additional proofs.

[Sirened]

are there any formally verified CPUs that support any of the constructs needed for anything more than microcontrollers? Like, I have not yet found a formally verified CPU which supports virtual memory or caching

[RunSet]

Don't trust anything from the world's largest advertising corporation until you hear it from a competing source they don't own or subsidize.

[Genbox]

I've always said that computer science has a PR problem.

Formally verified applications is such a foreign concept to people that when you say "verified correct" they get skeptical and mistrust the whole concept.

Saying something is "secure" when it has been formally verified will be received with a grain of salt, but it is much easier to say than:

"we wrote a detailed specification that define the whole system via algebra, and then we let a theorem prover run all possible permutations of the specification It has now tested a billion edge-cases and we have reached a state where it no longer finds any deviation from the specification."

At least it is provable better than someone saying "it is secure because we think it is".

[riedel]

I do not quite get it: seL4 is verified. Is the rest of the code as well? I understand that verification of Rust is just starting to gain traction (compared to C, Java or Ada), or did they make major progress here?

[29athrowaway]

Or just target the thing with a muon beam.