Jusletter IT

Internetwahlen sind gerade in der jüngeren Vergangenheit nicht immer reibungslos abgelaufen. Ein zu nennendes Beispiel wäre hier die ÖH-Wahl 2009.¹ Es liegt an dem natürlichen Unterschied zur gewöhnlichen Papierwahl, dass gerade bei elektronischen Wahl ein erhöhter Bedarf an Überprüfbarkeit und Nachvollziehbarkeit besteht. E-Voting an sich ist zukunftsträchtig und mit einer Verbesserung der bestehenden Lösungen bzw. Einsatz neuer Umsetzungsmöglichkeiten sollte auch diese neue Technologie überprüfbar werden.

Ein möglicher Ansatz stellt dieses «Public-Source-Counting-Tool» für das «Public Verification System (PubVeriS)»² dar. Es ermöglicht unabhängig von der verwendeten Software des Wahlservers, dieser muss nur die Datenstrings anhand der spezifizierten Interfacedefinitionen exportieren, eine verschlüsselte Wahlurne zu analysieren und auszuwerten. Desweiteren bietet es die Möglichkeit die Inputs in ein Spreadsheet zu exportieren und stellt somit die Schnittstelle zu anderen Auswertungsmethoden, bspw. per Hand oder ein anderes Tool, her.

Um die Verwendungsmöglichkeit nicht gleich von Beginn einzuschränken wurde es mit Hilfe der Programmiersprache Java³ programmiert. Da Java frei zugänglich und auch der Quellcode des Programms im Internet veröffentlich ist, wird ein hohes Maß an Transparenz und Überprüfbarkeit gewährleistet.

Um desweiteren eine möglichst einwandfreie Funktionalität zu gewährleisten wurden die einzelnen Modulteile sogenannten Unittests unterzogen und die gesamte Software abschließend mit Szenariotests, sprich Probewahlen, überprüft.

Jedoch kann man hierbei nicht von Verifikation im eigentlichen Sinne reden, um eine Software zu verifizieren muss Sie eindeutigen formalen Methoden entsprechen und diese in jedem Zustand erfüllen. Tests an sich bilden jeweils nur einzelne Zustände ab und können somit nur von Fall zu Fall unterscheiden, jedoch nie mit einer 100%igen Sicherheit alle Fälle und möglichen Zustände abbilden. Hier setzt das Konzept der Softwareverifikation an, welches im Rahmen der Dissertation umgesetzt werden soll.

Das Counting Tool wurde von mir in meiner Diplomarbeit entwickelt und nun soll dieses mit Hilfe von Methoden der Software Verifikation «Bottom-Up» neu entwickelt werden um eben jene Forschungslücke im Bereich von E-Voting zu schließen.

Zuerst wird in diesem Beitrag auf die ursprüngliche Software und deren Funktionalität eingegangen. Abschließend soll der Unterschied zwischen dem gewöhnlichen testen und Verifikation der Software dargestellt werden.

Um eine sichere und nachvollziehbare Funktionsweise dieses Analysetools zu gewährleisten wurde es von Anfang an anhand der vorgegebenen Spezifikationen prozessorientiert entwickelt.

Den Anfang der Entwicklung stellte also der Aufbau und Ablauf der einzelnen Prozesse dar. Diese wurden mit Hilfe von sogenannten Ereignisprozessketten (kurz EPK) verwirklicht. Um die einzelnen Prozesse zu überprüfen wurden Unittests der einzelnen Hauptmodule (RSA und XML) durchgeführt.

Den Abschluss der Entwicklung stellten sogenannte Szenariotests dar. Hierbei wurden verschiedene Testwahlen erzeugt und anschließend mit dem Programm analysiert. Die Ergebnisse mussten hierbei mit den Auswertungen des Wahlservers übereinstimmen.

Die Interfacedefinitionen⁴ stellen den Ausgangspunkt der Arbeit dar. Hierbei werden alle benötigten Inputs-Files und das Aussehen dieser vorgegeben. Folgende Dateien werden benötigt:

Die Options- und Ballotdateien sind im Election Mark-up Language (kurz EML)⁶ Format, die Schlüsseldatei im XML-Format. Alle Dateien beinhalten also die in der Spezifikation angegebenen Tags. Die Optionsdatei gibt die Parameter vor, mit Hilfe der Schlüsseldatei kann die Ballotdatei entschlüsselt werden und gibt somit die Stimmen frei, die dann anschließend noch überprüft werden.

