Sådan hjælper du udviklingen af open source valg-software

Vil du gerne give Danmark - og resten af kloden - sikker software, man kan stole på til parlamentsvalg? Se, hvad Demtech-folkene arbejder på og ønsker din hjælp til.

Kan du kode eller på anden måde udvikle software, og er du villig til at bruge noget fritid på at hjælpe Demtech-projektet med at få skabt verdens sikreste og bedste software til at afholde valg?

Så skal du ikke holde dig tilbage, lyder det fra Joseph Kiniry, professor på DTU og en del af Demtech-forskergruppen. Han vil gerne have hjælp til de ni projekter, som Demtech og en gruppe studerende i dag arbejder på at få gjort færdige.

Læs også: Hjælp forskerne med at gøre dansk valg-software open source

Rent praktisk er alle projekterne lagt på kodetjenesten Github, hvor bidragydere er velkomne til at kigge ind og se, hvad det drejer sig om. Kommunikationen sker via en Google-gruppe (e-mail: demtech-developers@googlegroups.com). Man må gerne sende en e-mail til Joseph Kiniry først og fortælle, hvad man kan og ønsker at arbejde med, men man kan også bare gå i gang.

»Normalt har jeg lige en chat eller lignende med folk, så vi kan finde ud af, hvad der interesserer dem og engagerer dem. Men det er ikke et krav at skrive først,« siger professoren.

De ni software-projekter har enten en liste over opgaver i Github eller en fil med en to do-liste, man kan kigge på og finde opgaver i. Det vigtigste system at få bragt videre lige nu er ’DVL’ (Digital Voter Lists), altså software til at registrere folk, når de ankommer på valgstedet.

»DVL har mest brug for hjælp lige nu, for kommunerne vil gerne bruge det til næste valg. Her er buglister, man bare kan gå i gang med,« siger Joseph Kiniry.

Han håber, at et dusin eller to blandt Version2’s læsere vil være med i dette open source-projekt, der potentielt kan give mere gennemskuelige og sikre valg i mange lande kloden rundt.

Mærkeligt i starten - men mange fordele

Da kravene til valg-software er meget høje, bliver kodearbejdet også styret helt efter principper for højest mulig sikkerhed. Det er måske lidt anderledes, end hvad folk er vant til, mener Joseph Kiniry, men omvendt kan det også være en lærerig oplevelse at være med til.

»Er man interesseret i at lære om sikkerhedskritisk softwareudvikling, eller vil man som udvikler gerne lære om nye, avancerede værktøjer og teknikker til at kode i bedre kvalitet, med en mindre indsats, vil det være interessant, hvordan vi gør det. For eksempel skriver vi kodespecifikationer med kontrakter for metoder og klasser,« siger Joseph Kiniry.

Kontrakterne for klasserne bestemmer, at konstanter skal være valide i forhold til klasser og objekter, også for subtypes. Kontrakter for metoderne bestemmer kravene til både kaldet og til implementeringen, uddyber han.

»At skrive specifikationer på den måde er en meget anderledes måde at gøre det på. Det virker mærkeligt i starten, men hurtigt bliver det en teknik, du ikke kan leve uden. Når du skriver specifikationerne på denne måde, skal du skrive mindre dokumentation, du får mindre kode, og du fokuserer kun på opgaven, ikke på håndtering af fejl, undtagelser og den slags. Du kan også lave automatiske unit-test,« forklarer Joseph Kiniry.

For en uddybning af principperne henviser han til en forelæsning, han har holdt for studerende engang (video-optagelse samt præsentation)

Du kan se et eksempel på kode nederst i artiklen.

Her er sprogene og værktøjerne

Herunder kan du se Joseph Kinirys engelsksprogede beskrivelse af værktøjerne, der bliver brugt, og af de ni softwareprojekter:

