Free & Fair is committed to releasing all our products, research, development, and proposals under open source licenses.  Our primary focus is creating open source, high assurance election systems that are great for our customers.  Our secondary focus is helping others create high assurance election systems using the concepts, tools, and techniques within our research field.

As such, today, on Wednesday, 17 May 2017, we are opening to the public more than 30 repositories in our Free & Fair GitHub Organization.  These repositories contain the product demonstrators, security audits, proposals, tools, and technologies that we use to create high assurance election systems, some of which have been under development since the late 1990s.

Some Highlights.  We’d like to shine a brighter light on a few of these repositories.  Here are some key projects that we think the community and our clients will be excited about.  Nearly all of these systems were implemented using our rigorous engineering methodology and use applied formal methods to provide assurance that the systems do exactly as they promise and are secure. We have used a whole host of technologies, including several programming languages and a handful of deployment platforms, to demonstrate the breadth of our capabilities, the flexibility of our methodology, and the myriad of ways one can provide assurance about a system’s correctness and security.

  • STAR-Vote: A demonstration Haskell implementation of the entire STAR-Vote system, as described in the original STAR-Vote journal paper.  This implementation is interesting due to our use of Haskell’s rich type system to characterize the system’s correct behavior.  Moreover, because Haskell is so expressive, our implementation is a fraction of the size of Rice’s open source Java implementation of STAR-Vote.
  • DVL: Several demonstration implementations in C# of an Electronic Poll Book.  This system is interesting in part because (i) the architecture specifications of the systems are largely similar across different, independent implementations, and (ii) all of the system’s behavior is characterized using Microsoft’s Code Contracts specification framework and tools.
  • OpenCount: OpenCount is a system that can interpret scanned paper ballots and interpret them into cast vote records.  It can understand some of the existing proprietary file formats for other vendors’ equipment, and can semi-automatically figure out the shape and nature of a ballot with a little help from an elections official.  OpenCount was originally designed and implemented at Berkeley under the guidance of Prof. David Wagner and we have, with their blessing, improved upon those initial experiments.  OpenCount is written in Python and C.
  • Tabulator: A tabulator capable of counting a set of cast vote records to determine the outcome of either plurality or ranked choice voting elections.  The entire system is formally specified and verified in the Coq theorem prover and our implementation is automatically extracted to Haskell from that theory.  We have also been hand-writing formally verified implementations in the Logika and SPARK programming languages, both of which support formal proofs of correctness.
  • Qubie: Our open hardware privacy-preserving polling place monitor.  Put a Qubie in the corner of your polling place and it will automatically record the flow of voters, permitting election officials to optimize their polling places from election to election.  Early versions of this system were built in Python and C on embedded platforms with parts bought from Amazon.  The third version of this system is under development using our rigorous engineering methodology and is implemented in verifiable C; we have also started design of a custom PCB to reduce Qubie’s unit cost to the point where deploying a Qubie in every polling place in America becomes an affordable and sensible thing to do.
  • Transparency: Our icing on the cake of transparency—every research proposal, RFI response, and RFP response that we have ever written, for all the world to see.

By opening these repositories to the public, we are releasing over a quarter of a million lines of specifications and code—representing more than 15 man years of work by nearly 100 contributors—under standard open source licenses, primarily BSD and GPL.  With this huge step we look forward to working with federal, state, and local election officials, as well as open source contributors and the election integrity community, toward realizing our dream of truly trustworthy elections for all democracies.