psYcho-edgE schrieb:
Wird schwer Backdoors in Open Source zu verstecken, meinst du nicht?
Klar liegen die Backdoors offen, aber die wenigsten untersuchen wirklich den Quelltext solch komplexer Softwarepakete so intensiv, dass sie entsprechende Lücken im Vorfeld finden.
Meistens werden solche Sachen erst gefunden, wenn man auffälliges Verhalten festgestellt wird und sich ein kundiger Mensch dann auf die Suche danach macht.
Deswegen ist auch eines der Hauptargumente für OpenSource - Sicherheitslücken und Backdoors können besser gefunden werden - eher Augenwischerei. Wie viele Zeilen Quelltext hat Linux? Ein paar Millionen sind es wohl jetzt. Na durchforste die mal nach Backdoors und nach Sicherheitslücken, wenn du keinen Verdacht hast, wo etwas sein könnte: Suche nach der Nadel im Heuhaufen.
Herdware schrieb:
Wenn ich mich richtig erinnere, war damals das Argument für dieses neue OS, dass man es von Grund auf speziell auf Multimedia/Medienbearbeitung und Multi-CPU auslegen wollte, was mit den damaligen Alternativen (DOS/Win3.X, MacOS und diverse Unix) nicht oder nur sehr umständlich (drangefrickelt) möglich war.
Unix ist heute auch mehr ein Marketing-Begriff als wirklich noch ein Betriebssystem. Wenn man sich die Entwicklung ansieht, sind ja gerade Windows NT als auch Mac OS X recht junge Betriebssysteme die ihre Wurzeln Anfang/Mitte der 90er haben.
Entsprechend sind ja beide Betriebssysteme heute nicht mehr monolitisch, sondern nutzen hybrid Kernel, die Vorteile aus beiden Welten vereinen - was in den 90er ja noch notwendig war.
Nur Linux baut auf einem monolitischem Kernel auf und galt bereits von Anfang an als veraltet, was aber auch nicht verwunderlich ist: Es war ein Freizeitprojekt eines Studenten. Klar hat man viele Probleme heute durch Tricks gelöst, aber es ist eben doch an manchen Stellen echt ein "Frickelsystem", aber ein gutes.
Herdware schrieb:
Inzwischen hat sich da aber so viel getan, dass man sich fragen kann, ob ein BeOS-Nachfolger noch irgendwelche Vorteile gegenüber den etablierteren Alternativen haben könnte.
Im Endeffekt wäre ein BeOS-Nachfolger selbst heute nicht mehr State-of-the-Art, ist es ja selbst auch nur ein "Hybrid-Kernel" wie Windows NT und Mac OS und die Überlegungen hinter BeOS sind ja auch die damals zu OS2 führten und Apple dazu bewog mehrfach einen Nachfolger für das alternde MacOS zu schaffen, was ja auch erst fruchtete, als NeXT übernommen wurde.
andy_m4 schrieb:
Wir brauchen endlich mal ein System das secure-by-design ist. Und das sind die etablierten Betriebssysteme alle nicht. Das fängt schon damit an, das viele davon (z.B: Linux) einen monolithischen Kernel haben. Klar versucht man das Problem in den Griff zu kriegen via Kernel-Self-Protection usw. Aber das ist mehr ein herumdoktorn an den Symptomen.
Falsch, viele Betriebsysteme haben heute einen Hybrid-Kernel. MacOS mit Darwin setzt sogar auf einem Mikro-Kernel auf, am Ende ist es aber ein Hybrid-Kernel. Windows NT basiert auch auf einem Hybrid-Kernel.
andy_m4 schrieb:
Man darf nicht vergessen, dass diese Konzepte die heute in Betriebssystemen Anwendung finden halt aus den 70er Jahren stammen. Damals hatte man weder die Mittel/Hardwareressourcen noch das Bewusstsein für Security.
Erneut falsch. Die Konzepte für die heutigen Betriebssysteme sind in den 90er entstanden, als man die "modernen" Konzepte der Mikrokernel umsetzten wollte, man aber recht schnell merkte, dass die Hardware noch nicht schnell genug ist. Microsoft wollte sogar Windows NT mit C++ umsetzten, was aber aus Geschwindigkeitsgründen wieder verworfen wurde.
andy_m4 schrieb:
Und der Vorteil bei verifizierter Software ist halt, dass Du weißt das sie fehlerfrei ist.
Und an dieser Stelle stellt sich mir echt die Frage: Weißt du überhaupt, wovon du redest? Es hat nämlich den Anschein, dass du es nicht hast.
Die formelle Verifizierung (also mathematisch bewiesen) ist sehr schwer und der Aufwand steigt stark an, je komplexer eine Software wird. L4 ist zwar formal verifiziert, aber der Aufwand dafür ist riesig gewesen. 7500 Zeilen Code und 200000 zur Prüfung. Also ca. 30 mal mehr. Einer der Gründe, warum man sich in der Regel nur auf kritische Komponenten bei einem formalen Beweis beschränkt.
Ab gewissen Komplexitäten wiederum ist eine formale Verifizierung nicht möglich. Stichwort: Halteproblem und Gödelscher Unvollständigkeitssatz. (Hui, dass ich die noch in meinen Unterlagen finde. XD). Ein weitere Grund, warum man sich bei der formalen Verifizierung ab gewissen Punkten nur noch auf Teile eines Programmes konzentiert, statt auf das gesamte Programm.
Und selbst DANN kommt es noch drauf an, was man formal denn wirklich verifiziert. Denn auch wenn ein Programm fehlerfrei ist, gilt das erst mal nur für den Quelltext, wenn der Quelltext ... da geht nämlich dann die Sache los mit Compilern, Hardwareunterbau und so weiter und so weiter.
Und selbst wenn dann alle einzelne Bestandteile formal verifiziert sind, bedeutet es noch lange nicht, dass sie es in ihrer Gesamtheit weiterhin sind UND DANN wird es erst recht lustig, denn dann suche mal den Fehler, wenn alle Bestandteile formal verifiziert sind, das gesamte Konstrukt aber nicht mehr.
Und ansonsten, wenn wir von "verifiziert" Software sprechen - mit automatisierten Tests usw: Pustekuchen, dass garantiert dir überhaupt keine Fehlerfreiheit.