News Clip OS: Neues Betriebssystem direkt von der Sicherheitsbehörde

andy_m4 schrieb:
Formale Verifikation hat weniger mit Checks gemein wie sie z.B. aus Unit-Tests bekannt sind.
Das Verfahren ähnelt mehr einem mathematischen Beweis.
Hab ich auch nicht behauptet. Zufälliger Weise habe ich auf dem Gebiet etwas Erfahrung.

Was dir ein ne formale Verifikation bescheinigen kann ist, das die SW eine Reihe formal spezifizierter Eigenschaften erfüllt. Sie garantiert dir aber nicht, dass du auch alle wichtigen Eigenschaften tatsächlich spezifiziert hast. Anders ausgedrückt: Du kannst nicht fragen "ist die SW korrekt" ohne zu spezifizieren, was korrekt überhaupt bedeutet.

Der Vorteil gegenüber Tests ist halt, dass eine einzelner check sein kann: "Es darf keine Division durch null geben, egal was die Eingangswerte sind", während man bei Tests streng genommen alle möglichen Werte durchprobieren müsste. Aber genauso, wie bei Tests kann ich eben komplett vergessen bestimmte Dinge zu überprüfen (und manches ist aufgrund von skalierungsproblemen auch schlichtweg nicht formal verifizierbar).

Außerdem, was heißt überhaupt "komplett verifiziert"? Was genau würde da verifiziert? Für welche Plattformen? Auf welchem Level (binärcode? Programmcode? Algorithmen?) .
 
  • Gefällt mir
Reaktionen: kullakehx und Teralios
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.
 
Warte mal eine Sekunde, gibts hier echt Leute die Closed Source als Vertrauenswürdiger einstufen als Open Source?

Also heute ist zwar erst Montag 13:00 Uhr, aber so schnell hab ich die Hoffnung ans Forum noch nie verloren.
 
  • Gefällt mir
Reaktionen: Herdware
Herdware schrieb:
Bei wirklich sicherheitsrelevater Software wäre es der allerletzte Strohhalm, darauf zu hoffen, dass die Sicherheitslücken nicht entdeckt werden, nur weil der Quell-Code nicht öffentlich ist.
Wie gesagt: Ich sag ja auch nicht, dass dies zum Standard erhoben werden oder gar als proaktives Mittel für Sicherheitsgewinn benutzt werden soll.
Es ging nur darum zu zeigen, dass nicht alles Gold ist was glänzt.

Herdware schrieb:
darauf zu hoffen, dass die Sicherheitslücken nicht entdeckt werden, nur weil der Quell-Code nicht öffentlich ist.
Nichtsdestotrotz hast Du mit Quelltext aber bessere Chancen Lücken zu finden.
Und weil Du gerade Windows nennst:
WannaCry war eine direkte Folge davon, dass Windows-Sourcen geleakt worden sind.
Kannst Du jetzt natürlich auch wieder als Argument gegen Closed-Source verwenden, weil dann durch den Leak mit einem Schlag alle Windows-Anwender plötzlich mit runtergelassenen Hosen dastanden. :-)
Aber wie gesagt. Darum gehts mir ja nicht.

Herdware schrieb:
Gut. Bei Flash brauchst Du wahrscheinlich nur ein Random-BLOB drauf werfen, um ein Bug zu triggern. :-)

Herdware schrieb:
Deshalb denke ich, dass diese französische Behörde schon den richtigen Weg geht, wenn sie ihr OS als Open Source veröffentlicht. Man gewinnt durch öffentlichen Quell-Code mehr Sicherheit, als man verliert.
Ich weiß nur nicht, ob es der richtige Weg ist. Ohne jetzt die Änderungen speziell zu kennen, wäre es begrüßenswerter wenn diese auf eine beliebige Distribution anwendbar wären. Eine eigene Distribution zu stemmen ist ja relativ aufwendig. Da sollte man sich vielleicht auf etablierte Distributoren stützen, die den Prozess beherrschen.
 
cryoman schrieb:
Ja klar, man schaut sich die Bibliotheken von "Clip OS" gerne in der Mittagspause an ;)
Sagt ja keiner. Es würde Personenjahre dauern, das ist klar.
andy_m4 schrieb:
Einige stellen sich das offenbar einfach vor. Ist ja Open-Source. Jeder (der Ahnung hat) kann reingucken.
teufelernie schrieb:
pffft der Netcode von BSD war auch ein Jahrzehnt komprimitiert und niemand hats bemerkt...
Man hat aber die Möglichkeit reinzuschauen und ist nicht darauf angewiesen mit einer blackbox zu arbeiten.
stevefrogs schrieb:
Ich bin schockiert, dass es hier so viele Träumer gibt, die glauben, dass Open Source Software quasi immun gegenüber Backdoors ist.
Glaubt das wirklich jemand? Jedes hinreichend komplexe Konstrukt hat Fehler und Schwachstellen. Klar kann das jemand ausnutzen und in den Quellcode Hintertüren einbauen. Der Punkt ist doch, dass dieser mit einer geringeren Anstrengung als es bei closed-source-code erforderlich wäre geprüft werden kann.
tmkoeln schrieb:
Und ja es ist auf Github, aber einerseits muss es noch lange nicht so sein das der Github Sourcecode der Sourcecode sein der in den Binaries verwendet wurde und andererseits muss für einen Ssourcecode abgleich jedes Kernel Modul geprüft werden...
Das ist in meinen Augen das eigentliche Problem.

