Secure and Dependable Systems

About

  • Course: Secure and Dependable Systems (CO21-320203)

  • Semester: Spring 2019

  • Instructor: Jürgen Schönwälder

  • TA: Milen Vitanov

  • TA: Aditya Dandekar

  • Class: Tuesday, 14:15-15:30, Lecture Hall Research I

  • Class: Thursday, 14:15-15:30, East Hall 4

  • Office: Monday, 11:15-12:30 (Research I, Room 87)

  • Start: 2019-02-05

Content

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).

Resources

Books

    1. Schneier: Applied Cryptography, 20th Anniversary Edition, Wiley, 2015

  • Wm.A. Conklin, Gregory White: Principles of Computer Security, 5th Edition, McGraw-Hill, 2018

    1. Singh: The Code Book: Science of Secrecy from Ancient Egypt to Quantum Cryptography, Anchor Books, 2000

Links

Schedule

Tu 14:15 Th 14:15 Topics
2019-02-05 2019-02-07 Dependability Concepts and Classic Computing Disasters
2019-02-12 2019-02-14 Software Engineering and Testing
2019-02-19 2019-02-21 Software Specification and Verification
2019-02-26 2019-03-28 Automated Generation of Proof Goals and Termination Proofs
2019-03-05 2019-03-07 Time, Events, and Causality in Distributed Systems
2019-03-12 2019-03-14 Broadcast Algorithms, Communicating Sequential Processes
2019-03-19 2019-03-21 Communicating Sequential Processes
2019-03-26 2019-03-28 pi Calculus
2017-04-02 2019-04-04 Cryptography, Symmetric Encryption Algorithms and Block Ciphers
2019-04-09 2019-04-11 Asymmetric Encryption Algorithms, Cryptographic Hash Functions
2019-04-16 2019-04-18 [Spring Break]
2019-04-23 2019-04-25 Certificates, Key Exchange Schemes, Pretty Good Privacy
2019-04-30 2019-05-02 Transport Layer Security, Secure Shell
2019-04-07 2019-05-09 Steganography, Covert Channels
2019-05-14 2019-05-16 Anonymity, Trusted Computing

Dates

Date/Due Name Topics
2019-02-28 Sheet #1 unit testing and coverage (stack and rpn calculator) rpn-stack.h rpn.h
2019-03-14 Sheet #2 correctness proof using Hoare logic
2019-03-28 Sheet #3 logical clocks, consistent cuts, and causal reliable broadcasts
2019-04-09 Midterm Exam Campus Center Eastwing (closed book, handwritten single-sided a4 or double-sided a5 cheat sheet allowed)
2019-04-25 Sheet #4 simple symmetric encryption algorithm (scrypt) p4-scrypt.zip
2019-05-09 Sheet #5 pgp keys and x.509 certificates
2019-05-16 Sheet #6 simple steganographic text hiding (pnmhide) p6-pnmhide.zip
2019-05-25 Final Exam 16:00-18:00, SCC Hall 3 (closed book, handwritten single-sided a4 or double-sided a5 cheat sheet allowed)

Results

Evaluation

Rules

The final grade is made up of the final exam (40%), a midterm exam (30%) and homework assignments (30%).

Electronic submission is the preferred way to hand in homework solutions. Please submit documents (plain ASCII/UTF-8 text or PDF, no Word) and your source code (packed into a tar or zip archive after removing all binaries and temporary files) via the online submission system. If you have problems, please contact one of the TAs.

Late submissions will not be accepted. Homeworks may need to be defended in an oral interview. In case you are ill, you have to follow the procedures defined in the university policies to obtain an official excuse. If you obtain an excuse, the new deadline will be calculated as follows:

  1. Determine the number of days you were excused until the deadline day.

  2. Determine the day of the end of your excuse and add the number of day you obtained in first step. This gives you the initial new deadline.

  3. If the period between the end of your excuse and the new deadline calculated in the second step includes weekend days, add them as well to the new deadline. (Iterate this step if necessary.)

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.

Students must submit solutions individually. If you copy material verbatim from the Internet (or other sources), you have to provide a proper reference. If we find your solution text on the Internet without a proper reference, you risk to lose your points. Any cheating cases will be reported to the registrar. In addition, you will lose the points (of course).

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 by a README file 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.

If you are unhappy with the grading, please report immediately (within one week) to the TAs. If you can't resolve things, contact the instructor. Problem reports which come late, that is after the one week period, are not considered anymore.

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.