News KataOS & Sparrow: Googles Betriebssystem ist beweisbar sicher konzipiert

[SVΞN]

Wie Google auf seinem Open Source Blog ankündigt, soll KataOS als beweisbar sicheres Betriebssystem auf Basis des Microkernel seL4 für smarte Geräte und solche aus dem Embedded-Bereich konzipiert worden sein. Das Projekt Sparrow soll die Referenzhardware, KataOS und RISC-V zu einer sicheren Plattform vereinen.

Zur News: KataOS & Sparrow: Googles Betriebssystem ist beweisbar sicher konzipiert

 

[konkretor]

nicht zu verwechseln mit https://katacontainers.io/


Bin mal gespannt wie sich das System entwickelt

 

[BlaBlam]

Nur aus Neugier: was versteht man unter "beweisbar sicher"? Dass es einem Audit unterzogen werden kann?

 

[mojitomay]

Klingt zu gut um Wahr zu sein.
Deshalb steckt der Teufel im Detail.

Ich bin gespannt ob man davon in Zukunft noch was hört.
Und inwiefern man am Ende doch (Hardware-)Backdoors hinein schmuggeln kann...

 

[RAMSoße]

ach ich weiß nicht. Vielleicht kenne ich mich da zu wenig aus, aber rein vom Bauchgefühl ist das doch schizophren.... auf der einen Seite können Sie nicht genug Daten sammeln auf der anderen wollen sie diese jetzt für den User zu "schützen" versuchen.
Auf der anderen Seite, bekommen dann nur sie die Daten....

 

[Peppi]

Bin mal gespannt wie sich das System entwickelt

Vermutlich in die falsche Richtung. Google ist eine der größten Datenkraken dieser Erde und spricht gleichzeitig von:

Wenn Geräten um uns herum nicht mathematisch nachgewiesen werden kann, dass sie die Daten sicher aufbewahren können, können die von ihnen gesammelten personenbezogenen Daten, wie Bilder von Personen und Aufzeichnungen ihrer Stimmen, für bösartige Software möglicherweise zugänglich sein.
Google

Ich denke das unsere Daten eher vor Google selbst geschützt werden sollten.

Peppi

 

[Bart1]

Joa, sowas von Google hinterlässt mehr als nur einen faden Beigeschmack.

 

[andi_sco]

Treppenwitz der Geschichte

Irgendwie kann ich es Google nicht glauben, dass die Daten hier sicherer sind

 

[SVΞN]

as versteht man unter "beweisbar sicher"? Dass es einem Audit unterzogen werden kann?

Dies bedeutet unter anderem, dass der Kernel nachweislich keinen der bisher verbreiteten Entwurfsfehler, wie beispielsweise Speicherüberläufe (Buffer Overflows), Zeigerfehler und Speicherlecks, enthält.

Im Jahr 2009 wurde am Forschungsinstitut NICTA in Zusammenarbeit mit der UNSW mit seL4 erstmals ein für allgemeine Anwendungen tauglicher Kernel formal verifiziert, d. h., es wurde mathematisch bewiesen, dass die Implementierung die Spezifikation des Kernels erfüllt und somit funktional korrekt ist.

Was Google auf Basis von KataOS daraus macht, steht natürlich noch auf einem ganz anderen Blatt.

Lobenswert ist allerdings, dass sowohöl KataOS als auch die Hardware-Plattform Sparrow mit RISC-V komplett Open Source sein und von jedem eingesehen werden können.

Irgendwie kann ich es Google nicht glauben, dass die Daten hier sicherer sind

Das kann ja dann von jedem eingesehen und überprüft werden.

 

[plami]

Nur aus Neugier: was versteht man unter "beweisbar sicher"? Dass es einem Audit unterzogen werden kann?

Beweisbar sicher heißt, dass es mathematische Beweise dafür gibt, dass der Quellcode und/oder der erzeugte Maschinencode gewisse Anforderungen erfüllt. Das bezieht sich hier wohl vor allem auf den Mikrokernel seL4, der genau dafür bekannt ist.

ach ich weiß nicht. Vielleicht kenne ich mich da zu wenig aus, aber rein vom Bauchgefühl ist das doch schizophren.... auf der einen Seite können Sie nicht genug Daten sammeln auf der anderen wollen sie diese jetzt für den User zu "schützen" versuchen.
Auf der anderen Seite, bekommen dann nur sie die Daten....

Google will, dass wir möglichst viele Daten von uns preisgeben. Das tun wir aber nur, wenn wir Google genügend vertrauen. Also hat Google natürlich ein Interesse daran, dass mit den Daten nur genau das passiert, was Google möchte, weshalb die technische Plattform möglichst sicher sein soll (vor Angreifern aus dem Internet, aber auch aus dem eigenen Unternehmen).

 

