Jusletter IT

Bei den beiden letzten IRIS-Tagungen wurde bereits eine unabhängige Stimmauswertungssoftware „Public Source Counting Tool“ und mögliche Refinement-Schritte zur Verifikation dieser vorgestellt.^{1 ,2}

Diese „Refinements“ sind jedoch mehr als eine bloße Verbesserung, vielmehr wird das gesamte Programm einer kompletten Revision unterzogen. Dies soll jedoch nicht durch verschiedene dynamische Testszenarien – z.B. im trivialen Fall durch zufällig generierte Strings – erfolgen, sondern das Programm soll mit Hilfe einer formalen Verifikation auf vollständige Korrektheit überprüft und damit verifiziert werden.

Allerdings erfolgt dieser Schritt nicht alleine, sondern soll als ein „Community-Based“-Projekt umgesetzt werden. Ein Wiki wird als eine Entwicklungs- und Dokumentationsplattform dienen und für jedermann frei zugänglich sein. Des Weiteren können interessierte Personen den Fortschritt und die verwendeten Methoden zur formalen Verifizierung verfolgen und ggfs. nachprüfen.

Dieser Beitrag gibt einen kurzen Überblick über die formale Verifizierung und soll dem Leser die Vorteile der Verwendung eines Wikis und dessen praktische Anwendung in diesem Bereich näher aufzeigen.

Gängige Methoden um die Funktionalität eines Programms sicherzustellen, sind beispielsweise verschiedene systematische Testverfahren, wie u.a. Szenario- bzw. Unittests, oder aber auch einfache Programmanalysen.³

Diese Methoden stellen eine gute Möglichkeit dar, um ein Programm auf seine korrekte Arbeitsweise hin zu überprüfen, jedoch sind sie nicht der Weisheit letzter Schluss. Je komplexer ein Programm desto wahrscheinlicher ist es, mit verschiedenen Tests nicht alle Zustände abbilden zu können. Somit ist es auch nicht möglich, eindeutige Aussagen – „true“ oder „false“ – über einzelne Programmteile zu bilden, im Idealfall gelingt es, die richtige Funktionsweise mit einer hohen Wahrscheinlichkeit zu belegen.

Wird hingegen die Software eindeutig formal – d.h. mit Hilfe von mathematischen Methoden – beschrieben und damit ein formales Modell des Programms erstellt, so sind eindeutige Aussagen möglich.

In diesem Beitrag bezieht sich der Begriff „Software-Verifikation“ immer auf eine formale Beschreibung mit anschließender Verifikation. Um eine Spezifikation – damit ist eine Definition über das Verhalten eines bestimmten Programmteils gemeint – gemäß obiger Definition zu verifizieren, muss man diese zuerst formal beschreiben und erst dann ist eine Verifikation möglich.

Als erstes beginnt die Transformation der informellen zu einer beweisfähigen, d.h. formalen, Beschreibung. Es werden sogenannte Verträge wie „Pre-, Postconditions“ und „Invariants“ – logische Aussagen die wahr sein müssen – für die einzelnen Programmvariablen bzw. -funktionen festgelegt, die zum Zeitpunkt des Aufrufs bzw. zum Zeitpunkt der Beendigung erfüllt sein müssen.

Liegt diese formale Spezifikation vor, kann die Korrektheit der Software unter der Führung mathematischer Beweise, sichergestellt werden. Dieser Schritt ist die eigentliche Verifikation der Software.

Um den Umfang von Anfang an eindeutig zu definieren werden sogenannte „trusted components“ eingeführt, die nicht weiter bearbeitet werden, sondern als gegeben betrachtet werden. Dies ist nötig, da es nicht möglich ist, alle Komponenten die auf die Software einwirken – wie z.B. das Betriebssystem oder die Computerhardware – formal zu verifizieren.

Ein Beispiel wie sich Verifikation vom normalen Testen unterscheidet bzw. detailliertere Ausführungen zu den oben genannten Schritten kann im EDEM2011-Beitrag des Autors gefunden werden.⁴

Prinzipiell lässt sich festhalten, dass diese Schritte entweder per Hand oder mit Hilfe eines Software-Tools, z.B. durch einen sogenannten „Theorem Prover“, durchgeführt werden können. Eine Verifikation per Hand ist allerdings fehleranfällig, da sich bei der Anwendung der verschiedenen Regeln Fehler einschleichen können.