In general, much of our R&D focuses on formal specification and verification of evoting cryptography, protocols, and systems. Thus, while we do use mainstream languages for some of our development (mainly Java and C#, and thus are working on JVM and .Net foundations), we also use non-mainstream programming and specification languages, validation and verification tools, logical frameworks, and theorem provers.
Here is the laundry list of technologies current in use to give a flavor for the kinds of tools and foundations we choose to use for mission-critical development:
For Domain Analysis; Requirements; High-level Design; Detailed, Formal, Language-neutral Design; and Architecture Specification: EBON: The Extended BON Specification Language (http://bon-method.com/), supported by tools like BONc, Beetlz, Visio, and OmniGraffle. BON is kind of like the core of UML that makes sense without all of the cruft and it has both a visual and a textual notation. It also includes contracts as a first-order construct.
For Java Software Development:
Much is done within the Mobius Program Verification Environment, an augmented version of Eclipse that includes several static analysis tools (customized versions of CheckStyle, PMD, FindBugs, etc.), extended static checking tools (namely, ESC/Java2), the Java Modeling Language (JML) tools for writing formal specifications used for documentation, runtime assertion checking, test generation, and verification (e.g., JML2 and OpenJML), unit test generation tools (JMLunitNG), the AutoGrader, EclEmma for coverage analysis, SLOCCOUNT and Metric plugins for code complexity analysis, and much more.
For C# Software Development:
Much is done within a similarly-extended version of Visual Studio Ultimate Edition, augmented by several add-ons including Code Contracts (just like JML for .Net), PEX (unit test generation), NUnit, NDepend, ReSharper (and several other tools from JetBrains), StyleCop, FxCop, and much more.
Other languages used include Haskell, Scala, F*, OCaml, Twelf, PVS, Alloy, SMT, Coq, etc.
Information about all of these software tools is available via DemTech's GitHub Organization and my research group's website (KindSoftware).
There are nine DemTech R&D projects on GitHub today. Here is their brief summary:
1. VoteTEC - A prototype kiosk voting system based upon the idea of trace-emitting computation, as described in the paper "Linear Logical Voting Protocols" by Henry deYoung and Carsten Schürmann. VoteTEC is written in Java by Eric Cederstrand and Carsten and the formalized foundations are written in Twelf (http://twelf.org/).
2. DVL - A prototype Digital Voter List system which generates ballots and voter cards, helps election volunteers check in voters on election day, and report on election participation rates. It is a distributed system, uses crypto, and there are four or five prototype systems. The DVL is formally specified in EBON and Code Contracts.
3. Votail - A verified implementation of Ireland's PR-STV tally system. It is written in Java and formally specified using EBON and JML.
4. Evoting-Systems - A snapshot of several other evoting systems developed around the world. We analyze other groups' systems for correctness and security flaws and to learn best- and worst-practices.
5. Logging - A verified logging system (like log4j) that is being tuned for elections. It is formally specified and verified using EBON, JML, and uses interval logics.
6. V4 - A verified, voter-verifiable, verified election scheme VVPAT device. This system is developed using 3D printing, custom Arduino boards, and is implemented in Java and C.
7. Uilioch - An election generator for generating system tests for different electoral schemes. Electoral schemes are formally specified using Alloy from MIT and the software that does the test generation is written in Java and uses model checking/model finding.
8. DiVS - A (mostly) verified implementation of (nearly all of) Denmark's electoral system. This system is meant to, someday, replace the currently-secret system development by Danish Statistics used to tally elections in Denmark. It is written in Java and formally specified using EBON and JML.
9. Crypto-Agda - A formalization of cryptography foundations for the Agda programming language. This system pushes crypto and programming with dependent types to the limit.

Et eksempel på, hvordan softwaren hos Demtech skal kodes med specifikationer for klasser og metoder. Denne kodestump skal indsamle oplysninger om en persons civilstand og familieforhold:

 //@ invariant (spouse != null) ==>
 //@ spouse.spouse == this;
 Citizen spouse() { return spouse; }
 boolean single() { return spouse == null; }
 //@ requires single();
 //@ ensures !single();
 //@ ensures spouse() == new_spouse;
 void marry(@NonNull Citizen new_spouse)
 { spouse = new_spouse;
 new_spouse.spouse = this; }
 //@ requires !single();
 //@ ensures single() & \old(spouse()).single();
 void divorce() { spouse.spouse = null;
 spouse = null; }
Citizen spouse;
 //@ invariant (spouse != null) ==>
 //@ spouse.spouse == this;
 Citizen spouse() { return spouse; }
 boolean single() { return spouse == null; }
 //@ requires single();
 //@ ensures !single() && spouse() == new_spouse;
 void marry(@Nullable /*@ nullable */ Citizen new_spouse)
 { spouse = new_spouse;
 new_spouse.spouse = this; }
 //@ requires !single() & spouse() != null;
 //@ ensures single() & \old(spouse()).single();
 void divorce() { spouse.spouse = null;
 spouse = null; }

Tips og korrekturforslag til denne historie sendes til tip@version2.dk
Kommentarer (3)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Log ind eller Opret konto for at kommentere