Der Output des Programms bezieht sich einerseits auf die Ergebnisdarstellung als Tabelle, andererseits auf die Möglichkeit die entschlüsselten Stimmen (optional mit Signaturtoken), also die Rohdaten, in ein Spreadsheet (CSV-File) zu exportieren.

Damit soll sichergestellt sein, dass man mit externen Programmen oder per Hand die Ergebnisse nachrechnen und überprüfen kann.

Das Programm basiert auf einzelnen Prozessen die in einem bestimmten Ablauf abgerufen werden. Grob unterteilt laufen 2 Schienen, die im Folgenden näher erklärt werden.

Diese Kette beginnt mit dem Start und endet mit dem Beenden des Programms. Zuerst können die verschiedenen Inputfiles, die Options-, Schlüssel- und Ballotdatei [siehe 2.1. ], eingelesen werden. Beim Einlesen der Optionsdatei werden gleichzeitig die Parameter und Zähler für die Stimmabgaben initialisiert. Zusätzlich kann optional gewählt werden ob ein Export der Stimmendatei (mit/ohne Signaturtoken) erfolgen soll.

Danach wird, ausgelöst durch den Klick auf den Start-Button, die Stimmverarbeitung gestartet. Nun holt das Programm eine Stimme inkl. zugehörigen Signaturtoken aus der Ballotdatei, entschlüsselt diese und prüft die Signatur. Sowohl die Signaturprüfung als auch die Entschlüsselung erfolgen durch den RSA Algorithmus⁷.

Danach beginnt der Auswertungsprozess für eine Stimme [siehe 2.3.2. ], nachdem dieser beendet ist erfolgt eine Überprüfung, ob noch weitere Stimmen in der Ballotdatei vorhanden sind. Wenn ja, wird diese Stimme geholt und wiederum entschlüsselt, überprüft und ausgewertet. Dieser Prozess wiederholt sich solange bis keine weiteren Stimmen mehr zur Auszählung vorhanden sind, dann wird das Wahlergebnis tabellarisch dargestellt.

Diese Prozesskette wertet eine Stimme aus. Innerhalb dieser Stimme können mehrere Haupt- bzw. Suboptionen gewählt werden. Wie viele genau erlaubt sind bestimmen die Parameter aus dem Optionsfile.

Die Auswertung beginnt, indem das Programm die 1. gewählte Hauptoption erfasst und überprüft ob es sich um eine normale Stimme oder Streichung handelt. Sollte es sich um eine Streichung handeln so wird automatisch die gewählte Option im Counter entsprechend, d.h. der «Streichungszähler» erhöht. Wenn es eine «normale» Stimmabgabe ist wird kontrolliert ob es sich um eine «Invalid Option» [siehe 2.4.1. ] handelt, welche je nach Art, als «invalid all» Option den Abbruch der Auswertung aller Optionen, als «invalid main» den der Hauptoptionen mit sich zieht. Wichtig ist, dass hierbei die «invalid» Option noch erhöht wird und somit ins Endergebnis einfließt.

Wurde eine «valid» Option, also eine normale Partei gewählt, wird der entsprechende Optionszähler erhöht. Danach wird überprüft ob diese Erhöhung die in dem Optionsfile angegebenen Parameter erfüllt. Sollte hierbei ein Fehler festgestellt werden wird der entsprechende Fehlerzähler erhöht, die Verarbeitung der Hauptoptionen gestoppt und mit der der Suboptionen fortgefahren. Wenn kein Fehler auftritt wird überprüft ob es noch weitere gewählte Hauptoptionen gibt, wenn ja wird mit der Verarbeitung dieser fortgefahren bis es keine weiteren mehr gibt.

Dann beginnt die Verarbeitung der Suboptionen, also die der Parteikandidaten. Prinzipiell ist die Verarbeitung dieser identisch mit jener der Hauptoptionen, nur das es hierbei keine «invalid» Optionen gibt, dafür aber der Panagierstatus überprüft wird. Panagieren bedeutet, dass die gewählte Suboption nicht zwangsweise mit der der Hauptoption zusammenstimmen muss, also die Vorzugsstimme nicht mit der gewählten Partei übereinzustimmen hat.

