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://cispade.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://cispade.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 virtualtophysical 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 lowlevel 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://cispade.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://cispade.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 means "T_impl simulates T_spec" and it is define as follows: 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 means "T_impl simulates T_spec" and it is define as follows: 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 stepwise 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 stepwise 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://cispade.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://cispade.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://cispade.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://cispade.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://cispade.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 examlike 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.unisaarland.de/students/accounts to obtain one. If you have one, join the channel #ifc (password: noninterference). 