Ergänzung: Wieso gehen denn Leute davon aus dass man die zig Zeigen Code mit einem Schlag auditieren muss und das ganze nicht auch parallel zur Entwicklung passiert? In meiner primitiven Vorstellung läuft es so dass, wenn ein neues Modul angeflanscht wird, sowohl dieses Modul als auch die Schnittstellen zu anderen überprüft werden. Dann folgt der commit und weiter geht's.
 
Zuletzt bearbeitet: (Ergänzung)
  • Gefällt mir
Reaktionen: cryoman
branhalor schrieb:
wahrscheinlich immer noch besser ne Behörde als Google, Apple oder sonst ein Konzern. Daß ne Behörde eingeheimste Daten an den Meistbietenden verhökert, dürfte relativ unwahrscheinlich sein.

Ich kann den Blödsinn nicht mehr hören! Wann haben Alphabeth oder Apple jemals personenbezogene Daten verkauft??
Warum sollte das Google überhaupt machen? Der wahre Reichtum der Firma liegt ja darin diese Daten zu haben und keinem zugänglich zu machen. Beide können sich so einen kurzsichtigen Blödsinn nicht erreichen, den du hier unterstellst.
 
Würde dem OS nicht trauen, wer weiß was für Hintertürchen da eingebaut sind.
 
andy_m4 schrieb:
WannaCry war eine direkte Folge davon, dass Windows-Sourcen geleakt worden sind.
EternalBlue (die von WannaCry verwendete Sicherheitslücke) wurde von der NSA entdeckt und die Informationen über die Sicherheitslücke wurden dann geleakt. Es gibt meines Wissens nach keine Hinweise darauf, dass die Sicherheitslücke im Quellcode von Windows gefunden wurde. Allgemein werden Sicherheitslücken auch bei Open-Source Software mittlerweile eher in den kompilierten Binärdateien mittels Fuzzing gefunden. Es macht hinsichtlich des Findens von Sicherheitslücken daher keinen großen Unterschied, ob man den Quellcode hat oder nicht. Hilfreich ist der Quellcode vor allem für das Beheben einer Sicherheitslücke und das ist ein Vorteil für die Nutzer und ein Nachteil für Angreifer. Daher macht es schon sehr viel Sinn, wenn sicherheitskritische Software Open-Source ist.
 
eSportWarrior schrieb:
Warte mal eine Sekunde, gibts hier echt Leute die Closed Source als Vertrauenswürdiger einstufen als Open Source?
Also ich bin jetzt meinen Kommentar als auch die paar anderen, die sich darauf bezogen haben, durchgegangen und in keinem steht auch nur ansatzweise, dass Closed-Source vertrauenswürdiger ist als OpenSource.

Nur ist eines der Hauptargumente, die ich immer für OpenSource lese, nun mal eben Augenwischerei. Klar hat man bei OpneSource-Software immer die Möglichkeit in den Quelltext hineinzusehen und zu prüfen, was dort gemacht wird, nur wird das eben nicht wirklich gemacht und je nach Projekt ist es - wie ich schrieb - eine Suche nach der Nadel im Heuhaufen.

Oft werden solche Sachen erst genau dann - und da ist es egal ob nun Closed-Source oder OpenSource - gefunden, wenn sich die Programme verdächtig benehmen, erst dann fängt man an hin zuschauen. Und selbst dann ist es einfacher das Programm erst mal zu "installieren" und das machen zu lassen, was es machen soll oder ob es eine Backdoor hat.

Oder verkürzt: OpenSource garantiert eben nicht, dass die Software keine Backdoors hat und sie garantiert auch nicht, dass diese Backdoors wirklich gefunden werden. Und ich bezweifle ernsthaft, dass die meisten hier überhaupt die nötige Kompetenz haben - selbst wenn sie hier so tun - Quelltext wirklich zu lesen und zu verstehen. Ich steige abseits meines Hauptfeldes - Informationssysteme, Datenbanken und CMS-Systeme - auch recht schnell aus und verstehe beim ersten drüber schauen nur einen Bruchteil von dem, was ich im Linux-Kernel und Co manchmal zu sehen bekomme.
 
  • Gefällt mir
Reaktionen: Drainward, cryoman, yummycandy und eine weitere Person
new Account() schrieb:
Mit anderen Worten: Du hast dir die Behauptung aus den Fingern gesaugt, was sie wertlos macht.
Du scheinst ja ein Experte auf dem Gebiet zu sein. Dann erhelle mich doch wie man heutzutage Sicherheitslücken findet. Ich habe dir Belege gegeben, dass auch bei quelloffener Software sehr viele Sicherheitslücken im Binärcode gefunden werden. Du kannst mir gerne einen Beleg geben, wo ein einzelnes Team 1000 Sicherheitslücken innerhalb von fünf Monaten bei der Suche im Quellcode gefunden hat.
 