Ob panagieren erlaubt ist oder nicht bestimmt wiederum ein Parameter aus dem Optionsfile. Wenn es nicht erlaubt ist wird explizit überprüft ob die gewählte Suboption mit einer gewählten Hauptoption zusammenpasst. Sollte dies vorkommen wird die Verarbeitung der Suboptionen abgebrochen und das Programm kehrt zur Hauptprozesskette zurück, wo es die Auswertung weiterer Stimmen vornimmt.

Diese Optionen sind normale Optionen die im Optionsfile durch einen speziellen Codetag als ungültig gekennzeichnet sind:

• «invalid all» gesamte Stimme (Haupt-/Suboptionen sind ungültig)
• «invalid main» Hauptoptionen sind ungültig, Suboptionen werden gezählt.

Diese spezielle Kennzeichnung soll es dem Wähler, wie bei der normalen Papierwahl wenn er beispielsweise alles durchstreicht, ermöglichen seinen Willen ungültig zu wählen zu zeigen.

Diese Fehler treten im Ablauf auf, werden aber alle vom Programm abgefangen und dabei wird jeweils der entsprechende Fehlerzähler erhöht.

• Gewählte Option ist nicht im Optionsfile, die gesamte Stimmabgabe ist ungültig.
• Parameter des Optionsfiles werden überschritten, jeweilige Optionsrubrik ist ungültig.
• Die Anzahl der erlaubten Stimmen die Haupt-/Suboptionen wurde überschritten.
• Die Anzahl der erlaubten Stimmen für eine Haupt-/Suboption, die kumuliert werden dürfen, wurde überschritten.
• Die Anzahl der erlaubten Streichungen der Haupt-/Suboptionen wurde überschritten.
• bei Suboptionen: Panagierfehler

Wie oben erwähnt erhöht jeder dieser Fehler einen entsprechenden Fehlerzähler. Damit kann auch die Anzahl der fehlerhaften Stimmen ausgewertet werden.

Diese schwerwiegenden Fehler führen immer zu einem Abbruch des Programms ohne weitere Auswertung der Ergebnisse. Folgende Fehler kommen dafür in Frage:

• Die Contest ID⁸ der Optionsdatei stimmt nicht mit der Contest ID der Ballotdatei überein.
• Es wurden Haupt-/ Suboptionen gewählt, in der Optionsdatei sind aber keine Haupt-/Suboptionen vorhanden.
• Kryptografiefehler (Entschüsselungsfehler oder Signaturfehler), da diese Fehler entweder auf eine Manipulation oder falsche Daten zurückzuführen sind.

Die Frage die sich am Ende des Entwicklungsprozesses stellen sind:

• Erfüllt die Software die Anforderungen?
• Wie kann man sicherstellen, dass die Software das macht, was sie machen soll?

Während sich die erste Frage noch relativ einfach abklären lässt (Abgleich mit dem Pflichten- bzw. Lastenheft, Treffen mit Kunden usw.), ist der 2. Punkt doch schon etwas schwierigen.

Diese Software wurde mit Hilfe von Testszenarios auf ihre Korrektheit überprüft, ein weiter möglicher Ausblick soll auf das Theorem der Software Verifikation gegeben werden. Auf diesem Punkt wird die Dissertation basieren.

Die ganze Software wurde mit Hilfe von Unit- und Szenariotests überprüft und somit sollte sichergestellt sein, dass sie einwandfrei funktioniert.

In den RSA-Unittests wurden jeweils Zufallsstrings variabler Länge erzeugt und diese dann ver- bzw. entschlüsselt und signaturüberprüft. In XML-Unittests wurden jeweils verschiedene xml-Dateien erzeugt und dann von der Software eingelesen um vor allem das Verhalten das Programms bei nicht «well-formed» xml-Tags zu testen.⁹

Bei den Szeanriotests wurden probeweise Wahlen mit Wahldaten erzeugt, die vor allem sämtliche möglichen Zustände im Wahlsystem abbilden sollten. Dann wurde die fertige Software herangezogen und mit diesen Daten gefüllt. Auf Grund dieser Testwahlen wurde die richtige Funktionalität der Software überprüft.

Im Normalfall sollte somit gewährleistet sein, dass die Software problemlos funktioniert jedoch kann man mit Testen alleine nie 100% sicher sein. Hier setzt das Konzept der Software Verifikation, welches im Folgenden dargestellt werden soll, an.

