Organizers:
- David Basin (ETH Zurich, Switzerland)
- Jannik Dreier (ETH Zurich, Switzerland)
- Carsten Schuermann (IT University of Copenhagen, Denmark)
Invited guest speaker:
- Achim Brucker (SAP AG, Germany)
ECTS: 5
This course is intended for PhD students and advanced Master students and it is designed to give an introduction to formal methods, teach the basics of code scanning theory, and allows students to gain first-hand experience with the state of the art code scanners. Code scanners are tools that inspect source code automatically for bugs, security problems and other issues. Code scanners are often used to evaluate software used in safety critical systems. Contingent on our ability to secure licenses, we will discuss five different tools, such as Coverity, Fortify, Code Sonar, AppScan, and FindBugs.
The course is organized in two parts. The first part takes place in April, where we (the organizers) will give several lectures about the formal under pinnings of code scanners. During the last lecture, we, will present some sample code, and assign (groups of) students to tools. The dates for the first part are
- April 7, 9-12 Introduction to code scanning. David Basin, 2A50
- 8, 9-12 Foundations. Carsten Schuermann, 5E10
- 9, 13-16 Case studies and tools. Jannik Dreier, 2A50
The second part of the course is then going to be tutorial like presentations of the PhD students who take the course for credit.
- May 19, 10-12 Invited lectures. Achim Brucker, 3A08
- May 20, 10-12 Presentation, Group 1, 3A08
- May 21, 10-12 Presentation, Group 2. 3A20/28
DEADLINE for the final report. May 16, 2014.
To sign up for this course, please send email to Christina Rasmussen (crasm@itu.dk)
Details
Recommended literature
- Chess, West, "Secure Programming with Static Analysis", Person 2007.
- Tsipenyuk, Chess, "Seven Pernicious Kingdoms: A Taxonomy of Software Security Errors", IEEE S&P, 2005.
- Bessey et. al., "A Few Billion Lines of Code Later, Using Static Analysis to Find Bugs in the Real World", CACM 2010.
- Musuvathi et. al., "CMC: A Pragmatic Approach to Model Checking Real Code", Usenix 2002.
- "Dependence Graphs and Program Slicing", CodeSurfer? Technology Overview.
- Young, Horwitz, "Protecting C Prorams from Attacks via Invalid Pointer Dereference", ESEC/FSE 2003.
- Young, Horwitz, Reps, "Pointer Analysis for Programs with Structures and Casting", PLDI 1999.
- Reps, "Program Analysis via Graph Reachability", Technical Report.
- Hovemeyer, Pugh, "Finding Bugs is Easy", OOPSLA 2004.
- Wyewah et. al., "Using Static Analysis to Find Bugs", IEEE Software 2008.
Case Studies
Norwegian Internet Voting Protocol
- Homepage
- Technical Documentation
- Official Source Code
- Building instructions:
- Download code.tar.gz and extract to /home/user/code/, and extract repository.tar.gz to /home/user/.repository
- To build, execute
mvn clean install -U -o -DskipTests -Dmaven.repo.local=/home/user/.repository
in each sub-directory of /home/user/code, in the following order:
- parent-config, jbasis-parent, cryptography, protocol, secure-logger, auditing, vsframework, authentication, evoting, counting
Literature:
- Kristian Gjøsteen. The Norwegian Internet Voting Protocol. Cryptology ePrint Archive, Report 2013/473. http://eprint.iacr.org/, 2013.
- Ida Sofie Gebhardt Stenerud and Christian Bull. When Reality Comes Knocking Norwegian Experiences with Verifiable Electronic Voting. In 5th International Conference on Electronic Voting 2012 (EVOTE 2012). LNI, 205. GI, 2012.
- Jordi Barrat, Michel Chevalier, Ben Goldsmith, David Jandura, John Turner and Rakesh Sharma. Internet Voting and Individual Verifiability: The Norwegian Return Codes. In 5th International Conference on Electronic Voting 2012 (EVOTE 2012). LNI, 205. GI, 2012.
- Jordi Puigalli and Sandra Guasch. Cast-as-Intended Verification in Norway. In 5th International Conference on Electronic Voting 2012 (EVOTE 2012). LNI, 205. GI, 2012.
- Denise Demirel, Hugo Jonker and Melanie Volkamer. Random Block Verification: Improving the Norwegian Electoral Mix-Net. In 5th International Conference on Electronic Voting 2012 (EVOTE 2012). LNI, 205. GI, 2012.
- Oliver Spycher, Melanie Volkamer, Reto E. Koenig. Transparency and Technical Measures to Establish Trust in Norwegian Internet Voting. In E-Voting and Identity - Third International Conference (VoteID 2011). Volume 7187 of LNCS, Springer, 2012.
- Jordi Puiggalí Allepuz, Sandra Guasch Castelló. Internet Voting System with Cast as Intended Verification. In E-Voting and Identity - Third International Conference (VoteID 2011). Volume 7187 of LNCS, Springer, 2012.
- R. Koenig, P. Locher, R. Haenni. Attacking the Verification Code Mechanism in the Norwegian Internet Voting System. In VoteID'13, 4rd International Conference on E-Voting and Identity. Guildford, U.K., 2013
- Véronique Cortier and Cyrille Wiedling. A formal analysis of the Norwegian E-voting protocol. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), pp. 109–128, Lecture Notes in Computer Science 7215, Springer, Tallinn, Estonia, March 2012.
Verificatum Mixnet
