Secure and Dependable Systems (Spring 2018)
Course: Secure and Dependable Systems (CO21-320203)
Instructor: Jürgen Schönwälder
TA: Yufei Liu, Orgest Xhelili
Monday 08:15 - 09:30 Lecture Hall Research I
Friday 09:45 - 11:00 Conference Room Research IV
Start: February 2nd, 2018

This course introduces formal methods for analyzing and assuring safety and security of software systems. The course starts off with a clarification of concepts such as dependability, quality, safety, and security of software systems, and how to achieve them in the software development process. We introduce the foundations of cryptography as a basis for security mechanisms. The main part of the course introduces different paradigms of safety/security analysis such as formal testing (code coverage), static program analysis (control/data flow analysis and abstract interpretation), model checking (computational tree logic), and program verification (Hoare calculus, dynamic logic). The formal techniques will be used for analyzing both safety and security properties of programs. Where possible, students will be given hands-on micro-projects in state-of-the-art tools (e.g., Isabelle for program verification).

Course Materials:
Books: TBD
Mon (08:15)Fri (09:45)Topics
2018-02-02 Introduction (Spectre)
2018-02-05 2018-02-09 Dependability Concepts and Classic Computing Disasters
2018-02-12 2018-02-16 Software Engineering and Testing
2018-02-19 2018-02-23 Software Specification and Verification
2018-02-26 2018-03-02 Automated Generation of Proof Goals and Termination Proofs
2018-03-05 2018-03-09 Time, Events, and Causality in Distributed Systems
2018-03-12 2018-03-16 Broadcast Algorithms, Communicating Sequential Processes
2018-03-19 2018-03-23 Communicating Sequential Processes
2018-03-26 2018-03-30 [Spring Break]
2018-04-02 2018-04-06 Midterm Exam (Campus Center Eastwing)
2018-04-09 2018-04-13 Basic Concepts of Cryptography and Symmetric Encryption Algorithms and Block Ciphers
2018-04-16 2018-04-20 Asymmetric Encryption Algorithms, Cryptographic Hash Functions, Certificates
2018-04-23 2018-04-27 Key Management Schemes, Pretty Good Privacy
2018-04-30 2018-05-04 Transport Layer Security and Secure Shell
2018-05-07 2018-05-11 Steganography, Covert Channels, Anonymity, Trusted Computing
2018-05-14 Summary and Exam Preparation
2018-02-26Sheet #1unit testing and coverage (stack and rpn calculator)
2018-03-08Sheet #2partial correctness and total correctess of the gcd algorithm
2018-04-04Sheet #3logical clocks and communicating sequential processes
2018-04-06Midterm Exam09:45-11:00 East Wing (closed book, hand written cheat sheet (one single-sided a4 page or a double-sided a5 page) allowed)
2018-04-24Sheet #4symmetric encryption and proof of work
2018-05-16Sheet #5gpg keys, X.509 certificates, ocsp
2018-05-25Final Exam09:00-11:00 Conference Hall (closed book, hand written cheat sheet (one single-sided a4 page or a double-sided a5 page) allowed)

The final grade is made up of the final exam (40 %), a midterm exam (30 %) and homework assignments (30 %). It is required to submit the solution for homeworks assignments electronically. Late submissions will not be accepted. Homeworks may need to be defended in an oral interview.

Any programs which have to be written will be evaluated based on the following criteria:

  • correctness including proper handling of error conditions
  • proper use of programming language constructs
  • clarity of the program organization and design
  • readability of the source code and any output produced

Source code must be accompanied with a README providing an overview of the source files and giving instructions how to build the programs. A suitable Makefile is required if the build process involves more than a single source file.

For any questions stated on assignment sheets, quiz sheets, exam sheets or during makeups, we by default expect a reasoning for the answer given, unless explicitely stated otherwise.

The policy on makeup quizzes is the following: There won't be any quiz makeups. If you (a) get an official excuse for a quiz from the registrar's office or (b) approach we well in advance of the quiz with a very good reason for not being able to participate (e.g., because you take a GRE computer science subject test at the day of a quiz), then the weight of the final exam will be increased according to the weight of the quiz you got excused for.