Jusletter IT

Im Bereich von e-Voting ist der Auszählungsvorgang der abgegebenen Stimmen, egal ob bei Präsenz- oder Distanzwahlen, eines der heikelsten und meist diskutierten Themen. Oft ist der genaue Ablauf bzw. die Nachvollziehbarkeit dieses Prozesses nur für Experten ersichtlich. Um der Wahlkommission oder Wahlbeobachtern bessere Möglichkeiten zur Überprüfung der Ergebnisse zu geben wurde ein Public Source Programm entwickelt, das diesen Zählprozess, in 2. Instanz und unabhängig von dem Softwaresystem des Wahlservers, ausführen kann.¹

Um die Software als solche – und damit die Ergebnisse – eindeutig zu verifizieren muss allerdings einen Schritt weitergegangen werden. Das Gebiet der Software Verifikation beschäftigt sich mit Methoden der formalen Beschreibung und Verifikation von Programmen. Dadurch wird die Funktionsweise der Software unmissverständlich abgebildet.

Ziel der Bemühungen ist somit eine formale Darstellung und ein Korrektheitsbeweis der Arbeitsweise des bereits vorhandenen «Counting Tools». Damit soll ein noch sichereres, effizienteres und verifiziertes Tool zur Kontrolle der Ergebnisse zur Verfügung gestellt werden. Um diesen Anforderungen gerecht zu werden ist es allerdings notwendig das Programm nach dem «Bottom-Up» Prinzip neu zu entwickeln.

Dieser Beitrag beginnt mit einem kurzen Einblick über das «Public Source Counting Tool» und leitet anschließend in die nötigen Schritte für eine formale Verifikation der Software über.

In diesem Kapitel wird ein kurzer Überblick über die Funktionsweise des Programms gegeben, eine genauere Beschreibung kann im Tagungsband der IRIS 2010² nachgelesen werden. Die System- und Testdokumentationen können auch online abgerufen werden.³

Als Input benötigt das Programm die verschlüsselten Stimmen («Ballots»), die Schlüsseldateien für die Entschlüsselung bzw. Signaturüberprüfung («Keyfile») und eine Datei für die Wahlparameter («Options»).⁴

Zuerst wird jeweils eine abgegebene Stimme aus der Ballot-Datei geholt, entschlüsselt und deren Signatur auf Basis des RSA Algorithmus⁵ überprüft. Sollten hierbei Fehler auftreten bricht das Programm mit einer entsprechenden Fehlermeldung ab. Sind Entschlüsselung und Signaturprüfung erfolgreich beginnt das Softwaretool mit dem Zählvorgang der jeweiligen Stimme.

Diese Phase beginnt mit der Auswertung einer gewählten Hauptoption (= Partei) die gewissen Parameterüberprüfungen, wie z.B. die max. Anzahl an abzugebenden Stimmen oder dem «invalid-Status», unterliegt. Diese Schritte werden für alle gewählten Hauptoptionen wiederholt, sollten dabei Fehler auftreten wird abgebrochen, der entsprechende Fehlerzähler erhöht und mit der Verarbeitung der Suboptionen (= Kanditaten) fortgefahren. Die Verarbeitung der Suboptionen erfolgt dabei nach demselben Schema nur wird hierbei zusätzlich, im Fall dass panagieren nicht erlaubt ist, überprüft ob die gewählte Hauptoption auch zur Suboption passt.

Abbildung 1: Ausschnitt des Auswertungsprozesses

Wenn alle Haupt- bzw. Suboptionen ausgewertet sind, holt das Programm die nächste Stimme in der Ballot-Datei, führt die Entschlüsselung und Signaturprüfung durch und beginnt danach wieder mit der Auswertung – es springt also wieder in den Hauptprozess zurück. Diese Prozedur wird solange wiederholt bis alle abgegebenen Stimmen ausgewertet sind.

Sollten bei der Auswertung Fehler auftreten, wird anhand der Art des Fehlers entschieden ob die gesamte Auswertung abgebrochen oder ein entsprechender Fehlerzähler erhöht wird. Am Ende wird das Ergebnis tabellarisch dargestellt.

Die Entwicklung einer fehlerfreien Software ist noch immer eine große Herausforderung. Es gibt verschiedene Ansätze um ihre Funktionsweise zu überprüfen. Eine beliebte Möglichkeit ist ein einfaches Testen des Programms, z.B. mit Hilfe von zufällig erzeugten Testwerten oder durch statistische Tests. Diese probabilistischen Nachweisverfahren sind einerseits kosteneffizient andererseits geben sie, je nach Umfang, mit einer gewissen Wahrscheinlichkeit die Zuverlässigkeit der Software an.⁶