Das Projekt soll ein höchstmögliches Maß an Transparenz, Wiederverwendbarkeit und Kompatibilität gewährleisten und daher ist die „manuelle“ Methode nicht die bevorzugte Wahl. Vielmehr wird ein Tool gesucht, welches die oben genannten Kriterien erfüllt.

Das „KeY“-Softwareprogramm ist ein Gemeinschaftsprojekt der Universität Karlsruhe, der Technischen Universität Chalmers in Göteborg und der TU Darmstadt. Ziel des Tools ist es, das Design, die Spezifikation, die Verifikation und die Implementierung von objektorientierter Software so nahtlos wie möglich zu gestalten.

Das Programm basiert auf der „Java Card“⁵ Programmiersprache, welche ein Subset von „Java 1.4“ darstellt. Es unterstützt außerdem die OCL-⁶ und JML-⁷ Sprachkonstrukte, die helfen, die Visualisierung der einzelnen Programmmodule bzw. des Programmablaufs darzustellen und die „Verträge” – d.h. die zu erfüllenden (Methoden-)Bedingungen – zu definieren.

Das „KeY“ Tool transformiert diese Vertragsbedingungen in sogenannte „Proof-Obligations“, die die logische Validität anhand der vorgegebenen Spezifikation überprüfen sollen. Die hierfür verwendete Logik nennt sich „Dynamic Logic“, welche – abgekürzt formuliert – eine Erweiterung der Prädikatenlogik um ausführbare Programmfragmente darstellt.

Die eigentliche Verifikation erfolgt damit in „KeY“ deduktiv, die aufgestellten Bedingungen werden anhand vorgegebener Regeln – im „KeY-System“ auch „Taclets“ genannt – überprüft und ausgewertet. Diese Verifikationsschritte werden vollautomatisch oder auch interaktiv – das Tool stoppt wenn es für ein konkretes Problem keine Lösung findet – durchgeführt. Sollte die vorhandene Basis an „Taclets“ nicht ausreichen, so gibt es die Möglichkeit eigene zu definieren oder den Verifikationsprozess an ausgewählte externe Solver weiterzuleiten.⁸

Genau diese Komponenten und die Tatsache, dass das Key Softwaretool unter einer freien Lizenz – GNU⁹ – angeboten wird, machen es zu einem geeigneten Kandidaten für die angestrebte Verifikation des „Public Source Counting“ Tools.

Die Verifikation einer nicht-trivialen Anwendung ist allerdings kein einfaches Unterfangen, vielmehr muss es als komplizierter und langwieriger Prozess angesehen werden. Meistens werden solche Verifikationsmethoden nur in Bereichen mit hohen Sicherheits- bzw. Qualitätsanforderungen eingesetzt.

Dieses Projekt versucht jedoch einen anderen Lösungsweg, die Software soll mit Hilfe eines Wikis von der Community verifiziert und kontrolliert werden. Dieser Ansatz ist nach Wissen des Autors ein Novum in diesem Bereich und soll im Folgenden kurz erläutert werden.

Der Begriff “Community” ist in diesem Beitrag als ein virtuelles „Come-Together“ von interessierten Leuten definiert. Virtuell bedeutet hierbei, dass die beteiligten Personen nicht denselben physischen Ort teilen bzw. zur selben Zeit anwesend sein müssen.

Damit können einerseits Unternehmen genannt werden, die die Software nutzen wollen oder aber auch Universitäten, die die Software bzw. die Verifikationsschritte in der Lehre oder zwecks Nachprüfung einsetzen wollen. Diese Definition umfasst aber auch (Einzel-)Personen, die einfach an der Software und der Überprüfung der Software interessiert sind.

Außerdem lässt sich festhalten, dass auch für e-Voting zuständige Behörden auf das Projekt Zugriff nehmen können und dadurch die Dokumentation, den Fortschritt und die Überprüfung des Softwaretools nachlesen bzw. selber nachvollziehen können.

Um das Projekt auch weiterhin gemeinschaftsbasiert nennen zu können, braucht die „Community“ einen gemeinsamen Kontext – in diesem speziellen Fall den Bereich e-Voting –, ein gemeinsames Entwicklungstool – „KeY“ und „Java“ – und einen gemeinsamen Raum – den Wiki.¹⁰

