1. Foren
  2. Kommentare
  3. Security
  4. Alle Kommentare zum Artikel
  5. › IMHO: Zertifizierungen sind der…

Verifiktion von Software (und Hardware)?

Am 17. Juli erscheint Ghost of Tsushima; Assassin's Creed Valhalla und Watch Dogs Legions konnten wir auch gerade länger anspielen - Anlass genug, um über Actionspiele, neue Games und die Next-Gen-Konsolen zu sprechen! Unser Chef-Abenteurer Peter Steinlechner stellt sich einer neuen Challenge: euren Fragen.
Er wird sie am 16. Juli von 14 Uhr bis 16 Uhr beantworten.
  1. Thema

Neues Thema Ansicht wechseln


  1. Verifiktion von Software (und Hardware)?

    Autor: Nocta 26.01.15 - 12:39

    Ich habe jetzt schon einige Vorschläge gelesen, dieser hier ist aber zumindest bei diesem Artikel noch nicht aufgekommen.
    Wie wäre es denn, wenn man statt Tests und Audits versucht, mathematisch / logisch zu beweisen, dass die Software und Hardware das tut, was sie tun soll?

    Was bräuchte man dafür? Einerseits eine vollständige mathematische Spezifikation der Software (was soll unter welchen Vorraussetzungen passieren?) und eine Software, die beweisen kann, dass der Quellcode die Spezifikation erfüllt.
    Weiterhin muss natürlich die Spezifikation penibel geprüft werden, was natürlich auch ein Problem ist. Aber nicht so ein großes Problem, wie den Quellcode an sich zu überprüfen.

    Ich weiß leider nicht genau, welche Einschränkungen es gibt und inwiefern einem hier vielleicht ein gödelscher Unvollständigkeitssatz oder Ähnliches in die Quere kommen kann.
    Aber im Prinzip sollte es für die meisten Programme möglich sein, sie automatisch beweisen zu können und hier und da müsste man manuell eine Schleifeninvariante finden und einfügen.



    1 mal bearbeitet, zuletzt am 26.01.15 12:43 durch Nocta.

  2. Re: Verifiktion von Software (und Hardware)?

    Autor: PG 26.01.15 - 13:07

    Nocta schrieb:
    --------------------------------------------------------------------------------
    > Was bräuchte man dafür? Einerseits eine vollständige mathematische
    > Spezifikation der Software (was soll unter welchen Vorraussetzungen
    > passieren?)
    Im Fall von Firmware: Eine vollständige, automatisch prüfbare Spezifikation der Hardware. Es ist schwierig, Firmware formal zu verifizieren, wenn nicht klar ist was "schreibe Wert X in Register Y" für Seiteneffekte hat.

    > und eine Software, die beweisen kann, dass der Quellcode die
    > Spezifikation erfüllt.
    Da gäbe es beispielsweise SPARK (http://www.spark-2014.org/ beschreibt die aktuelle Version)

  3. Re: Verifiktion von Software (und Hardware)?

    Autor: hab (Golem.de) 26.01.15 - 14:00

    Verifikation von Software ist ein spannendes Forschungsfeld. Aber es gibt einige Probleme damit.

    Zunächst mal muss man sich klarmachen dass so etwas extrem aufwändig ist. Im Moment ist das für "normale" Anwendersoftware (und auch Firmware) schlicht aus Kostengründen nicht realistisch.

    Dann gibt es eine Reihe von - ich sag mal - "Realweltproblemen". Man muss bei der formalen Verifikation von Software praktisch immer gewisse Vereinfachungen und Vorannahmen vornehmen. Dazu gehört beispielsweise dass man zumindest mit heutigen Methoden die Sicherheit von Kryptographie nicht beweisen kann. Dazu gehören aber auch Fragen wie die Sicherheit von Seitenkanälen, wo es schlicht um Fragen der Physik geht, die man nicht vollständig in einem Modell abbilden kann.

    Die spannende Frage dabei ist nun: Sind die Vorannahmen realistisch und plausibel oder habe ich am Ende ein System, das unter meinen Annahmen "beweisbar sicher" ist, aber ein Timingangriff ist trotzdem möglich, weil die Laufzeit der Algorithmen nicht Teil meines Modells war? Dann ist die ganze formale Verifikation nutzlos.

    Ein Projekt, was in dieser Richtung arbeitet und was ich sehr spannend finde ist miTLS. Das ist ein Forschungsprojekt, welches versucht, die Sicherheit von TLS zu beweisen und gleichzeitig eine verifizierte Implementierung zu erstellen. Allerdings ist die nicht in erster Linie für den praktischen Einsatz gedacht, sondern im Moment zumindest eher ein reines Forschungsvorhaben.
    Praktische Auswirkungen hat das aber trotzdem: Die Entwickler haben bei der Entwicklung eine ganze Reihe von Problemen sowohl im TLS-Protokoll selbst (u.a. der Triple-Handshake-Angriff) als auch in verschiedenen Implementierungen (u.a. BERserk in nss) entdeckt.

  4. Re: Verifiktion von Software (und Hardware)?

    Autor: derdiedas 26.01.15 - 14:50

    Was Du beschreibst ist ein typisches P-NP-Problem in der Informatik.

    Ist das Problem deterministisch zu Lösen kann man solch eine Software bauen. Ist dies jedoch nicht der Fall muss man alle Möglichkeiten durchkabbeln und das kann beliebig komplex werden.

    Und aktuell sind die Trennung verschiedener Komponenten eines IT Systems nicht perfekt und eindeutig voneinander getrennt, so das eine Inselbetrachtung einer Komponente ohne die Einflüsse anderer Komponenten nicht gewährleistet wird. Etwa ist der Speicher des BIOS sicher oder gibt es Seitenkanäle oder gar Hintertüren (Etwa über den Chipsatz).

    Daher ist das eine Problem die beliebig große Komplexität, das weitere das man nicht an die Information zu allen Beteiligten Komponenten kommt.

    Daher wird wohl eine Landung auf dem Mars einfacher sein, als das was Du möchtest.

    Gruß ddd

  5. Re: Verifiktion von Software (und Hardware)?

    Autor: Nocta 26.01.15 - 17:48

    Danke für die ausführliche Antwort.

    Mir ist klar, dass die formale Verifikation ihre Grenzen hat, insbesondere, wenn es um Probleme geht, die nicht (gut) vom formalen System erfasst werden (Seitenkanalangriffe usw.). Aber wenn man diese anderen Angriffsvektoren auf üblichem Wege versucht zu eleminieren und trotzdem noch verifizieren kann, dass die Software/Hardware der Spezifikation entspricht (und auch kein unspezifiziertes Verhalten aufweist (Backdoor)), dann wäre das doch klasse.
    Wobei man sich natürlich immer noch fragen kann, ob es nicht irgendwo ein Schlupfloch gibt.

    Dass man oft auch zusätzliche Annahmen reinnehmen muss, ist klar. Kryptographie basiert vor allem auf P!=NP, was man nicht beweisen kann. Wobei man das denke ich in der Spezifikation auch umgehen kann, weil es ja nicht darauf ankommt, ob das kryptographische Verfahren sicher ist, sondern, dass es korrekt (=spezifikationsgemäß) implementiert wurde. Die Sicherheit des kryptographischen Verfahrens beweist man lieber anderswo, beziehungsweise, nimmt sie einfach an.

    Mich würde mal interessieren, wie die Komplexität für die gängigen Ansätze ist. Gibt es Ansätze, die zumindest aus theoretischer Sicht die Chance aufweisen, sie in Zukunft für größere, reale Systeme einsetzen zu können? Um wirklich so etwas zu erreichen, wie ich es mir vorstelle?

    Das in Verbindung mit offener / freier Hard- und Software, nachvollziehbaren Buildprozessen und vieles mehr, was hier immer vorgeschlagen wird, wäre schon mal ein enormer Fortschritt. Leider wird es denke ich nicht allzu schnell allzu weit in diese Richtung gehen und selbst dann hätte man vermutlich noch genügend Dinge, über die man sich den Kopf zerbrechen kann. Ich frage mich, ob es jemals möglich sein wird oder überhaupt möglich sein könnte, dass wir von (fast) absoluter Sicherheit reden können. Fast, weil natürlich immer die Chance besteht, Passwörter - oder was auch immer - durch ein glückliches Raten zu "brechen".

  6. Re: Verifiktion von Software (und Hardware)?

    Autor: Nocta 26.01.15 - 18:06

    >Was Du beschreibst ist ein typisches P-NP-Problem in der Informatik.
    >
    > Ist das Problem deterministisch zu Lösen kann man solch eine Software bauen. Ist dies jedoch nicht der Fall muss man alle Möglichkeiten durchkabbeln und das kann beliebig komplex werden.

    Deterministisch lösbar ist es sicher. Du meinst vermutlich, ob es in polynomialzeit von einer deterministischen Turingmaschine lösbar ist. Ich glaube du wirfst die Begriffe ein wenig wild durcheinander, ohne wirklich zu wissen, was du sagst.
    Interessant wäre es für mich, ob es Algorithmen für Software Verification gibt, die in P liegen.
    Was vermutlich das war, was du ausdrücken wolltest.

    > Daher wird wohl eine Landung auf dem Mars einfacher sein, als das was Du möchtest.
    Das ist sicherlich einfacher, weil es schon längst möglich ist. Nicht das beste Beispiel, aber "I get your point"

  1. Thema

Neues Thema Ansicht wechseln


Um zu kommentieren, loggen Sie sich bitte ein oder registrieren Sie sich. Sie müssen ausserdem in Ihrem Account-Profil unter Forum einen Nutzernamen vergeben haben. Zum Login

Stellenmarkt
  1. DAVASO GmbH, Leipzig
  2. Pforzheimer Zeitung, Pforzheim
  3. Bundesamt für Sicherheit in der Informationstechnik, Bonn
  4. Heinz von Heiden GmbH Massivhäuser, Isernhagen

Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Spiele-Angebote
  1. (-91%) 1,20€
  2. 7,99€
  3. (-40%) 23,99€


Haben wir etwas übersehen?

E-Mail an news@golem.de


  1. Ausstieg: Hausakkus für Siemens kein Zukunftsgeschäft
    Ausstieg
    Hausakkus für Siemens kein Zukunftsgeschäft

    Siemens stellt den hauseigenen Strom-Heimspeicher Junelight offiziell ein. Die Solarspeicherakkus scheinen nicht genügend Geld zu bringen.

  2. Trollfabrik: Trump bestätigt Cyberangriff gegen Russland 2018
    Trollfabrik
    Trump bestätigt Cyberangriff gegen Russland 2018

    Der US-Präsent hat erstmals gesagt, dass es 2018 einen Cyberangriff gegen die russische Internet Forschungsagentur gegeben habe, der Einmischung in die US-Politik vorgeworfen wird.

  3. Leak: Macbook Pro mit Apple Silicon könnte Ende 2020 erscheinen
    Leak
    Macbook Pro mit Apple Silicon könnte Ende 2020 erscheinen

    Noch schnell ein Macbook mit Intel-Prozessor kaufen - oder auf Apple Silicon warten? Ein Leak hilft etwas bei den Überlegungen.


  1. 14:11

  2. 13:37

  3. 12:52

  4. 12:18

  5. 11:27

  6. 10:06

  7. 17:20

  8. 15:21