Formale Verifikation und Validierung von Smart Cards

Giesecke & Devrient (G&D) ist weltweit führender Anbieter von Produkten für sicheren Zahlungsverkehr und die Identifizierung von Personen, Dokumenten und Waren (z.B. digitale Signatur, Biometrie). Unter anderem werden Chipkarten für die Bereiche Telekommunikation und Debit-/Creditsysteme entwickelt. Aufgrund der stark ansteigenden Komplexität der Chipkartensoftware und der mit diesen Produkten verbundenen Sicherheitsaspekte ist das Testen von Chipkartensoftware ein wesentlicher Bestandteil des SW-Entwicklungsprozesses bei G&D.

Der Beitrag zeigt, wie bei G&D formale auf Prädikatenlogik basierende Testentwurfstechniken erfolgreich eingesetzt werden, um z.B. die nach ITSEC geforderte Verifikation und Validierung von sicherheitskritischen Applikationen zu erfüllen. Neben der Methodik wird auch das G&D-Testtool SOCRATES zur formalen Testentwicklung vorgestellt.

Dr. Stefan Kriebel, Giesecke&Devrient GmbH