Secure and Dependable Systems

Teaching

About

  • Course: Secure and Dependable Systems (CO21-320203)
  • Semester: Spring 2020
  • Instructor: Jürgen Schönwälder
  • TA: Huynh, Dung Tri
  • TA: Mana, Irsida
  • Class: Thursday, 14:15-15:30, R.1-53 Lecture Hall
  • Class: Friday, 11:15-12:30, RLH-274 Seminar Room
  • Office Hours: Monday, 11:15-12:30 (Research I, Room 87)
  • Final Exam: Thursday, 2020-05-28 12:30-14:30 (SCC - Hall 4)
  • Makeup Exam: Monday, 2020-08-31 17:00-19:00 (R.1-53 Lecture Hall)

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

Books

  • Bruce Schneier: Applied Cryptography, 20th Anniversary Edition, Wiley, 2015
  • Wm.Arthur Conklin, Gregory White: Principles of Computer Security, 5th Edition, McGraw-Hill, 2018
  • Simon Singh: The Code Book: Science of Secrecy from Ancient Egypt to Quantum Cryptography, Anchor Books, 2000

Schedule

Thu 14:15 Fri 11:15 Topics
2020-02-06 2020-02-07 Recent Computing Disasters and Dependability Concepts
2020-02-13 2020-02-14 Software Engineering and Testing
2020-02-20 2020-02-21 Software Specification and Verification
2020-02-27 2020-03-28 Automated Generation of Proof Goals and Termination Proofs
2020-03-05 2020-03-06 Software Vulnerabilities and Exploits
2020-03-12 2020-03-13 Exploits, Attacks, and Compromises
2020-03-19 2020-03-20 Cryptography, Block Ciphers, Symmetric Encryption Algorithms
2020-03-26 2020-03-27 Asymmetric Encryption Algorithms, Cryptographic Hash Functions
2017-04-02 2020-04-03 Digital Signatures, Certificates, Key Exchange Schemes
2020-04-09 2020-04-10 [Spring Break]
2020-04-16 2020-04-17 Pretty Good Privacy, Transport Layer Security
2020-04-23 2020-04-24 Transport Layer Security, Secure Shell
2020-04-30 2020-05-01 Steganography, Covert Channels
2020-05-07 2020-05-08 Anonymity, Mix Networks and Onion Routing, Isolation, Trusted Computing
2020-05-14 2020-05-15 Authentication, Authorization, Auditing

Assignments

Date/Due Name Topics
2020-02-27 Sheet #1 unit testing and coverage (stack and rpn calculator) rpn-stack.h rpn.h
2020-03-05 Sheet #2 fuzzying (stats calculator)
2020-03-12 Sheet #3 correctness proof (exponentiation algorithm)
2020-03-19 Sheet #4 Intel x86_64 machine code and stack frames
2020-03-26 Sheet #5 simple symmetric encryption algorithm (scrypt) p5-scrypt.zip
2020-04-02 Sheet #6 decryption of an RSA encrypted message, cryptographic puzzle
2020-04-16 Sheet #7 X.509 certificates, diffie-hellman key exchange
2020-04-23 Sheet #8 pretty good privacy, transport layer security
2020-04-30 Sheet #9 penetration testing, ethical hacking virtual machine
2020-05-07 Sheet #10 simple steganographic text hiding (pnmhide) p10-pnmhide.zip

Rules

The final grade is determined by a final exam (100%). There will be graded homework assignments but the homework assignments do not impact the final grade.

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.

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 explicitly stated otherwise.

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.