Abstract
Voting is a critical component of any democratic process; and electronic voting systems should be developed following best practices for critical system development. E-voting has illustrated the importance of formal software engineering in the development of complex systems: poorly engineered and poorly documented voting systems have had serious negative consequences for all system stakeholders. It is clear that the formal verification of e-voting system models would help to address problems associated with certification against standards, and would improve the trustworthiness of the final systems. However, it is not yet clear how best to carry out such formal modelling and verification in order to leverage the compositional nature of the problem, and manage the complexity of the task.
The choice of modelling language - for expressing the high level design and architecture of an e-voting system - poses many problems due to the complex mix of requirements that such a system is required to meet. Different modelling languages are more-or-less suited to the verification of different critical requirements. Thus, we report on a mixed model approach: where we address 3 different types of critical requirements using 3 different modelling languages and development strategies. Firstly, we report on network quality-of-service issues that are analyzed through simulation models. Secondly, we report on functional correctness of a counting process that can be validated through algebraic techniques. Finally, we report on the use of formal refinement to reason about the correctness of design steps when adding detail to an architecture model. To conclude, we acknowledge the main problem that arises from such a mixed-model approach to architecture verification: how can we be sure that the different models are coherent when we integrate them in a final implementation?
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R., Butler, M.J., Hallerstede, S., Voisin, L.: An open extensible tool environment for event-b. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Anane, R., Freeland, R., Theodoropoulos, G.: E-voting requirements and implementation. In: The 9th IEEE International Conference on E-Commerce Technology and the 4th IEEE International Conference on Enterprise Computing, E-Commerce, and E-Services. CEC/EEE, Tokyo, Japan, July 2007, pp. 382–392 (2007)
Braun, N., Brändli, D.: Swiss e-voting pilot projects: Evaluation, situation analysis and how to proceed. In: Krimmer [20], pp. 27–36
Bryans, J.W., Littlewood, B., Ryan, P.Y.A., Strigini, L.: E-voting: Dependability requirements and design for dependability. In: ARES 2006: Proceedings of the First International Conference on Availability, Reliability and Security, Washington, DC, USA, pp. 988–995. IEEE Computer Society Press, Los Alamitos (2006)
Cansell, D., Gibson, J.P., Méry, D.: Formal verification of tamper-evident storage for e-voting. In: Hinchey, M., Margaria, T. (eds.) Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, England, UK, pp. 329–338. IEEE Computer Society Press, Los Alamitos (2007)
Cansell, D., Gibson, J.P., Méry, D.: Refinement: A constructive approach to formal software design for a secure e-voting interface. Electronic Notes in Theoretical Computer Science 183, 39–55 (2007)
Carew, D., Exton, C., Buckley, J., McGaley, M., Gibson, J.P.: Preliminary study to empirically investigate the comprehensibility of requirements specifications. In: Romero, P., Good, J., Acosta Chaparro, E., Bryant, S. (eds.) Psychology of Programming Interest Group 17th annual workshop (PPIG 2005), pp. 182–202. University of Sussex, Brighton (2005)
Chaum, D., van der Graaf, J., Ryan, P.Y.A., Vora, P.: Secret ballot elections with unconditional integrity. Report CS-TR-1058, Department of Computing Science, University of Newcastle upon Tyne (2007)
Chen, Y.-Y., Jan, J.k., Chen, C.-L.: The design of a secure anonymous internet voting system. Computers & Security 23(4), 330–337 (2004)
Clarkson, M.E., Chong, S., Myers, A.C.: Civitas: A secure remote voting system. In: Chaum, D., Kutylowski, M., Rivest, R.L., Ryan, P.Y.A. (eds.) Frontiers of Electronic Voting. Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), vol. 07311, Schloss Dagstuhl, Germany (2007)
Gibson, J.P.: Formal Object Oriented Development of Software Systems Using LOTOS. Thesis CSM-114, Stirling University (August 1993)
Gibson, J.P.: E-voting requirements modelling: An algebraic specification approach (with cafeobj). Report NUIM-CS-TR-2005-14, Department of Computer Science, National University of Ireland, Maynooth (2005)
Gibson, J.P., Lallet, E., Raffy, J.-L.: Analysis of a distributed e-voting system architecture against quality of service requirements. In: The Third International Conference on Software Engineering Advances (ICSEA 2008), pp. 58–64. IEEE Computer Society Press, Los Alamitos (2008)
Gibson, J.P., Lallet, E., Raffy, J.-L.: Feature interactions in a software product line for e-voting. In: Nakamura, Reiff-Marganiec (eds.) Feature Interactions in Software and Communication Systems X, Lisbon, Portugal, June 2009, pp. 91–106. IOS Press, Amsterdam (2009)
Gibson, J.P., McGaley, M.: Verification and maintenance of e-voting systems and standards. In: Remenyi, D. (ed.) 8th European Conference on e-Government, Lausanne, Switzerland, July 2008, pp. 283–289. Academic Publishing International (2008)
Hoffman, L.J.: Internet voting: will it spur or corrupt democracy? In: CFP 2000: Proceedings of the tenth conference on Computers, freedom and privacy, pp. 219–223. ACM, New York (2000)
ISO/IEC. Estelle: A formal description technique based on an extended state transition model. Technical Report ISO 9074, Information technology - Open Systems Interconnection (1997)
Jefferson, D., Rubin, A.D., Simons, B., Wagner, D.: Analyzing internet voting security. ACM Commun. 47(10), 59–64 (2004)
Joaquim, R., Zuquete, A., Ferreira, P.: REVS — A Robust Electronic Voting System. In: Proceedings of the IADIS International Conference on e-Society, Lisbon, Portugal, June 2003, pp. 95–103 (2003)
Krimmer, R. (ed.): Electronic Voting 2006: 2nd International Workshop, Co-organized by Council of Europe, ESF TED, IFIP WG 8.6 and E-Voting.CC, Castle Hofen, Bregenz, Austria, August 2-4. LNI, vol. 86. GI (2006)
Krimmer, R., Triessnig, S., Volkamer, M.: The development of remote e-voting around the world: A review of roads and directions. In: Alkassar, A., Volkamer, M. (eds.) VOTE-ID 2007. LNCS, vol. 4896, pp. 1–15. Springer, Heidelberg (2007)
Maaten, E.: Towards remote e-voting: Estonian case. In: Prosser, A., Krimmer, R. (eds.) Electronic Voting in Europe. LNI, vol. 47, pp. 83–100. GI (2004)
Madise, Ü., Martens, T.: E-voting in estonia 2005. the first practice of country-wide binding internet voting in the world. In: Krimmer [20], pp. 15–26 (2005)
McGaley, M., Gibson, J.P.: E-voting: a safety critical system. Report NUIM-CS-TR-2003-2, Department of Computer Science, National University of Ireland, Maynooth (2003)
McGaley, M., Gibson, J.P.: A critical analysis of the council of europe recommendations on e-voting. In: EVT 2006: Proceedings of the USENIX/Accurate Electronic Voting Technology Workshop 2006 on Electronic Voting Technology Workshop, pp. 9–22. USENIX Association (2006)
Mills, D.L.: Internet time synchronization: the network time protocol. IEEE Transactions on Communications 39(10), 1482–1493 (1991)
Qadah, G.Z., Taha, R.: Electronic voting systems: Requirements, design, and implementation. Comput. Stand. Interfaces 29(3), 376–386 (2007)
Roth, S.K.: Disenfranchised by design: voting systems and the election process. Information Design Journal 9(1), 1–8 (1998)
Rubin, A.D.: Security considerations for remote electronic voting. ACM Commun. 45(12), 39–44 (2002)
Sandler, D.R., Wallach, D.S.: The case for networked remote voting precincts. In: EVT 2008: Proceedings of the USENIX/Accurate Electronic Voting Technology Workshop 2008 on Electronic Voting Technology Workshop, Berkeley, CA, USA, July 2008. USENIX Association (2008)
Selker, T., Goler, J.: The save system — secure architecture for voting electronically. BT Technology Journal 22(4), 89–95 (2004)
Sterzbach, B.: Gps-based clock synchronization in a mobile, distributed real-time system. Real-Time Syst. 12(1), 63–75 (1997)
Storer, T., Duncan, I.: Practical remote electronic elections for the uk. In: PST, pp. 41–45 (2004)
Tappenden, A., Beatty, P., Miller, J.: Agile security testing of web-based systems via httpunit. In: ADC 2005: Proceedings of the Agile Development Conference, Washington, DC, USA, pp. 29–38. IEEE Computer Society Press, Los Alamitos (2005)
Weibel, H., Béchaz, D.: IEEE1588 Implementation and Performance of Time Stamping Techniques. In: Conference on IEEE 1588, Gaithersburg (september 2004)
Zúquete, A., Almeida, F.: Verifiable anonymous vote submission. In: SAC 2008: Proceedings of the 2008 ACM symposium on Applied computing, pp. 2159–2166. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gibson, J.P., Lallet, E., Raffy, JL. (2010). Engineering a Distributed e-Voting System Architecture: Meeting Critical Requirements. In: Giese, H. (eds) Architecting Critical Systems. ISARCS 2010. Lecture Notes in Computer Science, vol 6150. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13556-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-13556-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13555-2
Online ISBN: 978-3-642-13556-9
eBook Packages: Computer ScienceComputer Science (R0)