„Wikiwiki“ ist das hawaiianische Wort für „schnell” oder „sich beeilen”. Der Name beschreibt damit bereits die typische Charakteristik einer Wiki-Software. Sie soll dem User – der „Community“ – die Möglichkeit bieten, schnell und unkompliziert einen Beitrag zu schreiben. Der Fokus soll auf dem Inhalt des Beitrags und nicht auf dem der einzelnen Veröffentlichungsschritte liegen. Ein Wiki stellt somit eine einfache Plattform für gemeinschaftliche Arbeit an Texten und Beiträgen dar.¹¹

Technisch wird der Wiki über einen Internet-Server mit Datenbank, meist SQL mit PHP-Hypertext-Preprocessor, realisiert. Für dieses Projekt wurde eines der meistgenutzten und berühmtesten Wiki-Softwaresysteme MediaWiki gewählt.12

Einerseits findet es eine hohe Verbreitungsdichte – ist damit auch einfach zu nutzen und erhält laufend Updates – anderseits bietet es umfassende Funktionalität und ermöglicht auch Erweiterungen, wie z.B. ein Ticket-System für ein effizientes Bug-Tracking oder ein Subversion-System welches Änderungen protokolliert und somit sicherstellt, dass die User immer mit der aktuellsten Version des Programms arbeiten, die den eigentlichen Wiki weiter verbessern.

In Abbildung 1 wird ein Ausschnitt des Wikis dargestellt. Auf der linken Seite ist die Navigationsstruktur mit blauer Schrift und grauem Hintergrund. Hier befinden sich die Hauptmenüpunkte, wie die „Interface Definition“ – die Dokumentation über die benötigten Inputs für die Software –, ein „Process Overview” – stellt die einzelnen Programmethoden und deren Interaktion dar –, die „Open Tasks“ – die To-do Liste –, eine Anleitung wie das Programm funktioniert und wie die Ergebnisse zu interpretieren sind und der wichtigste Punkt, die Modul-Sektion.

In diesem Menüpunkt werden alle Klassen, deren Methoden und Bedeutung übersichtlich aufgelistet. Es ist damit möglich jede einzelne Methode einer Klasse sichtbar zu machen und deren Funktionalität sowie formale Verifikation darzustellen.

In Abbildung 1 wird im „MainFrame“ gerade die Counterklasse dargestellt. Diese Klasse wird beispielsweise für die Fehlerzähler oder aber auch für die Optionszähler der Software verwendet.¹³ Wie ersichtlich, wird zuerst eine allgemeine Beschreibung der Klasse angegeben, danach deren Java-Quellcode und schließlich für jede einzelne Methode die formale Spezifikation bzw. deren formaler Beweis angegeben.

Die Methode „increase“ erhöht beispielsweise den Variablenwert um 1. Der triviale Programmcode lautet hierfür:

Counter++

Die sehr vereinfachte formale Spezifikation für diesen Umstand lautet:

Counter = 0     -->   (Counter = 1)

 

Diese Implikation gibt für den Spezialfall, dass das Counterobjekt gestartet wird, den Wert 0 zugewiesen bekommt und nachdem der Aufruf erfolgt und beendet wurde dieser den Wert 1 – damit um 1 erhöht wurde – erhält.

Diese formale Definition könnte, würde sie verallgemeinert werden, eine erste „Postcondition“ darstellen, die der Methodenkontrakt im Beweisführungsverfahren nach dem Methodenaufruf zu erfüllen hat. Des Weiteren müssten noch Annahmen über die „Preconditions“ – jene Bedingungen die beim Start der Methode erfüllt sein müssen – getroffen werden. Diese können im vorliegenden Fall beispielsweise einen Hinweis enthalten, dass das Counterobjekt bereits generiert worden sein muss, d.h. also <> null sein muss.

All diese formalen Spezifikationen erfolgen direkt im Java-Quellcode über sogenannte Metakonstrukte mit Hilfe der Java Modeling Language (JML). Diese Metasprache eignet sich hervorragend für die Spezifikation über das Verhalten von Methoden und Klassen. Außerdem hat die JML einen de-facto-Standard und ist somit kompatibel mit anderen alternativen Verifikationstools.¹⁴

Sobald diese formale Definition abgeschlossen ist, kann das ganze Konstrukt in ein geeignetes Tool – wie z.B. die oben vorgestellte Software „KeY“ – übernommen werden und dort auf deren Korrektheit überprüft werden. Die Software protokolliert die einzelnen Schritte, d.h. führt Aufzeichnungen über die angewendeten Regeln – logische Schritte zur deduktiven Vereinfachung des Problems. Das Protokoll wird dann als „Proof“ der Methode im Wiki publiziert und kann dann wiederum von einer dritten Person in das Verifikationstool geladen und nachgeprüft werden.