Auch das oben vorgestellte Counting Tool wurde auf diese Weise auf seine korrekte Funktion überprüft. Damit die Wahrscheinlichkeit eines Softwarefehlers verschwindend gering bleibt sind sowohl die einzelnen Module als auch die komplette Software mit sogenannten Szenario- und Unittests überprüft worden.⁷

Aber nicht nur reines Testen führt zu einer fehlerfreien Software, vielmehr müssen auch die Spezifikationen korrekt umgesetzt sein und dies setzt eine regelmäßige Kommunikation zwischen dem Entwickler und Auftraggeber voraus.

Eine andere Möglichkeit eine Software eindeutig zu beschreiben und diese danach auf ihre Richtigkeit zu überprüfen, stellen die Methoden der Software Verifikation dar. Durch eine formale Beschreibung und eine zugrundeliegende Logik bieten sie den Rahmen um ein Softwaresystem systematisch zu spezifizieren, zu entwickeln und zu verifizieren. Dazu sind mehrere Schritte notwendig auf die unter Punkt 3.2. genauer eingegangen wird.

Interessante Beispiele für die Bedeutung der Software Verifikation sind prominente Software Fehler wie der Intel Fließkomma Bug⁸ im Jahr 1994, bei dem der Pentium Prozessor bei einigen Divisionen die letzten Kommastellen falsch berechnet hat oder eine Fehlberechnung in der Raumfahrt bei der die Raumfähre Endeavor ein Rendezvous mit dem Intelsat Satelliten aufgrund eines Rundungsfehlers in der Arithmetik verpasste.⁹

Wie u.a. aus den Beispielen hervorgeht, eignen sich diese Verifikationsmethoden besonders dort, wo an das Programm bzw. die Software hohe Qualitäts- oder Sicherheitsanforderungen gestellt werden.

Wie bereits erwähnt kann durch verschiedene Tests ein großer Funktionsbereich der Software abgedeckt werden. Ein Test kann zu einem gegebenen Zeitpunkt immer nur einen Zustandspfad abbilden daher hängt die Effektivität von der Art und Umfang des Tests und der Komplexität der Software ab.

Im Unterschied dazu wird mit Hilfe einer formalen Verifikation das gesamte Zustandsspektrum erfasst, es können somit Fehler aufgedeckt werden, die durch normales Testen einfach nicht erfasst werden können. Wie jedoch beim Testen kann es auch hierbei, je nach Art der verwendeten Methoden, zu Problemen kommen.¹⁰ Daher ist es wichtig, bereits zu Beginn der Spezifikation über die Vor- und Nachteile der einzelnen Verfahren Bescheid zu wissen und die geeignetste auszuwählen.

Um die Software formal zu verifizieren sind folgende Schritte notwendig:

Abbildung 2: Schritte der Umsetzung

Um das «Public Source Counting Tool» zu verifizieren ist es notwendig, es von Grund auf neu zu programmieren. Der erste Schritt beginnt mit der Transformation der informellen zu einer beweisfähigen, d.h. formalen, Beschreibung. Dieser Punkt setzt ein eindeutiges Verständnis der informellen Spezifikation voraus. Es werden sogenannte «Pre-, Postconditions» und «Invariants» (= logische Aussagen die wahr sein müssen) für die einzelnen Variablen bzw. Methoden oder Funktionen festgelegt, die zum Zeitpunkt des Methodenaufrufs 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, d.h. Bedienung durch ein geeignetes Verfahren, sichergestellt werden. Dieser Schritt ist die eigentliche Verifikation der Software. Er kann sowohl per Hand als auch unter Verwendung von speziellen Tools durchgeführt werden. Hierbei wird die Einhaltung der logischen Aussagen für einzelnen Funkionen einerseits und die Beziehungen zueinander unter der Zuhilfenahme von sogenannten Axiomen andererseits bewiesen.

Diese Entwicklung soll modulbasiert sein, daher werden zuerst die beiden Hauptmodule RSA und XML, danach der korrekte Zählvorgang und am Ende der «Rest», d.h. das Zusammenspiel der einzelnen Module, der Software spezifiziert und verifiziert. Vor allem der Korrektheitsbeweis des RSA Kryptographie Moduls kann sich als herausfordernder Punkt herausstellen. Formale Verifikation ist auf dem Gebiet der Kryptographie erst rudimentär entwickelt, einen möglichen Umsetzungsansatz für dieses Modul stellt die Arbeit von Boyer und Moore¹¹ dar.

