NSA: Fehlerfreie Software ist wirtschaftlich machbar

Der US-Geheimdienst National Security Agency (NSA) hat eine Fallstudie für die Entwicklung sicheren Codes veröffentlicht. Diese entstand im Rahmen eines Projekts zur Arbeit an einem biometrischen Zugangssicherungssystem. Die Software-Entwicklung erfolgte dabei im Auftrag der NSA bei dem britischen Unternehmen Praxis High Integrity Systems. Dieses hat den Tokeneer genannten Code nun zusammen mit den Design-Zielen, Arbeitsabläufen und Spezifikationen offen gelegt.

Drei Entwickler von Praxis haben den 10.000 Zeilen langen Quellcode geschrieben. Sie hatten dafür 260 Personentage Zeit. Pro Tag und Mitarbeiter wurden also lediglich 38 Zeilen neuen Codes programmiert. Dadurch blieb ausreichend Zeit, die Sicherheit des jeweiligen Abschnitts selbst sowie im Zusammenhang mit anderen Komponenten zu prüfen.

Die Entwickler nannten ihr Arbeitskonzept "Correctness by Construction". Dieses umfasste unter anderem die genaue Dokumentation des Codes, eine häufige Prüfung und die Nutzung der Programmiersprache SPARK, eine Ada-Variante, die eine gute statistische Analyse der Sourcen ermöglicht.

Nach dem Abschluss des Projekts wurde die Software einer tiefgehenden Prüfung unterzogen. Dabei konnten keine Fehler mehr festgestellt werden, die zu Sicherheitslücken führen würden, hieß es. Das Programm erfüllte sogar die harten Anforderungen des Common Criteria Evaluation Assurance Level (EAL) 5.

EAL ist eine Spezifikation, in der die Prüftiefe und die daraus resultierende Vertrauenswürdigkeit von Software beschrieben wird. Bisher galt es nicht als sinnvoll, herkömmliche Software mit EAL5 zu entwickeln. Hierfür wurden stets besondere Anforderungen, bei denen es nicht auf die Wirtschaftlichkeit ankam, angenommen. Tokeneer soll nun der Gegenbeweis für diese These sein.

Weitere Informationen: Tokeneer-Projekt