Es wird dadurch kein einziges IoT-Projekt sicher

[ultim]

Das OS (Kata OS) wird dadurch beweisbar keine Speicherfehler haben. Solche Fehler repräsentieren allerdings nur 40-60% von potenziellen Sicherheitslücken und einen noch kleineren Anteil von praktischen Lücken. Meistens werden IoT-Projekte nicht über Pufferüberläufe gehackt, öfters geht es um ungewollte Enthüllung von Informationen, fehlerhafte oder fehlende Berechtigungsprüfungen, unsicheres Firmwareupgrade, algorithmische Schwachstellen etc.

Womit die Bezeichnung "beweisbar Sicher" absolut irreführend und praktisch nur ein Marketing-Gag ist. Sicherer, ja. Beweisbar sicher, lächerlich.

[Blindie]

Das sollte doch klar sein, das sicherste system bringt nichts wenn die Lücke beim Anwender liegt.

[ultim]

Schon. man kann aber das nicht ignorieren wenn das so ein wesentliches Teil der Gesamtlösung ist. Unter dem "Anwender" wird hier natürlich nicht der Endbenutzer verstanden, sondern die Entwickler, die mit dem OS dann Projekte umsetzen sollen. Einerseits ist seL4 nur ein Microkernel, d.h. da sind nicht einmal Funktionen enthalten, die eigentlich oft Teil eines Kernel sind, und damit gibt es für diese Funktionen, die dann von "Anwendern" nachprogrammiert werden, vom Start keine Sicherheitsbeweise. Andererseits gilt die "mathematisch beweisbar"-Eigenschaft für seL4 auch nur unter gewissen Annahmen, zB. wie eine fehler- und lückenlose mathematische Spezifikation, wo 99% aller Projekte gleich ihre erste Fehler machen. Über andere Sachen, wie zB. über Speichermanipulation/Korruption über DMA durch Treiber (die ebenfalls nicht im Beweismodell enthalten sind) ist es sogar unmöglich mathematisch zu argumentieren. Und dann gibt es natürlich noch die ganze Applikationslogik.

Also, klar. Der Fehler wird vielleicht in Treibern oder im Applikationskod liegen (und somit in *beiden* Fällen ausserhalb von seL4/KataOS), aber nur, weil man deklariert "das ist nicht unser Kod", werden die Fehler noch nicht vermieden. Ich finde von einem "beweisbar sicheren" Platform zu reden ist grob irreführend, denn auch wenn das unter glücklichen Umständen isoliert gesehen für den Microkernel selbst sogar gilt, das heisst relativ wenig für ein Gesamtprojekt. Man soll nicht den Eindruck vermittelt, dass ein Projekt wesentlich sicherer werden würde nur weil der Microkernel darunter sicherer ist.



2 mal bearbeitet, zuletzt am 17.10.22 12:49 durch ultim.

[486dx4-160]

ultim schrieb:
--------------------------------------------------------------------------------
> Das OS (Kata OS) wird dadurch beweisbar keine Speicherfehler haben. Solche
> Fehler repräsentieren allerdings nur 40-60% von potenziellen
> Sicherheitslücken und einen noch kleineren Anteil von praktischen Lücken.
> Meistens werden IoT-Projekte nicht über Pufferüberläufe gehackt, öfters
> geht es um ungewollte Enthüllung von Informationen, fehlerhafte oder
> fehlende Berechtigungsprüfungen, unsicheres Firmwareupgrade, algorithmische
> Schwachstellen etc.
>
> Womit die Bezeichnung "beweisbar Sicher" absolut irreführend und praktisch
> nur ein Marketing-Gag ist. Sicherer, ja. Beweisbar sicher, lächerlich.

Naja, zumindest ist die PR-Abteilung von Google in einem Punkt ehrlich:
"Wenn den Geräten um uns herum nicht mathematisch nachgewiesen werden kann, dass sie Daten sicher aufbewahren, könnten die von ihnen gesammelten personenbezogenen Daten - wie Bilder von Personen und Aufzeichnungen ihrer Stimmen - für bösartige Software zugänglich sein."

Es geht um den Schutz der gesammelten personenbezogenen Daten, die _bei Google_ auf irgendwelchen Geräten gespeichert sind.
Endkundengeräte müssen personenbezogene Daten, Bilder und Stimmaufzeichnungen selbstverständlich weiterhin zugänglich machen, sonst wäre die Bude bald pleite.

[Urbautz]

