Applikationssicherheit beginnt schon bei der Softwareentwicklung

Saubere Wirtschaftlichkeitsanalyse vorbereiten

Dem häufig vorgebrachten Argument, die aufwändige statische Quellcodeanalyse ziehe oftmals erheblichen Mehrkosten nach sich, versuchen die Anbieter dadurch entgegen zu wirken, dass sich bereits durch das Auffinden eines einzigen Bugs die gesamte Investition schon wieder gerechnet habe. Aus Sicht der Unternehmen gilt es jedoch derartige Versprechen kritisch im jeweiligen Kontext zu hinterfragen und die Unterschiede zwischen den Lösungsspezialisten genauer unter die Lupe zu nehmen.

Am Ende entscheidet nämlich in der Regel der Software-Entwickler im Unternehmen selbst über das Wohl und Wehe seiner Kreation. Er liest und wertet möglicherweise gemeinsam mit den Sicherheitsspezialisten im Unternehmen die Berichte über entsprechende Tools aus und entscheidet, ob es sich tatsächlich um brauchbare Defekte und Sicherheitsschwachstellen handelt, denen weiter nachgegangen werden muss.

Anbieter Fortify Software plädiert für eine Art Sicherheitsauditor, der den Code als einwandfrei abhakt bzw. den Code beaufsichtigt. Andererseits gilt das Gebot, die „false positiv rate“ möglichst gering zu halten. Demzufolge verbleibt letztlich die Aufgabe beim Sicherheitsauditor, die „guten“ Elemente aus dem Unbrauchbaren heraus zu filtern.

Somit gilt es aus Anwendersicht, die vollständige Transparenz und Effektivität des jeweils präferierten Lösungsansatzes zu erkennen, gegeneinander abzuwägen und das Nebensächliche vom Wichtigen zu trennen. „Gibt man den Unternehmen also ein Tool zu Hand, auch wenn es über einen Sicherheitsauditor geschieht, bei dem sie sich durch eine Menge Nebensächliches lesen müssen, so werden sie dieses Tool nicht nachhaltig verwenden können“, bilanziert Coverity-Chef Ben Chelf.

Es lande somit meist im Regal und verstaube dort. Deshalb plädiert Coverity für eine Abkehr des Kurses, der Sicherheitsauditor erhalte eine Checkliste oder einen Bericht - und könne somit überprüfen, ob er seine Grundvorgaben erfüllt habe und der ordnungsgemäße Ablauf sichergestellt sei. „Vielmehr geht es darum, dass der Code besser wird“, so der Experte weiter.

Gegenüber anderen Spezialisten aus dem Spektrum der Architekturanalyse setzt Coverity deshalb vor allem auf seine Pfadsimulations-Maschine „Boolean Satisfiability Engine“ (SAT-Engine), mit deren Hilfe sich die falsche Positivrate weiter nach unten drücken und zusätzliche Defekte auf neuartige Weise identifizieren ließen, etwa Pufferüberläufe und Integerüberläufe. „So stellen wir sicher, dass die meisten Punkte, die wir melden, auch tatsächlich relevante Probleme sind“, fasst Ben Chelf zusammen.

Seite 4: Technische Kniffe enttarnen Programmierfehler

weiter...

Technische Kniffe enttarnen Programmierfehler

Ein SAT-Solver ist ein Computerprogramm mit einer Formel mit Variablen, die durch UND, ODER, NICHT verknüpft sind. Der SAT-Solver determiniert, ob sich die einzelnen Variablen so den Werten WAHR oder FALSCH zuordnen lassen, dass das Ergebnis der gesamten Formel den Wert WAHR annimmt und SAT damit erfüllt ist. Verwirklicht wenigstens eine Zuordnung diese Voraussetzung, gibt der SAT-Solver eine spezielle Erfüllbarkeitsanweisung aus. Wenn nicht, kennzeichnet er die Formel als „Nicht erfüllbar“. Außerdem kann er die Richtigkeit seiner Entscheidung demonstrieren.

Voraussetzung für die Anwendung von SAT auf Software ist, dass der Quellcode in einer Form vorliegt, die automatisch an den SAT-Solver übergeben werden kann. Genau hier kommt die Software DNA Map zum Tragen: Sie stellt die erforderliche Information vom Code in jeder gewünschten Form dar. Weil SAT-Solver mit den Operatoren WAHR, FALSCH, UND, ODER und NICHT arbeiten, können die relevanten Teile des Programms in diese Konstrukte umgewandelt werden.

Als Beispiel dient hier die 8-Bit-Variable „char a;“. Um „a“ als WAHR- oder FALSCH-Werte darzustellen ist es hilfreich, sich ihre acht Bits (digitale Nullen und Einsen) als WAHR beziehungsweise FALSCH vorzustellen. Damit wird „a“ zu einem Array aus acht Booleschen Werten:

a_0, a_1, a_2, a_3, a_4, a_5, a_6, a_7

Zusätzlich ist die Übersetzung der Operationen notwendig, die im Programmcode Teil von Ausdrücken sind. Alle Ausdrücke im Code lassen sich in eine äquivalente Formel transformieren, die mit den Operatoren UND, ODER, NICHT arbeitet. Das ist erforderlich, da ein Compiler die Operationen in Maschinencode-Instruktionen umwandeln muss, die ein Prozessor abarbeiten kann. Vereinfacht ausgedrückt schickt der Schaltkreis des Chips nur Nullen und Einsen (niedriges und hohes Spannungspotenzial) durch eine Vielzahl von Gates, die sich wie UND-, ODER-, NICHT-Operatoren verhalten. Daher ist die oben gemachte Zuordnung zulässig. Beispielsweise lässt sich der Ausdruck

a==19

in diese Formel konvertieren:

!a0 ^ !a1 ^ !a2 ^ a3 ^ !a4 ^ !a5 ^ a6 ^ a7

a0 ist hier das höchste Bit von „a“ (high bit), a7 das Niedrigste (low bit). Die Eingabe dieser Formel in einen SAT-Solver würde die folgende Variablenzuordnung ergeben, mit der die Erfüllbarkeit nachgewiesen wäre:

a0 = False (0)a1 = False (0)a2 = False (0)a3 = True (1)a4 = False (0)a5 = False (0)a6 = True (1)a7 = True (1)

Diese achtstellige Binärzahl 00010011 ist äquivalent zu 19.

Nach der Überführung der gesamten Software DNA Map in eine Kombination aus den Booleschen Operatoren WAHR, FALSCH, NICHT, UND, ODER lassen sich zahlreiche Formeln daraus ableiten. SAT-Solver können den Code dann analysieren und zusätzliche, komplexere Qualitäts- und Security-Schwachstellen aufspüren.