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

Verifiktion von Software (und Hardware)?

  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: hannob (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. Zum Login

Stellenmarkt
  1. NOVENTI HealthCare GmbH, München
  2. nexnet GmbH, Berlin
  3. Kassenzahnärztliche Vereinigung Baden-Württemberg (KZV BW), Stuttgart
  4. Berliner Stadtreinigungsbetriebe (BSR), Berlin

Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Spiele-Angebote
  1. 0,99€
  2. 4,99€
  3. 4,99€


Haben wir etwas übersehen?

E-Mail an news@golem.de


Definitive Editon angespielt: Das Age of Empires 2 für Könige
Definitive Editon angespielt
Das Age of Empires 2 für Könige

Die 27 Einzelspielerkampagnen sollen für rund 200 Stunden Beschäftigung sorgen, dazu kommen Verbesserungen bei der Grafik und Bedienung sowie eine von Grund auf neu programmierte Gegner- oder Begleit-KI: Die Definitive Edition von Age of Empires 2 ist erhältlich.


    In eigener Sache: Aktiv werden für Golem.de
    In eigener Sache
    Aktiv werden für Golem.de

    Keine Werbung, kein unerwünschtes Tracking - kein Problem! Wer Golem.de-Inhalte pur nutzen möchte, hat neben dem Abo Golem pur jetzt eine weitere Möglichkeit, Golem.de zu unterstützen.

    1. Golem Akademie Von wegen rechtsfreier Raum!
    2. In eigener Sache Wie sich Unternehmen und Behörden für ITler attraktiv machen
    3. In eigener Sache Unser Kubernetes-Workshop kommt auf Touren

    DSGVO: Kommunen verschlüsseln fast nur mit De-Mail
    DSGVO
    Kommunen verschlüsseln fast nur mit De-Mail

    Die Kommunen tun sich weiter schwer mit der Umsetzung der Datenschutz-Grundverordnung. Manche verstehen unter Daten-Verschlüsselung einen abschließbaren Raum für Datenträger.
    Ein Bericht von Christiane Schulzki-Haddouti

    1. Datenschmuggel US-Gericht schränkt Durchsuchungen elektronischer Geräte ein
    2. Digitale Versorgung Viel Kritik an zentraler Sammlung von Patientendaten
    3. Datenschutz Zahl der Behördenzugriffe auf Konten steigt

    1. Apple Music, News+ und Apple TV+: Apple soll Super-Abo planen
      Apple Music, News+ und Apple TV+
      Apple soll Super-Abo planen

      Apple will angeblich ein gebündeltes Abonnement aus Apple Music, Apple News+ und Apple TV+ zum vergünstigten Preis anbieten. Das könnte zu Einbußen bei den Inhaltspartnern führen. Apple hat wohl Probleme, neue Abonnenten für News+ zu gewinnen.

    2. Grounded angespielt: Ameisenarmee statt Rollenspielepos
      Grounded angespielt
      Ameisenarmee statt Rollenspielepos

      Das eigentlich auf klassische Rollenspiele spezialisierte Entwicklerstudio Obsidian Entertainment hat ein ungewöhnliches Survivalgame vorgestellt: In Grounded kämpfen Spieler im Miniformat gegen Ameisen und Marienkäfer.

    3. Project Xcloud: MS-Spielestreaming unterstützt Dualshock 4 und Windows 10
      Project Xcloud
      MS-Spielestreaming unterstützt Dualshock 4 und Windows 10

      Anfang 2020 kommt Project Xcloud, das Spielestreaming von Microsoft, nach Deutschland. Der Dienst wird Windows 10 und das Gamepad der Playstation 4 unterstützen - zumindest vorerst aber nicht den Controller des Konkurrenten Stadia.


    1. 08:02

    2. 07:44

    3. 07:28

    4. 07:12

    5. 07:02

    6. 17:46

    7. 17:10

    8. 16:58