Vor allem muss der Angreifer dafür schon im IoT-Netz sein - und damit kann man jede geräteinterne Sicherheit in der Pfeife rauchen.
Solange das Netz "unkontrolliert" von außen erreichbar ist - also nicht durch mindestens ein VLAN vom eigentlichen Internet getrennt, bringt das gar nix.

[ultim]

Urbautz schrieb:
--------------------------------------------------------------------------------
> Vor allem muss der Angreifer dafür schon im IoT-Netz sein - und damit kann
> man jede geräteinterne Sicherheit in der Pfeife rauchen.
> Solange das Netz "unkontrolliert" von außen erreichbar ist - also nicht
> durch mindestens ein VLAN vom eigentlichen Internet getrennt, bringt das
> gar nix.

Na ja, das kann man normalerweise mit Verschlüsselung und Authentifizierung auch lösen. Wenn man davon ausgehen könnte dass diese fehlerfrei umgesetzt und die Geräte auch sonst sicher sind dann wären Maßnahmen wie VLANs sogar unnötig.



1 mal bearbeitet, zuletzt am 17.10.22 13:20 durch ultim.

[Thargon]

Geht es bei Kata OS denn überhaupt um Sicherheit im Sinne von Security oder nicht doch um Safety? Das sind zwei völlig verschiedene Dinge, auch wenn man das im Deutschen nicht gut voneinander unterscheiden kann.

So wie ich den Artikel interpretiere, ist Kata OS insofern beweisbar sicher (safe), da das System beweisbar niemals in eine Situation undefinierten Verhaltens kommen wird. Wenn natürlich die Verhaltensdefinition lückenhaft oder sonstwie unsicher ist (mangelnde security), dann können auch mit Kata OS böse Dinge passieren.

[jsonn]

Neben dem Auslagern von Treibern aus dem Kernel wird doch insbesondere das Verhalten der CPU als Teil des Models als korrekt vorausgesetzt. Wie gefährlich das ist, haben doch Meltdown und Spectre gezeigt.

[nubar]

Du vergisst oder verdrehst dabei aber den eigentlichen Punkt. Niemand konnte bisher beweisbar sichere Anwendungen bauen, die auf einem OS laufen, weil das nämlich ein bewiesen sicheres OS vorausgesetzt hätte. Darum hat das auch niemand probiert. Es war ein aussichtsloses Unterfangen. Das hieß auch, dass man mit jedem Schrott Geld verdienen konnte und niemand ein Interesse an sicheren Anwendungen hatte. Sie sollten nur nicht die beschissendsten am Markt sein. Und sogar das vergessen die "Kunden" nach ein paar Wochen... und benutzen den Krempel munter weiter, solange es sie nicht selbst erwischt hat.

Insofern ist das hier ein echter Fortschritt.

[kayozz]

ultim schrieb:
--------------------------------------------------------------------------------
> Das OS (Kata OS) wird dadurch beweisbar keine Speicherfehler haben. Solche
> Fehler repräsentieren allerdings nur 40-60% von potenziellen
> Sicherheitslücken und einen noch kleineren Anteil von praktischen Lücken.

Durch Pufferüberläufe sind schon Raketen abgestürzt (z.B. Ariane 5, man hat den Code der Ariane 4 genommen, aber nicht die Höhere Endgeschwindigkeit bedacht). Ein "sicheres" System verhindert nicht, dass man der Rakete einen falschen Winkel einprogrammiert und die zur Erde stürzt, aber trotzdem hätte man den Fehler effektiv unterbunden, da das bereits ein Compile Time Fehler gewesen wäre.

Im übrigen sind Speicherfehler im Gegensatz zu logischen Fehlern beim Review schwerer zu entdecken und können bei Ausnutzung durch präparierte Eingabedaten oftmals sehr mächtig sein.

Eine "einfache" Sicherheitslücke, bei der ich z.B. durch präparierte URLs Kundendaten abgreifen kann, erlaubt z.B. keine Rechteausweitung, wie es mit vielen Speicherfehlern der Fall wäre.

[winterkoenig]

jsonn schrieb:
--------------------------------------------------------------------------------
> Neben dem Auslagern von Treibern aus dem Kernel wird doch insbesondere das
> Verhalten der CPU als Teil des Models als korrekt vorausgesetzt. Wie
> gefährlich das ist, haben doch Meltdown und Spectre gezeigt.

Dazu steht ja was im letzten Absatz des Artikels.

[WasntMe]

