Poster : Security in E-Voting

In this work, we consider the verification of security properties of Java programs that use cryptographic operations. Our motivating objective is to provide cryptographic guarantees on the code level for a Java implementation of a realistic, usable electronic-voting system, called sElect1. While tools for verification of Java programs are available, including tools for checking noninterference properties, they cannot deal with cryptography: guarantees for cryptographic primitives are based complexity arguments and therefore these primitives do not provide absolute security against unbounded adversaries (which is the adversary model employed in these tools). In our work, we propose a framework that allows the existing tools for checking noninterference to verify cryptographic properties, such as cryptographic indistinguishability, of Java programs. We applied our framework to several case studies, using the Joana and KeY tools. The integration of these tools in our framework led to interesting insights and motivated us to improve the existing techniques and develop new techniques for proving noninterference.