Advertisement

Bounded Verification of Voting Software

  • Greg Dennis
  • Kuat Yessenov
  • Daniel Jackson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

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.

Keywords

Unit Testing Relational Logic Symbolic Execution Java Code Java Modeling Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)Google Scholar
  2. 2.
    Leavens, G., et al.: Java Modeling Language, http://www.jmlspecs.org
  3. 3.
    Jacobs, B.: Counting votes with formal methods. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116. Springer, Heidelberg (2004)Google Scholar
  4. 4.
    Fairmichael, F.: Full verification of the KOA tally system University College Dublin. Bachelor’s Thesis (March 2005)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Kiniry, J.: Formally counting electronic votes (but still only trusting paper). In: ICECCS 2007, pp. 261–269 (July 2007)Google Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Dennis, G., Yessenov, K.: Forge website, http://sdg.csail.mit.edu/forge/
  9. 9.
    Vaziri, M.: Finding Bugs in Software with a Constraint Solver. PhD thesis. MIT (February 2004)Google Scholar
  10. 10.
    Taghdiri, M.: Inferring Specifications to Detect Errors in Code. In: 19th Int. Conf. on Automated Software Engineering (ASE 2004), Linz, Austria(September 2004)Google Scholar
  11. 11.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)Google Scholar
  12. 12.
    Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating Small Scope Hypothesis (2003) (MIT CSAIL unpublished manuscript)Google Scholar
  13. 13.
    Dennis, G., Chang, F.S.H., Jackson, D.: Modular verification of code with SAT. In: ISSTA 2006, Portland, Maine (July 2006)Google Scholar
  14. 14.
    Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Jackson, D.: Object models as heap invariants. Essays on Programming Methodology, 247–268 (2000)Google Scholar
  16. 16.
    Morgan, C.: The specification statement. In: ACM Trans. Program. Lang. Syst, vol. 10, pp. 403–419. ACM Press, New York (1988)Google Scholar
  17. 17.
    Morgan, C.: Programming from Specifications. Prentice Hall International (UK) Ltd., Hertfordshire (1994)zbMATHGoogle Scholar
  18. 18.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  19. 19.
    Kiniry, J.R., Morkan, A.E., Denby, B.: Soundness and completeness warnings in ESC/Java2. In: SAVCBS 2006, New York, pp. 19–24 (2006)Google Scholar
  20. 20.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)Google Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    Dewer, R.: The SETL Programming Language (1979)Google Scholar
  25. 25.
    Beyer, D.: Relational programming with Crocopat. In: Proceedings of the 28th International Conference on Software Engineering (May 2006)Google Scholar
  26. 26.
    DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Greg Dennis
    • 1
  • Kuat Yessenov
    • 1
  • Daniel Jackson
    • 1
  1. 1.Computer Science and Artificial Intelligence LaboratoryMassachusetts Institute of TechnologyCambridgeUSA

Personalised recommendations