Formale Spezifikation generischer ITSEC-Funktionalitätsklassen

Wir skizzieren einen bei DST derzeit untersuchten Ansatz zur formalen Spezifikation der in den ITSEC beschriebenen Funktionalitätsklassen. Auf Grundlage der formalen Spezifikation läßt sich die Konsistenz der (formalen) Spezifikation eines konkreten Produktes zu den Vorgaben der ITSEC nicht nur informal motivieren, sondern mathematisch beweisen. Auf diese Weise wird die Objektivierbarkeit, die Qualität und die Effizienz des Evaluierungsprozesses gesteigert. Für die Evaluierung von Produkten gemäß Stufe E6 ist die Anwendung der hier geschilderten oder vergleichbarer Konzepte unverzichtbar.