MC´s schrieb:
Würde dem OS nicht trauen, wer weiß was für Hintertürchen da eingebaut sind.

Im Gegensatz zu geschlossenen Betriebssystemen kann hier jeder nachschauen, was eingebaut wurde. Natürlich muss dass immer noch jemand überhaupt erstmal tun, aber die Chancen dafür dürften recht hoch sein.
 
Weder bin ich Experte auf dem Team, noch habe ich irgendetwas behauptet, was ich belegen müsste.
Ohne Beleg ist deine Argumentation einfach für die Tonne. Und selbst, wenn das meiste nicht durch Quellcodes gefunden wird, macht es trotzdem einen Unterschied ob man den Quellcode hat: Die restlichen Sicherheitslücken werden ja schließlich über jenen gefunden.

Dein geforderter Beleg wäre übrigens nicht notwendig und auch nicht hinreichend um deine Behauptung zu widerlegen: Was sind 1000 Lücken in der Masse an Sicherheitslücken (11000 registrierte letztes Jahr - Dunkelziffer?)? Und wieso muss ein(!) Team diese finden, wenn es auch 1000 Teams könnten? wohlgemerkt nicht jedes Team hat die Kapazitäten und die Technologie von Google...
 
new Account() schrieb:
Ich kann mir nämlich vorstellen, dass gerade bei weniger verbreiteter/beliebter Software es tendenziell sicherer sein kann, dass da kein Sourcecode veröffentlicht wird: Keiner schaut den Code an außer irgendwelche Angreifer.

Das kann ich mir auch vorstellen. Ich hoffe zumindest, dass das der Grund ist, warum die öffentliche Verwaltung uvm. noch nicht auf Linux migriert sind bzw. im Fall von LiMux zurück zu Windows gehen. Wenn es nur die Bequemlickeit der Nutzer wäre, die die Wahl auf Windows fallen lässt, dann wäre das nur von kurzem Erfolg, weil man sich damit ggf.
  • a) in kommerzielle Abhängigkeiten begibt
  • b) der Spionage der Amerikaner auf Quellcode-Ebene aussetzt
  • c) der "Grundlagenforschung" beraubt, mit der die - zugegebenermaßen - größere Zahl an erforderlicher Service-Manpower für selbstgestrickte Linux-Derivate einher gehen würde.
Jedenfalls denke ich, dass ähnlich wie beim Fernsehsender "ARTE" eine Kollaboration von Franzosen und Deutschen in dieser Sache hilfreich wäre angesichts amerikanischer Dominanz in diesem Sektor.
 
new Account() schrieb:
Was sind 1000 Lücken in der Masse an Sicherheitslücken
1000 Lücken in nicht mal einem halben Jahr von einem einzigen Team sind sehr viele, wenn man von 11000 Lücken pro Jahr ausgeht. Das alleine zeigt schon die Effizienz von Fuzzing gegenüber klassischen Methoden. Das Team, über das es in dem Artikel geht, ist auch nicht das einzige, dass Fuzzing einsetzt. Du kannst davon ausgehen, dass noch wesentlich mehr Lücken mit Fuzzing gefunden wurden. Die Leute, die sich mit der Suche nach Sicherheitslücken beschäftigen, können für gewöhnlich auch sehr gut Assembler lesen und sind damit eher weniger auf den Quellcode angewiesen, aber das wirst du mir wahrscheinlich eh nicht glauben.

Wenn du 1000 Teams dran setzt, hast du eben wesentlich höhere kosten, als wenn man Computer daran rechnen lässt. Du willst ja wohl auch keine Belege von mir, dass man Maschinen in der Fertigung einsetzt, weil das gleiche auch von 1000 Menschen gemacht werden könnte. Wie viel Mittel Google hat tut auch nichts zur Sache so lange du nicht weißt, wie viel Mittel Google in Computer für die Suche nach Sicherheitslücken steckt.

Ich verstehe auch ehrlich gesagt nicht, was du versuchst zu erreichen. Wenn du glaubst, dass die meisten Sicherheitslücken im Quellcode gefunden werden, dann liefer doch dafür Belege. Aber scheinbar hast du dafür ja keine, sonst hättest du sie schon lange gebracht. Wenn du mir nicht glauben willst, dann musst du das auch nicht. Das ist nur das was ich mir über die Zeit in dem Bereich angelesen habe und ich im Austausch mit Leuten erfahren habe, die sich intensiver mit dem Thema beschäftigen.
 
kullakehx schrieb:
Du hast die Möglichkeit es zu kontrollieren (lassen).

Spaetestens wenn irgendein Binary Blob geladen wird, kann die Backdoor drin sein.
z.b. beim Microcode Update fuer CPU, Netzwerk oder Grafikkarte.
 
ghecko schrieb:
Jetzt müssen unsere deutschen Behörden das nur noch Forken, etwas anpassen und schon ist Microsoft Windows nicht mehr "alternativlos". War es zwar nie, aber :rolleyes:
...und als erste setzt es bestimmt die Stadt München ein.
 
Zurück
Oben