Information about the course:
Capita Selecta Software Security (Dutch: Capita Selecta Veilige Software (CSVS))
Academic year 2011-2012
Dave Clarke, Wouter Joosen and Frank Piessens
Official syllabus of the course.
Course Contents
This course treats a number of advanced topics in the area of software
security, typically related to software security research tracks pursued in the
DistriNet research group. The course is organized in a number of modules. For
this academic year, the following 3 modules are covered:
- Formal Verification of Software
Lecturer: Bart Jacobs
In this module we teach students the VeriFast
approach for verifying safety properties of single-threaded and
multithreaded imperative programs. We focus on the C language, but the
approach is equally applicable to Java and C#. We show how to build and use
a tool to prove absence of data races, memory leaks, buffer overflows, and
user-specified functional correctness properties. The assignment for
this module consists of verifying the safety of a small internet service
written in C.
Reading material:
Lectures are on the following days: Oct 5, Oct 12, Oct 19 and Oct 26. For the exact location and timing see the official syllabus.
- Hands-on hacking
Lecturer: Nick Nikiforakis
Despite the advances of the last 20 years in the field of computer security applications still get exploited
and systems still get compromised. Code injection is one of the most notorious problems in computer security and the
code injection attack incidents of last couple of years (e.g., Adobe Reader and Microsoft Internet Explorer) attest
that the problem is far from solved. While the theory behind code injection attacks and countermeasures was covered in
the Secure Software Development course (OVS), this module will take a practical, hands-on approach.
Students will be taught about the basics of code injection attacks, understand their mechanisms and see how they work
in practice by looking at example attacks, and by developing attacks themselves. They will also learn about the evolution
of code injection countermeasures and how hackers have adapted their techniques in order to overcome them.
Subjects that will be covered (among others): stack and heap-based buffer overflows, format string vulnerabilities,
non-control data attacks and return-to-libc attacks.
Course Materials:
- Some chapters of: "Hacking: the art of exploitation, 2nd Edition" (Jon Erickson).
Reading material:
Lectures are on the following days: Nov 9, Nov 16, Nov 23 and Nov 30. For the exact location and timing see the official syllabus.
- Logical Methods in Security
Lecturer: Dave Clarke
Rigourous approaches to software security require formal evidence that a system guarantees the desired security properties. Logical methods
offer a variety of approaches for providing such evidence via techniques such as modal logic, type systems and model checking.
Logical methods can provide clear semantics of security mechanisms and policies and what they entail. Topics covered in this module include
logics for reasoning about information flow, access control, dynamic policy enforcement, and anonimity.
Course Materials:
Additional material of interest:
Lectures are on the following days: Feb 22, Feb 29 and Mar 7. For the exact location and timing see the official syllabus.
Each module consists of 3-4 lectures, and a practical assignment. Students
are expected to prepare in advance for each module by reading the provided
literature.
Calendar
See the syllabus of the course.
Evaluation
Each module has its own evaluation, consisting of a combination of (1)
questions about the lectures, (2) grading of the practical assignment.