News
01.02.2021
|
PROTO: project assignment deadlineReminder: you have got until Wednesday to pick a project. You can still pick one afterwards, but conflicts are resolved for the team that picked their project before the deadline. |
01.02.2021
|
SysV: Oral examDetails and time table for the Oral exam is published on the SysV webpage. Please check it. |
19.01.2021
|
SysV: Sheet 3 Solutions and GradeI have graded assignment 3 and you should have received an email with your grade and a marked version of your solution. Solutions to assignment 3 are available here. |
11.01.2021
|
SysV: Oral exam date
The oral exam will be on February 5. Further details will be published on the course webpage soon. |
11.01.2021
|
SysV: [Update] Problem set 3There was a minor typo (in using i and j) in the description of the second question from Problem set 3. Please check it! |
09.01.2021
|
SysV: Oral examThe oral exam for "System Verification" part of the course will be sometime in February after Robert's lectures. I will send out a doodle link next week to find a date which suits all students who want to take the exam. |
09.01.2021
|
SysV: Q&A session videoThe video for the fourth Q&A session is published: link. |
09.01.2021
|
SysV: Sheet 2 Solutions and GradeI have graded assignment 2 and you should have received an email with your grade and a marked version of your solution. Solutions to assignment 2 are available here. |
07.01.2021
|
IFC - Oral Exam ResultsThe results of the IFC oral exams are now published and you should have received an email with your score. I did enter the results a few days after the exams, but did not realize that I needed a few more clicks to publish them. Apologies for the inconvenience. |
06.01.2021
|
SysV: fourth Q&A session starting soonThe last Q&A session for the system verification techniques starts at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/94653471916?pwd=bzFtaUdaL1NTY3VUYUhEZ2gyNU9oZz09 Agenda for the today meeting is:
The last Q&A session for the system verification techniques starts at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/94653471916?pwd=bzFtaUdaL1NTY3VUYUhEZ2gyNU9oZz09 Agenda for the today meeting is:
Please join :) |
04.01.2021
|
Register in LSF by Feb. 1The official exam date for the course is Feb. 8, so we kindly ask students who want to receive points from the course to register in LSF by Feb. 1. Thanks! |
03.01.2021
|
SysV: Notes on the third question of Problem set 2 (deadline is extended)It seems that some of you (and not all) had problem understanding third question, so I try here to clarify this question a bit more and I extend the deadline until Wednesday (January 6) so that you can fix your answers. The goal of this question is to see how we... Read more It seems that some of you (and not all) had problem understanding third question, so I try here to clarify this question a bit more and I extend the deadline until Wednesday (January 6) so that you can fix your answers. The goal of this question is to see how we can apply a compositional approach to prove noninterference for a real world scenario where we have a processor connected to the main memory and the MMU. The interaction between these three components is clearly stated in the third lecture so if you have not heard about them before please refer to the lecture three. In this scenario the core component is acting on behalf of the user level processes. This means that it receives requests in term of read and write operations from the user processes and tries to execute them and retrive the data from (or write user supplied date into) the memory. As you may remember from your Operating System course processes are using virtual addresses to access the memory. However, the main memory is indexed with physical addresses. This implies that whenever the core receives a memory access request from a user process, it should first translate this address into the corresponding physical address and for this the core queries the MMU. 1- The word "interface" in the first part of the question has a standard meaning. In other words by "interface" we mean a set of functionalities that the core provides to user level processes or to interact with the memory and the MMU. 2- I think the second part of the question is completely clear. What you need to do here is to define an observation relation as required by the noninterference property. The observation relation defines which parts of the memory and core states are visible to an attacker. In translating virtual-to-physical addresses the MMU uses page tables which store the mapping between virtual and physical addresses. So the page tables are security critical and must be protected from modifications by a user level process. Otherwise they can change the mappings in these tables and get access to secret part of the system and invalidate the noninterference property. 3- The third part of the question asks you to define a predicate which prevents user level processes from changing page tables. We need this to be able to prove the noninterference property and without defining such a constraint we cannot do the proof. In order to answer this question what you will need to define is a function like MMU which takes as input the memory and user request plus some other stuffs (if needed, you figure this out) and return either the corresponding physical address or an error saying that the request is invalid due to permission error or other issues. 4- If you manage to define the previous parts reasoning compositionally about the noninterference property should be easy. What you will need to do here is to split the proof other the noninterference property into two separate parts one about the core components and the other one about the memory. To help you further with answering this question I ask you to check the section 4 of this paper (link). Please also remember that if you have any problem understanding lectures or exercises YOU SHOULD ASK US thats why we have Q&A sessions. |
03.01.2021
|
SysV: the fourth lecture is outThe fourth lecture is available now: link (https://dl.cispa.de/s/twYqAqGjGxSo8pt). This lecture we talk about validation of abstract side channel models for computer architectures. The goal of this lecture is to learn about combining formal methods and fuzzing to... Read more The fourth lecture is available now: link (https://dl.cispa.de/s/twYqAqGjGxSo8pt). This lecture we talk about validation of abstract side channel models for computer architectures. The goal of this lecture is to learn about combining formal methods and fuzzing to find bugs in low-level systems. Supplementary materials: Please make sure to check the lecture before our Q&A session on Wednesday (January 6). |
28.12.2020
|
SysV: Sheet 1 Solutions and GradeI have graded assignment 1 and you should have received an email with your grade and a marked version of your solution. Solutions to assignment 1 are available here. |
19.12.2020
|
SysV: third assignment (Deadline January 15, 23:59)The third problem set on SysV is available now.
The deadline is January 15, 23:59. We wish you a happy and prosperous new year :) |
19.12.2020
|
SysV: Q&A session videoThe video for the third Q&A session is published: link. |
16.12.2020
|
SysV: third Q&A session starting soonThe third Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/97307213380?pwd=eTNxbHI2eHJWRStMQVZIUWJjTXhOZz09 Agenda for the meeting is:
The third Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/97307213380?pwd=eTNxbHI2eHJWRStMQVZIUWJjTXhOZz09 Agenda for the meeting is:
Please join :) |
15.12.2020
|
SysV: note on "option simulation"Regarding the "option simulation" note that the right hand side diagram represents the situation where we have "stuttering", however we know that the "measure" is decreasing thus the abstract model cannot infinitely stutter. When the stuttering finished then the... Read more Regarding the "option simulation" note that the right hand side diagram represents the situation where we have "stuttering", however we know that the "measure" is decreasing thus the abstract model cannot infinitely stutter. When the stuttering finished then the left hand side diagram holds and we can continue to compare abstract and concrete models behaviour. |
15.12.2020
|
SysV: notes on confidentiality preserving refinementSome notes on confidentiality preserving refinement stated in the following theorem: where Regarding the simulation relation used in the confidentiality preserving refinement part of the... Read more Some notes on confidentiality preserving refinement stated in the following theorem: where Regarding the simulation relation used in the confidentiality preserving refinement part of the lecture, please note the direction of the simulation property, that is "T_impl simulates T_spec". This is in opposite direction of the simulation property we normally use to prove the functional correctness of systems. The specific direction that we used here guarantees that all permitted behaviour of the systems (modeled by the specification) are also behaviour of the implementation model. In the simulation relation definition the condition "if s_1 \in \alpha then s'_1 \in \alpha" guarantees that initial states of the two transitions are related by the property \alpha |
14.12.2020
|
SysV: note on confidentiality preserving refinementI posted a note about the specific simulation relation that we used to get the confidentiality preserving refinement in our Rocketchat channel. Please checked it out! |
13.12.2020
|
SysV: the third lecture is outThe third lecture is available now: link (https://dl.cispa.de/s/GyeL7TLRkQkrRrR). This lecture we talk about refinement based reasoning and learn how to use a step-wise approach to simplify verification of a large scale system. Supplementary materials:
The third lecture is available now: link (https://dl.cispa.de/s/GyeL7TLRkQkrRrR). This lecture we talk about refinement based reasoning and learn how to use a step-wise approach to simplify verification of a large scale system. Supplementary materials:
Please make sure to check the lecture before our Q&A session on Wednesday (Dec. 16).
|
11.12.2020
|
SysV: second assignment (Deadline January 3, 23:59)The second problem set on SysV is available now. The deadline is January 3, 23:59. |
11.12.2020
|
SysV: Q&A session videoThe video for the second Q&A session is published: link. |
09.12.2020
|
[IFC] - Sheet 3 Solutions and GradeI have graded assignment 3 and you should have received an email with your grade and a marked version of your solution. A few general comments about this assignment:
I have graded assignment 3 and you should have received an email with your grade and a marked version of your solution. A few general comments about this assignment:
|
09.12.2020
|
SysV: second Q&A session starting soonThe second Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/98380099551?pwd=NGpyc29UWUhiaHZLQ2pqMXZvUE9qZz09 Agenda for the today meeting is:
The second Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/98380099551?pwd=NGpyc29UWUhiaHZLQ2pqMXZvUE9qZz09 Agenda for the today meeting is:
Please join :) |
06.12.2020
|
SysV: the second lecture is outThe second lecture is available now: link (https://dl.cispa.de/s/ct8Jo4iMwC3bogT). This lecture we talk about compositional reasoning and learn about some of the techniques that are used in practice to decompose large scale system verification. Supplementary... Read more The second lecture is available now: link (https://dl.cispa.de/s/ct8Jo4iMwC3bogT). This lecture we talk about compositional reasoning and learn about some of the techniques that are used in practice to decompose large scale system verification. Supplementary materials: Please make sure to check the lecture before our Q&A session on Wednesday (Dec. 9). |
03.12.2020
|
SysV: Q&A session videoThe video for the first Q&A session is published: link. Unfortunately we managed to record only the second half of the session! |
03.12.2020
|
SysV: first assignment (Deadline December 18, 23:59)The first problem set on SysV is available now. The deadline is December 18, 23:59. |
02.12.2020
|
IFC Sheet 2 - Solutions and GradeI have graded assignment 2 and you should have received an email with your grade and a marked version of your solution. A few general comments about this assignment:
I have graded assignment 2 and you should have received an email with your grade and a marked version of your solution. A few general comments about this assignment:
|
02.12.2020
|
SysV: first Q&A session starting soonThe first Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/97760616192?pwd=ZVJrRW9mclo2VmJ6TzF6V2dFY09udz09 Agenda to the meeting today is:
The first Q&A session for the system verification techniques start at 10:00AM today. Zoom link: https://cispa-de.zoom.us/j/97760616192?pwd=ZVJrRW9mclo2VmJ6TzF6V2dFY09udz09 Agenda to the meeting today is:
Please join :)
|
01.12.2020
|
Final Q&A session starting soonPlease join: https://cispa-de.zoom.us/j/99706408403?pwd=R3QyeVY0Y3RZU3ZxNDNnb1RZSGJKQT09 |
29.11.2020
|
SysV: the first lecture is outThe first lecture is available now: link (https://dl.cispa.de/s/BmE27p7wqrcCMZs). This lecture we talk about preliminaries and try to set the stage for the other lectures. Supplementary materials: The first lecture is available now: link (https://dl.cispa.de/s/BmE27p7wqrcCMZs). This lecture we talk about preliminaries and try to set the stage for the other lectures. Supplementary materials: Please make sure to check the lecture before our Q/A session on Wednesday (Dec. 2). |
29.11.2020
|
Second part of the course starts ...This week we start with the second part of the course, which covers topics related to system verification (SysV). As it is announced before this part of the course will be given by recorded lectures (plus supplementary materials including lecture notes and... Read more This week we start with the second part of the course, which covers topics related to system verification (SysV). As it is announced before this part of the course will be given by recorded lectures (plus supplementary materials including lecture notes and other useful documents) which will be available at the beginning of each week. On Wednesdays we will meet to check the important points together to clarify parts which are not clear and we will also try to answer your questions and talk about exercises. The communication will be done through Rockchat #sysv channel, so please join the channel and ask your questions there. Organisation of the course is available here, where we also publish links to the course materials. |
28.11.2020
|
Syllabus PublishedYou can find the topics covered in each lecture and that can be asked at the the oral exam in the IFC page, |
28.11.2020
|
Material for IFC Q&A 4Here you can find the recorded video and the notes for Q&A session 4. The notes include some clarification about assignment 1 and an example evaluation of a MAC computation (forcing and thunk semantics), which highlights the difference between pure and... Read more Here you can find the recorded video and the notes for Q&A session 4. The notes include some clarification about assignment 1 and an example evaluation of a MAC computation (forcing and thunk semantics), which highlights the difference between pure and forcing/thunk semantics and how they preserve typing. |
26.11.2020
|
IFC Sheet 3 Published (Deadline December 6, 23:59)The third exercise sheet on IFC is published here. The deadline is December 6, 23:59. |
26.11.2020
|
IFC Lecture 4 - Material UploadedI have uploaded the notes and the video of the 4th lecture on IFC. |
24.11.2020
|
IFC - Oral Exam & Final Q&A Session - ***Changed Dates***I have mixed up the weeks in my calendar and therefore I have to reschedule the exams and final Q&A session as you can see below. The slots in the old doodle are not available anymore. If you have already booked one of those slots, you have to pick a new... Read more I have mixed up the weeks in my calendar and therefore I have to reschedule the exams and final Q&A session as you can see below. The slots in the old doodle are not available anymore. If you have already booked one of those slots, you have to pick a new one. Apologies for the inconvenience.
New DatesThe oral exam will take place on December 3 and December 4, on Zoom. To register for the exam, book a slot in this Doodle. You can find more information on the content and the format of the exam on the IFC page. You are welcome to join the final Q&A session on December 1, from 14 to 16 on Zoom to ask questions about all the topics of the course. During this session, we can also simulate an oral examination in preparation for the exam, where I ask exam-like questions and students try to answer and receive immediate feedback. |
24.11.2020
|
IFC Sheet 1 - Solutions and GradeI have graded assignment 1 and you should have received an email with your grade and a marked version of your solution. Do not forget that assignment 2 is due tonight at 23:59. |
19.11.2020
|
IFC Lecture 3 - Material UploadedI have uploaded the notes and the video of the 3rd lecture on IFC. |
17.11.2020
|
IFC Sheet 2 Published (Deadline Friday 24, 23:59)The second exercise sheet for IFC is published here. The deadline is Friday 24, 23:59. Submissions must be made on CMS (not by email). |
04.11.2020
|
Account for RocketChatTo log in to RocketChat, use your SIC account, not the university account. Normally, all students should automatically get an account, but it appears that an employee shortage has delayed this process. If you do not have a SIC account, follow the instructions... Read more To log in to RocketChat, use your SIC account, not the university account. Normally, all students should automatically get an account, but it appears that an employee shortage has delayed this process. If you do not have a SIC account, follow the instructions at https://it.cs.uni-saarland.de/students/accounts to obtain one. If you have one, join the channel #ifc (password: non-interference). |
Despite decades of research in computer security, security vulnerabilities still plague computer systems with an ever-growing number of new vulnerabilities discovered every day. How can we ensure that computer systems are really secure? Formal methods offer a promising approach towards this goal: they can guarantee the absence of specific security vulnerabilities with mathematical certainty and therefore help us develop mode reliable systems.
In this course, we will study how formal methods can be applied to verify that the design and implementation of computer systems respect their intended security policies. The course is structured in three independent parts, which focus on specific techniques for different domains: language-based information-flow control, security protocols, and system-level verification. As a whole, the course will give you hands-on experience in reasoning about security at different layers of abstraction through established principled techniques and a broad introduction to state-of-the-art research in the area.
Topics and Instructors
-
Language-based Information-Flow Control (Marco Vassena)
In the first part of the course, we will study information-flow control techniques that track how data flows in a program to enforce data confidentiality and integrity. We will discuss both static and dynamic IFC techniques based on security type systems and taint tracking, as well as techniques that track data flows in a program at a different granularity (for example per program variable or per program block). Finally, we will see how programming languages principles can be applied to formally verify that these techniques enforce security. Basic knowledge of programming languages theory is preferred, but not required.
- Proof techniques for system verification (Hamed Nemati)
The main goal of the second part of this course is to show you how we should approach verification of large scale systems like micro-kernels and hypervisors. This is a very challenging task in practice. We will study abstraction, decomposition and refinement as techniques that usually used in practice to facilitate verification of such systems. Finally, in our last lecture we see how we can combine fuzzing and formal verification to validate systems that their verification is not feasible in practice.
-
Protocol Verification (Robert Künnemann)
Protocol verification assumes that the cryptography is perfect and tries to ensure that they are used correctly. It is not about defending against super smart mathematicians exploiting biases in key streams, but equally smart hackers confusing one party about the state of another party.We will discuss how to get from the Alice-bob notation to a minimalistic, precise specification of the protocol and its setuphow to formulate our security requirements and how to verify that these requirements hold, using tools that have by now reached an impressive degree of automation.
Organization
Registration: open now! (Once you are registered here, don't forget to register in the LSF.)
When: Wed 10h-12h
Where: Zoom (links will appear in the calendar)
Calendar & Lecture plan: link (Click "..." next to calendar for subscription link for your favorite application) (work in progress)
Mode:
- First part (Marco): live lectures on Wednesday 10-12, Q&A session on Friday 10-12.
- Second+Third part (Hamed + Robert): flipped classroom: recorded lectures on Monday, Q&A session on Wednesday.
Exam requirements: three exercise sheets per part, 50% of total points, work in groups allowed
Exam: two oral exams (first and second part), and one project (third part). Passing requirement is >4.0 on two of the three.
Official exam date : February 8 2021 (register in LSF by February 1 2021)
RocketChat: Since the course is entirely virtual, we invite students to join these RocketChat channels to discuss the content of the lectures with the instructors.
- Information-Flow Control: channel #ifc, password: non-interference
- System Verification : channel #sysv, password: non-interference
- Protocol Verification (TBA)
To log in to RocketChat, use your SIC account, not the university account.
Course Goals
-
Understand the challenges of some open problems in computer security
-
Learn state-of-the-art techniques to address these problems and how to apply them (as a programmer, protocol designer, web developer etc.)
-
By-product: a taxonomy of where things can go wrong in security on different layers
Learning Objectives
After the course, students will be able to:
-
Apply Information-Flow Control (IFC) techniques to the design of secure programming languages.
-
Analyze the security guarantees of IFC languages through programming languages principles.
-
Discuss problems, solutions, and open challenges presented in IFC research papers.
-
Understand fundamental concepts in verification.
-
Learn how to use formal techniques to find vulnerabilities in low-level systems.
-
Gain knowledge to be able to read and understand papers in system verification.
-
Model protocols and cryptographic assumptions in the applied-pi calculus.
-
Express authentication and secrecy properties via correspondence and reachability.
-
Exploit automated tools to verify protocols.
Target Audience
Mainly M.Sc students and interested graduate students. Interested and motivated B.Sc students should contact us and argue that (a) they are particularly interested and (b) they have the necessary background in logical reasoning to follow the course.