ultim schrieb:
--------------------------------------------------------------------------------
> Womit die Bezeichnung "beweisbar Sicher" absolut irreführend und praktisch
> nur ein Marketing-Gag ist. Sicherer, ja. Beweisbar sicher, lächerlich.

Für den Microkernel seL4, auf dem Kata OS basiert, wurde das vor mehr als 10 Jahren formal bewiesen (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf). Du kannst davon ausgehen, dass das ein wenig mehr als ein Marketing-Gag ist.

"Beweisbar sicher" heißt in dem Zusammenhang, dass formal nachgewiesen wurde, dass der Microkernel sich gemäß den Spezifikationen verhält und keine Implementierungsfehler, wie uninitialisierte Variablen, Pufferüberläufe, Deadlocks, ... enthält. Ein darauf basierendes Gesamtsystem ist natürlich nur dann beweisbar sicher, wenn jede darauf laufende Komponente ebenfalls diesen Nachweis bringt. Aber genau das wurde ja auch im Artikel geschrieben.



2 mal bearbeitet, zuletzt am 17.10.22 15:09 durch WasntMe.

[FeuerTeuer1]

WasntMe schrieb:
--------------------------------------------------------------------------------
> ultim schrieb:
> ---------------------------------------------------------------------------
> -----
> > Womit die Bezeichnung "beweisbar Sicher" absolut irreführend und
> praktisch
> > nur ein Marketing-Gag ist. Sicherer, ja. Beweisbar sicher, lächerlich.
>
> Für den Microkernel seL4, auf dem Kata OS basiert, wurde das vor mehr als
> 10 Jahren formal bewiesen (www.sigops.org Du kannst davon ausgehen, dass
> das ein wenig mehr als ein Marketing-Gag ist.
>
> "Beweisbar sicher" heißt in dem Zusammenhang, dass formal nachgewiesen
> wurde, dass der Microkernel sich gemäß den Spezifikationen verhält und
> keine Implementierungsfehler, wie uninitialisierte Variablen,
> Pufferüberläufe, Deadlocks, ... enthält. Ein darauf basierendes
> Gesamtsystem ist natürlich nur dann beweisbar sicher, wenn jede darauf
> laufende Komponente ebenfalls diesen Nachweis bringt. Aber genau das wurde
> ja auch im Artikel geschrieben.

der Ultim hat null Plan, wovon er redet, da helfen auch Deine Erklärungen nicht. Der Techsplained allen das Feld, als hätte er IT Security erfunden, dabei aber noch nie im echten Security-Umfeld gearbeitet. Ich frage mich immer, was Leute reitet, sich so weit aus dem Fenster zu hängen, wenn man wirklich überhaupt keine Ahnung hat.

Finde aber die Hintergründe zu den Aktivititäten spannend. Gibt ja ein paar Firmen aus dem Umfeld Dresden, die seit mehr als 10 Jahren in all möglichen Domänen in Deutschland versuchen, das zu etablieren. Hätte auch eine große Nummer in deutschen Autos werden können, hab das aber dann nicht weiter mitbekommen.

[m1-ultras]

ultim schrieb:
--------------------------------------------------------------------------------

> Womit die Bezeichnung "beweisbar Sicher" absolut irreführend und praktisch
> nur ein Marketing-Gag ist. Sicherer, ja. Beweisbar sicher, lächerlich.

Nein. Jeder mit etwas Ahnung weiß, das bei solcher, mit Theorembeweisern als sicher bewiesener Software, der Beweis nur bezüglich einer gegebenen Spezifikation gilt. Diese Spezifikation ist so gut wie nie allumfassend und in manchen Fällen sogar selbst falsch.

Im Extremfall hast Du die Bugs nur von der Software in die Spezifikation verschoben, was aber auch schon hilfreich ist, weil man die Spec leichter prüfen kann.

[ultim]

Dass es eine Beweisbarkeit nur in Relation zu einer formalen Spezifikation geben kann war hier schon immer klar. Im Thread habe ich darauf wohl als erstes selbst hingewiesen, hätte man das zweite Beitrag oben von mir gelesen (samt 2. Absatz wo ich etwas ausführlicher erkläre warum mMn. das Marketing von KataOS irreführend ist).

Thargon hat richtig darauf hingewiesen, dass es potenziell auch um eine Verwirrung zwischen Safety und Security gehen könnte. Entsprechend bauen fast alle Beiträge danach auf die Nützlichkeit von formalen Verifikation der Funktion auf. Nur anscheinend hat es fast keiner gecheckt worum es bei KataOS geht.

Verwirrend ist es, weil es zumindest bei seL4 noch tatsächlich um die funktionale Sicherheit (safety) geht. Allerdings hat KataOS hierzu nichts beigetragen hat. seL4 existiert seit vielen-vielen Jahren (wurde ja noch im letzten Millenium gestartet), und war auch schon ohne KataOS, ohne Rust und ohne Google beweisbar funktional sicher. Dann kommt Google, fügt Teile von einem Betriebssystem in Rust hinzu, schreibt Rust-Schnittstellen für die existierende C-Routinen, und deklariert das Plattform als Beweisbar *Secure*. Dass es hier um "Secure" und nicht um "Safe" geht, ist u.a. auch von der offiziellen Ankündigung sichtbar (siehe: https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html).
Der Fehler: Die neuen Rust-Teile sind aber nicht mehr von der Beweisbarkeit erfasst.

Und daher mein Kritik an das falsche "Marketing". KataOS wirbt durch die Kombination von seL4 und Rust mit Security und mit ihrer Beweisbarkeit, wobei so wie es ausschaut aktuell keiner von diesen zutrifft. Beweisbar ist das Projekt nicht sondern nur die seL4-Teile davon, und Secure ist das Projekt auch nicht, weil im Code ausserhalb von seL4 die reine Abwesenheit von Speicherverwaltungsfehlern für Security noch lange nicht ausreicht.
(Die Hypothese, dass die überwiegende Mehrheit von Sicherheitslückjen eh im Applikationscode stecken wird, kommt auch noch dazu wie früher erwähnt, ist aber fast nebensächlich).


Unwichtiges p.s.
Eine Gratulation geht an FeuerTeuer1, der als einziger Kommenter weder argumentiert noch auf potenzielle Fehler hingewiesen hat, sondern grundlos gleich mit einer persönlichen Beleidigung losgegangen ist, ohne irgendeine Diskussion vorher. Wobei gerade er nicht verstanden hat, worum es bei KataOS geht. Ein unwichtiger aber schöner Twist ist, dass eben er nicht verstanden hat worum es bei KataOS geht.



2 mal bearbeitet, zuletzt am 18.10.22 02:57 durch ultim.

[t_e_e_k]

486dx4-160 schrieb:
--------------------------------------------------------------------------------.
> Endkundengeräte müssen personenbezogene Daten, Bilder und
> Stimmaufzeichnungen selbstverständlich weiterhin zugänglich machen, sonst
> wäre die Bude bald pleite.

Das ist schon lange nicht mehr deren Modell. Die Verlagerung auf lokale Geräte ist aktuell deren Ding. Pixel phones verarbeiten immer mehr lokal (Assistent ist Lokal, Bildbearbeitung Lokal, Musikerkennung Lokal, ...), mit Matter/Thread werden die Routinen deiner Heimautomatisierung Lokal ausgeführt.

Der Trend geht weg vom großen Rechenzentrum hin zu den iot, die Zuhause laufen: Nest (Thermostat, Kamera, Türschloss, Rauchmelder, ...), Intelligente speaker, WLAN Router, ...)