Die Methoden der Software Verifikation setzen auf einen anderen Weg. Der Begriff Verifikation bedeutet, dass die Software eindeutig beschrieben wird und dass die Anforderungen eindeutig erfüllt werden. Anders als bei einem normalen Test wird das Programm bzw. sämtliche Programmzustände formal (mathematisch) beschrieben. Das Programm wird damit in Zustandspfade aufgeteilt. Alle Fehlerzustände sollen damit aufgedeckt und somit ein richtiger Programmablauf gewährleistet werden.¹⁰

Gerade bei komplexen Programmen ist die richtige Verifikation einer Software aber sehr schwierig und vor allem ökonomisch teuer, daher wird es meist nur in sicherheitsrelevanten Bereichen oder bei hohen Entwicklungskosten angewendet.

Ein besonders Ereignis war 1994 der Intel Fließkomma Bug, bei dem der Pentium Prozessor bei einigen Divisionen die letzten Kommastellen falsch berechnet hat.¹¹ Mit Hilfe von Software Verifikation hätte dieser Fehler vermieden werden können.

Untenstehend soll anhand eines einfachen Beispiels die Funktionsweise von Software Verifikation vorgeführt werden.

Den Ausgangspunkt stellt die Erzeugung 2er Zufallszahlen, die jeweils die Zuständex= 0 oderx = 1 bzw.y = 0 odery = 1 odery = 2 abbilden. Dann soll die Formel:x/(y+x-2) berechnet werden.¹²

Würde man jetzt die Software gewöhnlich testen so könnte man ausgehend von einem Inputset {x,y} jeweils immer nur einen möglichen Pfad abgehen. Das heißt es könnte also passieren, wenn man das obige Beispiel 2 mal durchlaufen lässt und jeweils die Inputsets {0,0} bzw. {1,0} erhält (die Zahlen werden ausschließlich zufällig erzeugt) nicht auf die fehlerhaften Zustände mit den Inputsets{0,2} und{1,1} kommt.

Natürlich kann bei diesem einfach Beispiel argumentieren, dass wenn man das Programm oft genug testet mit einer hohen Wahrscheinlichkeit alle möglichen Ergebnisse erhalten kann. Was aber passiert wenn x und y jeweils 100 Werte annehmen können?

Bei der Verifikation werden alle Programmzustände erforscht und somit in einem Lauf alle möglichen Zustände erkannt. Damit können auch bei höheren Werten alle möglichen Fehlerzustände erkannt werden.

Der Vorteil des Systems liegt in seiner Unabhängigkeit. Egal welches Softwaresystem der Wahlserver verwendet: Es müssen nur die richtigen Interfacestrings erzeugt werden, damit das Auswertungstool die Eingaben versteht.

In der Hoffnung, dass das bereits bestehende Auswertungstool einen weiteren Beitrag zur Transparenz und Nachvollziehbarkeit im Bereich von E-Voting liefert, soll das neue Projekt die restlichen Zweifel über die richtige Auswertung der Stimmen beheben.

Ausgehend von einem «trusted» Inputmaterial soll hierbei über die Methoden der Software Verifikation eine eindeutige Ergebnisdarstellung ermöglicht und somit die Richtigkeit der Ergebnisse von den Wahlservern untermauert werden.

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)
Deutsch, Michael S, Software Verification and Validation, Englewood Cliffs, NJ, S 7. ff. (1982)
o.A., JAVA,www.java.com , aufgerufen: 10.01.2010
o.A., JPF,http://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/random_example , aufgerufen: 08.12.2009
o.A ., OASIS Standards, www.oasis-open.org/specs/index.php#eml5.0 , aufgerufen: 12.01.2010
o.A. , ÖH Wahl wird aufgehoben. In: Standard (Hrsg.),http://derstandard.at/1259280839327/Uni-Wien-OeH-Wahl-wird-aufgehoben , aufgerufen am: 10.01.2010
Prosser, Alexander, E-Voting,www.evoting.at . aufgerufen: 15.01.2010
Prosser, Alexander, Public Verification System (PubVeriS) for eVoting Version 1.0 Interface Definition,www.e-voting.at/countingtool/download/PubVeriS_Interface.pdf aufgerufen am:12.01.2010
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, Alexander, Public Source Counting Tool: Unit Test,www.evoting.at/countingtool/index_unittest.html , aufgerufen 15.01.2009

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