Abstract
We present a case-study in which vote-tallying software is analyzed using a bounded verification technique, whereby all executions of a procedure are exhaustively examined within a finite space given by a bound on the size of the heap and the number of loop unrollings. The technique involves an encoding of the procedure in an intermediate relational programming language, a translation of that language to relational logic, and an analysis of the logic that exploits recent advances in finite model-finding. Our technique yields concrete counterexamples – traces of the procedure that violate the specification.
The vote-tallying software, used for public elections in the Netherlands, had previously been annotated with specifications in the Java Modeling Language and analyzed with ESC/Java2. Our analysis found counterexamples to the JML contracts, indicating bugs in the code and errors in the specifications that evaded prior analysis.
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.
References
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: PLDI 2002, pp. 234–245 (June 2002)
Leavens, G., et al.: Java Modeling Language, http://www.jmlspecs.org
Jacobs, B.: Counting votes with formal methods. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116. Springer, Heidelberg (2004)
Fairmichael, F.: Full verification of the KOA tally system University College Dublin. Bachelor’s Thesis (March 2005)
Kiniry, J., Morkan, A., Cochran, D., Fairmichael, F., Chalin, P., Oostdijk, M., Hubbers, E.: The KOA remote voting system: A summary of work to date. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661. Springer, Heidelberg (2007)
Kiniry, J.: Formally counting electronic votes (but still only trusting paper). In: ICECCS 2007, pp. 261–269 (July 2007)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231–255. Springer, Heidelberg (2002)
Dennis, G., Yessenov, K.: Forge website, http://sdg.csail.mit.edu/forge/
Vaziri, M.: Finding Bugs in Software with a Constraint Solver. PhD thesis. MIT (February 2004)
Taghdiri, M.: Inferring Specifications to Detect Errors in Code. In: 19th Int. Conf. on Automated Software Engineering (ASE 2004), Linz, Austria(September 2004)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating Small Scope Hypothesis (2003) (MIT CSAIL unpublished manuscript)
Dennis, G., Chang, F.S.H., Jackson, D.: Modular verification of code with SAT. In: ISSTA 2006, Portland, Maine (July 2006)
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424. Springer, Heidelberg (2007)
Jackson, D.: Object models as heap invariants. Essays on Programming Methodology, 247–268 (2000)
Morgan, C.: The specification statement. In: ACM Trans. Program. Lang. Syst, vol. 10, pp. 403–419. ACM Press, New York (1988)
Morgan, C.: Programming from Specifications. Prentice Hall International (UK) Ltd., Hertfordshire (1994)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Kiniry, J.R., Morkan, A.E., Denby, B.: Soundness and completeness warnings in ESC/Java2. In: SAVCBS 2006, New York, pp. 19–24 (2006)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)
Deng, X., Lee, J., Robby,: Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, Washington, DC, pp. 157–166. IEEE Computer Society, Los Alamitos (2006)
Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: Biryukov, A. (ed.) FSE 2007. LNCS, vol. 4593. Springer, Heidelberg (2007)
Frias, M., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Inverardi, P., Jazayeri, M. (eds.) ICSE 2005. LNCS, vol. 4309, pp. 442–451. Springer, Heidelberg (2006)
Dewer, R.: The SETL Programming Language (1979)
Beyer, D.: Relational programming with Crocopat. In: Proceedings of the 28th International Conference on Software Engineering (May 2006)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dennis, G., Yessenov, K., Jackson, D. (2008). Bounded Verification of Voting Software. In: Shankar, N., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2008. Lecture Notes in Computer Science, vol 5295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87873-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-87873-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87872-8
Online ISBN: 978-3-540-87873-5
eBook Packages: Computer ScienceComputer Science (R0)