[Kein Kostverächter]

Nein, dadurch alleine wird kein ganzes Projekt sicher. Wenn der Rest ein Holzschuppen ist, bringt die beste Tresortüre nichts.
Wenn man allerdings ernsthaft eine sicheres Produkt anstrebt, ist es doch hilfreich, dass es zumindest schon mal eine Komponente (den OS-Kernel) gibt, der richtig eingesetzt beweisbar sicher ist. Denn andere Kernel müsste man auditieren oder sich auf die Audits anderer verlassen, und bei einem Audit kann immer etwas übersehen werden. Die Tatsache, dass es mathematisch beweisbar ist, dass eine Kernkomponente keine Speicherfehler (und nebenbei bemerkt auch keine Nebenläufigkeitsfehler, was noch beindruckender ist) hat, ist da schon viel wert.
Das man mit Social Engineering trotzdem immer noch unbefugt irgendwo eindringen kann, ist eine Binsenweisheit, das galt auch schon für alte Burgen und Festungen.

Bis die Tage,

KK

----------------------------------------------------------
Mach dir deine eigenen Götter, und unterlasse es, dich mit einer schnöden Religion zu beflecken.
(Epikur, griech. Phil., 341-270 v.Chr.)
----------------------------------------------------------
We provide AI Blockchain Cloud (ABC) enabled applications bringing Enterprise level synergies to vertically integrated business processes.