[TiKu]

Nur aus Neugier: was versteht man unter "beweisbar sicher"? Dass es einem Audit unterzogen werden kann?

Nein, eigentlich sollte das heißen, dass mathematisch beweisbar ist, dass das System sicher ist. Ich frage mich allerdings, ob das auch für bisher unbekannte Angriffsvektoren gilt.

 

[Gnarfoz]

Da hat bei Rust aber jemand safe mit secure verwechselt.
Rust ist doch primär darauf ausgelegt, klassische Fehler beim Speichermanagement unmöglich zu machen. Das ist "safety", nicht "security".
Ich bin mir sicher (😉) , dass man auch mit Rust dumme Programme schreiben kann, die mit Nutzerdaten nicht sorgfältig umgehen.

 

[KitKat::new()]

Das ist "safety", nicht "security".

Inwiefern?

Angesichts dessen, dass der Großteil der Sicherheitslücken durch Speicherfehler kommt, hilft es der Security enorm.
Bei safety helfen natürlich weniger Bugs ebenso.

(Und weder das eine noch das andere kann man alleine durch Speichersicherheit garantieren)

PS: Eine weitere Eigenschaft von Rust ist, dass es auch die Freiheit von Data Races bietet.

 

[Joshinator]

Rust ist doch primär darauf ausgelegt, klassische Fehler beim Speichermanagement unmöglich zu machen

Die Google Programmierer:

fn main() {
    unsafe {
        // muss alles unsafe sein, sonst meckert der compiler
    }
}

 

[andi_sco]

Das kann ja dann von jedem eingesehen und überprüft werden.

Schauen wir mal

PS du hast die 100.000 Likes bald voll - gibt es da ein Jubiläums Special?

 

[Hito360]

sicher fuer wen? Nutzer oder Datensammler? xD
bisher hat Google ausser Android fast jedes "Projekt" fallen lassen, wenns kein Geld bringt. Siicheres OS klingt schoen, wurde aber mit bestimmtem GeldverdienerZweck gebaut, nicht aus Wohlwollen der Menschheit

 

[madmax2010]

Irgendwie kann ich es Google nicht glauben, dass die Daten hier sicherer sind

Um die Daten geht es hier nur in zweiter Linie.


Für die, die das thema interessiert: Der deutsche Wikipediaartikel dazu ist überraschend gut: https://de.wikipedia.org/wiki/Beweisbare_Sicherheit
Mmn. Besser als der englische.

Falls jemand sehen will wie sowas aussieht:
https://eprint.iacr.org/2020/756.pdf
Hier findet sich das ganze Auf Protokoll / Anwendungsebene am Beispiel FIDO2

Siicheres OS klingt schoen, wurde aber mit bestimmtem GeldverdienerZweck gebaut, nicht aus Wohlwollen der Menschheit

Klar zum Geld verdienen.
Es geht hier eher darum, dass man aus jedem Zustand des Systems, alle möglichen Folgezustände ableiten kann und einen Beweis erbringen kann, dass es keine Weiteren zustände, die nicht absehbar sind, möglich wären.
Und das halt für alle Zustände 1-n
Schau dir die Beweisführung für FIDO an.
Natürlich geht man da nich für jeden Atomaren zustand einzeln dran, sondern sucht Mathematische abkürzungen, dere n Vollständigkeit an anderer Stelle schon bewiesen wurde

 

[DFFVB]

So wie ich das verstehe: Wir sammeln eure Daten, ihr habt aber Bedenken. Hey wir erzählen euch, dass wir das mega sicher machen, also noch sicherer als früher. Kriegen wir sie jetzt?

 

[Termy]

Irgendwie kann ich es Google nicht glauben, dass die Daten hier sicherer sind

Naja, es ist halt wie mit unserer Regierung: Wenn Google sich fuer 'die Guten' haelt, dann kann es schon sein, dass die Daten sicher sind

Ich bin bei Google ja auch immer hin- und hergerissen. Auf der einen Seite leisten sie so viel gutes, grade im Bereich Open Source, auf der anderen Seite wurde 'don't be evil' gestrichen und es wird mit knallharten Bandagen Wettbewerb sabotiert und Profit maximiert...

 

[ShadowDragon]

Dies bedeutet unter anderem, dass der Kernel nachweislich keinen der bisher verbreiteten Entwurfsfehler, wie beispielsweise Speicherüberläufe (Buffer Overflows), Zeigerfehler und Speicherlecks, enthält.

Interessant zu erwähnen ist vlt. noch, dass es nur bei Mikrokernels möglich ist, diesen formal zu überprüfen. Bei dem Linux Kernel oder dem Windows Kernel mit Millionen Zeilen Code ist dies eher schwierig, vor allem in angemessener Zeit.