Die logischen Schritte zur Auflösung des – wenn auch im obigen Fall trivialen – Problems basieren auf der zugrundeliegenden Logik. Eine einfache Regel, die u.a. hierbei angewendet wird, ist der „Modus Ponens“, der bspw. aus 2 Prämissen (A, B) und der Implikation A-> B aussagt, dass wenn A gilt auch – als Conclusio – B gilt.

Durch den Community-Ansatz soll, wie schon von einem der berühmtesten Wiki-Modelle „Wikipedia“ vorgezeigt, eine beträchtliche Akzeptanz und Verbreitungsdichte – sowohl in Hinblick auf e-Voting generell als auch auf die Software selber – erzielt werden.

Im Bereich der formalen Verifikation ist dieser Problemlösungsansatz als neu zu werten, da diese Beweisführungsmethoden aufgrund des hohen Aufwands meist nur in sicherheitsrelevanten Bereichen oder in Domänen mit hohen Investitionskosten und geringer Fehlertoleranz, wie bspw. der Luft- u. Raumfahrt oder der Automobilindustrie, eingesetzt werden.

Eine verifizierte Software, die einen unabhängigen “recount“ der Stimmen (inkl. der Verifikation der Stimmberechtigung und -abgabe) ermöglicht, bietet den Benutzern die Möglichkeit, nicht formal verifizierte Wahlergebnisse der Erstauszählung nachzuprüfen und somit bei Übereinstimmung beider Ergebnisse die Stimmauszählung als formal verifiziert zu werten.

Um die benötigte Reichweite im World Wide Web zu erhalten, ist es äußerst wichtig, einen Partner bzw. Webseitenbetreiber, der bereits gut in den diversen Suchmaschinen gelistet ist, zu finden. Der Autor ist glücklich, einen solchen Partner in der Österreichischen Computer Gesellschaft (OCG) gefunden zu haben, deren Webseite (www.ocg.at) als Host für den Wiki fungieren wird.

Demuth, B., OCL Portal, http://www-st.inf.tu-dresden.de/ocl/ aufgerufen 2011.

Ebersbach, A., Glaser, M., Heigl, R., Wiki-Tools: Kooperation im Web, Springer, Berlin (2005).

Ehrenberger, W., Software-Verifikation, Carl Hanser Verlag, Wien (2000).

Free Software Foundation (Hrsg.), GNU Operating System, http://www.gnu.org/licenses/gpl.html aufgerufen 2011.

Leavens, G., The Java Modeling Language JML, http://www.eecs.ucf.edu/~leavens/JML/ aufgerufen 2011.

MediaWiki (Hrsg.), How does MediaWiki work?, http://www.mediawiki.org/wiki/MediaWiki, aufgerufen 2011.

Oracle (Hrsg.), Java Card Technology, http://www.oracle.com/technetwork/java/javacard/overview/index.html aufgerufen 2012.

Scheidl, A., An Independent E-Voting Recount Solution - Introduction To A Community-Based Development and Revision Approach. In: Prosser, A., Golob, B., Leitner, C., Simic, D., (eds.), Conference Proceedings Eastern European e|Gov Days 2011, books@ocg.at, p. 97–108 (2011).

Scheidl, A., Public Source Counting Software für verifizierbares E-Voting. In: Schweighofer, E., Geist, A., Staufer, I., (Hrsg.), Tagungsband des 13. Internationalen Rechtsinformatik Symposions IRIS 2010, books@ocg.at, S. 103-110 (2010).

Scheidl, A., Public Source Counting Tool für eine Unabhängige Stimmenauswertung bei e-Voting – Ein Verifikationsansatz. In: Schweighofer, E., Kummer, F., (Hrsg.), Tagungsband des 14. Internationalen Rechtsinformatik Symposions IRIS 2011, books@ocg.at, S. 297-302 (2011).

Scheidl, A., Public Source Counting Tool, http://www.evoting.at/countingtool aufgerufen 2011.

Weiß, B., Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction, Universität Karlsruhe Universitätsbibliothek, Karlsruhe, S. 3–10. (2011).

Wise, G., Appendix A for An EPA/USDA Partnership to Support Community-Based Education. In: Applying US Community Development Process Lessons (1998).