Analyse von C-Programmen bezüglich Secure Coding mittels LTL-Modelchecking

Die Verwendung von Secure Coding Richtlinien hilft Softwareentwicklern 
unsichere Programmierpraktiken durch sichere Alternativen zu ersetzen. 
Dabei ist es in der Praxis schwierig die Einhaltung dieser Richtlinien 
sicherzustellen. Aus diesem Grund wurde in dieser Arbeit ein Ansatz 
entwickelt, wie die Einhaltung einer Richtlinie für ein gegebenes 
C-Programm automatisch überprüft werden kann. Hierzu wird zunächst die 
gewünschte Richtlinie formalisiert, damit sie automatisiert analysiert 
werden kann. Da viele der Secure Coding Richtlinien den zeitlichen 
Ablauf bestimmter Ereigniße beschreiben, eignet sich Lineare 
Temporallogik (LTL) zum Formalisieren der Richtlinien. Im Rahmen 
dieser Arbeit wurde ebenfalls eine Sprache entwickelt, die es 
ermöglicht die in der Logikformel verwendeten propositionalen Atome 
auf konkrete C-Konstrukte abzubilden. Dieser Ansatz ermöglicht es 
abstrakte Eigenschaften auf konkret gegebene C-Programme abzubilden. 
Der Modelchecker SPIN kann für die in Linearer Temporallogik 
formalisierte Richtlinie überprüfen, ob diese auf dem Eingabeprogramm 
gilt. Allerdings kann SPIN nicht direkt C-Programme analysieren, 
sondern erwartet ein Promela-Modell als Eingabe, auf dem es die 
Analyse durchführt. Daher wurde in dieser Arbeit ein 
syntaxorientiertes übersetzungsverfahren entwickelt, welches das zu 
überprüfende C-Progamm automatisch in ein angemeßenes Promela-Modell 
übersetzt. Diese übersetzung kann auf zwei verschiedenen 
Abstraktionsebenen erfolgen. Die abstraktere Ebene betrachtet nur die 
Struktur des Kontrollflußgraphen des zu überprüfenden C-Programms. 
Dabei wird die Semantik ein zelner Anweisungen des C-Programms nicht 
betrachtet. Die detailliertere Ebene bildet die Semantik des 
C-Programms in Promela nach. Als Insipration für die zweite 
Abstraktionsebene diente das von Ke Jiang entwickelte 
übersetzungsverfahren C2Promela.