> 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).
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.
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.
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.
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.
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...
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?)
So now everyone is doing the same thing so called value the 'privacy' (aka only they could collect the data for themselves to do personalized ads). So in the end you pick the one who hoard ur data and show the ads. What's the difference again?
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.
That statement is kind of information-free. If China knows they have Apple completely over the barrel, why wouldn't they demand a lot?
But for how they cooperate, Apple's own transparency report shows they give information on Apple customers to Chinese authorities thousands of times per year, and accept the vast majority of requests: https://www.apple.com/legal/transparency/cn.html
Likewise in Russia: https://www.apple.com/legal/transparency/ru.html
Versus Google which has avoided giving information to or censoring search results in both countries and as a result is mostly banned.
https://www.reuters.com/technology/google-is-fined-390-mln-r...
Google's given up on business there but still puts their sites out there (as they should).
Funny how you specifically mention China, as if it worked differently in USA - the country where you can get four years of jail time for talking back to police.
You can set up auto-deletion of data every 3 months.
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.
1) Tech companies increased their security, but it wasn't enough, and security services still have a feed of nearly all data, through a combination of software/hardware/algorithmic flaws.
2) Tech companies did manage to mostly stem the flow of information into security services. However, security services simply sent secret letters to all the big players demanding an API/backdoor and requiring them not to talk about it.
(or some mix of the two)
If you take security and specifically insider threats seriously, you can't privilege or hide any subsystem, or it becomes a threat of its own, so the same processes that prevent an attacker from creating a shadow-system in your infrastructure also prevent you from doing the same thing.
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. [...]"""
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.
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.
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.
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.
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).
So nobody is being tricked. It just too early to say what real products will do.
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.
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.
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.
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".
>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.