HiPerSec -Security and Performance Evaluation for Future JavaCard Architectures

Moderne Eingebettete Systeme erfordern für gewöhnlich ein hohes Maß an Informationssicherheit. Unglücklicherweise ist diese in einem System weder sichtbar noch messbar. Sie muss als Gesamtkonzept im System und auch im Entwicklungsprozess berücksichtigt werden. Sorgfältige Systemveriffikation ist notwendig um sicherzustellen, dass alle Sicherheitsanforderungen implementiert wurden. Solche Veriffikationen auf Systemebene sind bei heutigen Systemen sehr aufwändig und deswegen besonders teuer. Die Berücksichtigung von Sicherheitsanforderungen während eines Hardware/Software Codesign Prozesses hat einen groÿen Vorteil: Die Anforderungen können von Beginn des Entwicklungsprozesses berücksichtigt und fortlaufend mit dem Rest des Systems optimiert werden. Allerdings ist darauf zu achten, dass Optimierungen Verletzungen von Sicherheitsanforderungen zufolge haben können. Deswegen ist eine fortlaufende und automatisierte Sicherheitsveriffikation in einem iterativen Codesign-Prozess unumgänglich. Diese Arbeit beschreibt einen innovativen und iterativen Entwicklungsprozess. Dieser erlaubt die fortlaufende Optimierung und Veriffikation des Systems. Der Entwicklungsprozess basiert auf einem Systemmodell welches iterativ verfeinert und optimiert wird. Dies wird wiederholt bis alle Systemanforderungen erfüllt sind. Jede Iteration beinhaltet dabei ihre eigene Veriffikation aller Sicherheitsanforderungen. Dies stellt sicher dass Verletzungen von Sicherheitsanforderungen unverzüglich bemerkt und behoben werden. Der Ansatz dieser Arbeit beruht auf ergänzende Informationen (Meta-Informationen) die im Model bzw. in der Implementierung des Systems eingebettet sind. Diese Informationen können zur Laufzeit oder während einer Simulation ausgewertet werden und helfen das System zu Analysieren, zu Optimieren und auch zu Veriffizieren. In dieser Arbeit werden funktionale Sicherheitsanforderungen als Meta-Informationen dargestellt. Während einer Systemsimulation werden diese ausgewertet um dynamische Abhängigkeiten zwischen Systemkomponenten und Sicherheitsanforderungen herauszufinden. Darauf basierend kann eine Veriffikation durchgeführt werden. Unter anderem wird dies in dieser Dissertation mittels Formalen Methoden durchgeführt. Der wissenschaftliche Beitrag dieser Dissertation ist der innovative Hardware/Software Codesign-Ansatz mit der Verikation von Sicherheitsaspekten basierend auf einer systemweiten Simulation. Die nahtlose Integration von Sicherheitsanforderungen in das System sowie auch in den Entwicklungsprozess erlaubt eine regelmäÿige Optimierung und automatisierte Veriffikation des Systems. Diese Veriffikation wurde mittels Formalen Methoden durchgeführt ohne dabei die praktische Anwendbarkeit für den industriellen Einsatz einzubüßen.