This project explores process composition tools as applied to elections, concentrating particularly on mail-in and Internet voting. This includes exploration of how to compose systems from pre-analyzed process components, how to analyze the vulnerability of these systems to attacks, and how to guarantee that important security properties are ensured for the resulting composed system. The underlying processes represent aspects of national and local elections, their composition produces an election process, and analysis of the composition gives insight into potential errors or attacks on the election.
Elections are human-intensive processes, processes that directly involve humans in important decision-making and coordination activities, including their interactions with hardware and software components. Providing an approach for formally reasoning about human participation extends current security work. The project also breaks new ground by exploring process-based approaches for modeling and defending against attacks.
The project works closely with government agencies at both the national and local levels to provide in-depth realistic evaluation of results.
Election officials in the U.S. can directly employ the results of this work to make U.S. election processes more verifiably secure, simpler, and easier to change as new technologies, laws, and regulations are imposed. Moreover the technologies developed in this project can be used in most human-intensive processes that have critical security concerns.
This work has addressed the need to determine whether or not a process used to carry out an election contains defects or vulnerabilities that could jeopardize the correctness of the results reported, or violate the security of the election or the privacy of voters. Elections are very complicated processes that begin with the creation of criteria for certifying voters, election officials, and devices used, proceeds through voter registration, purchase of equipment, deployment of personnel, performance of the actual balloting process, and concludes with canvassing and recounting when necessary and appropriate. The sheer size and complexity of such a process creates the possibility of undetected defects and vulnerabilities to attacks that may come from insiders or outsiders. The project has shown that some of these defects and vulnerabilities can be detected by the application of analysis approaches applied to rigorously defined, detailed models of election processes. Some of these analysis approaches are extensions of techniques that were originally developed to help improve the quality of software systems. Others involve automation and extensions to safety analysis approaches that have typically been manually applied by industrial and safety engineers. The project has created some example models of key components of actual election processes used in California and has applied prototype tools based upon these software and safety analysis approaches. The project has identified some actual defects and vulnerabilities in these models. Thus this project suggests that creating precise and detailed election process models, and then subjecting them to rigorous analysis, can indeed improve the correctness and security of these process models. Accordingly, the project outcomes suggest a systematic approach to improving the robustness and reliability of actual elections, which are key cornerstones of democracy in the US.