Zu beachten ist, dass das Projekt die jeweiligen konkreten Implementierungen und die eigentliche Arbeitsweise der Software verifiziert und nicht die zugrundliegenden Algorithmen. Das bedeutet z.B. in Hinsicht auf das RSA Modul, dass nicht der RSA Algorithmus überprüft wird sondern seine konkrete Implementierung in die Software.

Um dieses und weitere Probleme auszuschließen und den Arbeitsbereich von Anfang an eindeutig zu definieren werden gewisse «trusted components» eingeführt die als gegeben betrachtet werden. Diese sind u.a. gewisse Java Komponenten wie die «BigInteger» Klasse, das Betriebssystem und die Computerhardware bzw. Software auf der das Programm läuft.

Der letzte Schritt beschäftigt sich mit der Umsetzung der formalen Spezifikation in die gewünschte Programmiersprache. Im Falle des «Public Source Counting Tools» handelt es sich hierbei um Java. Es gibt bereits Ansätze in denen im Source Code die Spezifikation erfolgt und dadurch eine enge Verbindung zwischen Spezifikation und Umsetzung entsteht. In diesem Zusammenhang ist das Key-Projekt, das u.a. auch mit der Java Modeling Language (JML) arbeitet, zu nennen.¹²

Dieses Projekt zielt auf eine Steigerung des Vertrauens in die richtige Auswertung der Stimmabgaben ab und richtet sich vor allem an jene Personen, die sich mit diesem Prozess und/oder der Überprüfung von e-Voting Wahlen beschäftigen. Das einleitend vorgestellte Tool ist bereits fertig entwickelt und damit voll einsatzfähig. Die Stärke liegt vor allem in seiner Eigenständigkeit ( es kann unabhängig von der bei der elektronischen Wahl verwendeten Software zur Überprüfung der Wahlergebnisse herangezogen werden. Die in diesem Beitrag vorgestellte Möglichkeit der Verifizierung der Software soll diesen Effekt nochmals steigern. Der Zählvorgang stellt die eigentliche Funktion des Tools dar und daher wird diesem für die Verifikation ein ganz besonderes Augenmerk geschenkt werden. Auch und vor allem das RSA Kryptographie Modul ist eine wichtige Kernkomponente für die korrekte Arbeitsweise und wird daher genauso detailreich spezifiziert und überprüft werden. Ein weiterer Mehrwert dieses Projekts besteht darin, dass die Module, wie bspw. RSA Verschlüsselung oder XML-Parser, einzeln sowie auch in Kombination miteinander verifiziert und somit auch in anderen Projekten eingesetzt werden können.

Beckert, B.; Hähnle, R., & Schmitt, P.H. (Hrsg .), Verification of Object-Oriented Software: The KeY Approach, Springer Verlag, Berlin (2007).
Berezin , S.,Model Checking and Theorem Proving: a Unified Framework , Carnegie Mellon University, Pittsburgh (2002)
Boyer, R.S., & Moore J.S., Proof Checking the RSA Public Key Encryption Algorithm. In: The American Mathematical Monthly, Vol. 91, No. 3 S. 181-189 (1984)
Coe, T., Mathisen, T., Moler, C.& Pratt, V., Computational aspects of the Pentium affair. In:Computational Science & Engineering, IEEE , Volume: 2,Issue: 1 , S. 18-30 (1995)
Ehrenberger, W., Software Verifikation, Carl Hanser Verlag, Wien (2002)
Neumann, P.G., Computer Related Risks, Addison Wesley (1995)
Prosser, A., The Ruling of the Federal Constitutional Court on Evoting and Its Technical Consequences for Internet Voting. In: Prosser, A., Parycek P. (Hrsg.), Proceedings of EDEM 2009, books@ocg.at, S. 17-26 (2009)
Prosser, A., Public Verification System (PubVeriS) for eVoting Version 1.0 Interface Definition,www.e-voting.at/countingtool/download/PubVeriS_Interface.pdf aufgerufen am: 12. Januar 2011
Rivest, R., Shamir, A., & Adleman, L., A method for obtaining Digital Signatures and Public Key Cryptosystems. In: Communications of the ACM, Vol. 21(2), S. 120-126 (1978)
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,www.evoting.at/countingtool , aufgerufen 12. Januar 2011

---

Alexander Scheidl, Dissertant, Department für Informationsverarbeitung und Prozessmanagement, Augasse 2- 6, 1090 Wien AT,alexander.scheidl@wu.ac.at

---