On March 29, 30, and 31, 2007, a team of computer security researchers met for three full days at UC Berkeley to conduct a review of Pvote. On May 20, two reviewers met again to review Pvote. The subject of the review was:
- The Pvote Software Review Assurance Document, which describes the design and implementation of Pvote and sets out its security responsibilities, assumptions, and correctness claims.
- The source code for Pvote 1.0 beta, which is supposed to meet the claims made in the assurance document.
The reviewers were:
- Matt Bishop, professor, UC Davis (present March 29, 30)
- Ian Goldberg, professor, University of Waterloo (present May 20)
- Tadayoshi Kohno, professor, University of Washington (present March 31 and May 20)
- Mark Miller, primary designer and author of the E language (present March 29, 30, 31)
- Dan Sandler, graduate student, Rice University (present March 29, 30, 31)
- Dan Wallach, professor, Rice University (present March 29, 30)
David Wagner and I were on hand to explain Pvote's design and implementation, answer the reviewers' questions, and provide them any assistance they requested in their investigation.
The findings of the review are described in detail in the Report on the Pvote security review.
Bug injection
Between the second and third days, David Wagner and I inserted three bugs into Pvote to motivate the reviewers and gauge the effectiveness of the review. The bugs were chosen to enable an attack on the election if deployed in conjunction with maliciously designed ballot definition files. We expected the first bug to be easy to find, the second bug to be moderate, and the third bug to be hard to find.
At the beginning of the third day, we announced that there was at least one bug in Navigator.py. We chose this file because it was the most complex and most central to the functioning of Pvote. As we had hoped, our announcement motivated them to subject the file to intense scrutiny.
The reviewers found the first two of the three inserted bugs. Despite being told the 60-line region of the code containing all the inserted bugs, they did not find the third inserted bug. And, despite their focused attention, they did not discover any bugs in the original code.
Results
The reviewers did not find any bugs in the source code to Pvote 1.0 beta.
The reviewers found one error in the assurance document. One of the security responsibilities stated in the document is that Pvote must "commit the ballot when and only when so requested by the voter" (referred to as R9).
However, by design, a Pvote ballot definition can cause a page transition to occur automatically after a specified time has passed with no response from the user. Because a transition to the last page commits the ballot, an automatic "timeout transition" to the last page will commit the ballot without explicit voter action, contrary to R9. Therefore, the ballot definition file needs to be checked to ensure that no timeout transition arrives at the last page. The assurance document describes several ballot definition checks that need to be performed to ensure R9 (see section 7.11), but failed to mention the need to check for timeout transitions.
zesty
ca.