News
30.01.2022

SysV: Oral examPlease pick a time slot that suits you better for the oral exam from this Doodle table. The oral exam will be on February 10. Zoom link for the exam: https://stanford.zoom.us/j/92422300762?pwd=VlVNemhKS0FtTmZTOHhwQzBnZFdvUT09

05.01.2022

SysV: fourth Q&A sessionSo far there is no question on Askbot, which means again there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link... Read more So far there is no question on Askbot, which means again there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09 
03.01.2022

PROTO parts start at 16:00 and materials onlineHi! The PROTO lectures, which start next next week (Jan 12) will not be at the usual time, but at 16:00. This is to be compatible with Standford time, see the discussion on Askbot. Hi! The PROTO lectures, which start next next week (Jan 12) will not be at the usual time, but at 16:00. This is to be compatible with Standford time, see the discussion on Askbot. Cheers, Robert 
02.01.2022

SysV: the fourth lecture is outThe fourth lecture is available now: link (https://drive.google.com/file/d/1GnrphWdqJz5gDeoFbg1kNbSNcDYPBU5/view?usp=sharing). This lecture we talk about validation of abstract side channel models for computer architectures. The goal of this lecture is to learn... Read more The fourth lecture is available now: link (https://drive.google.com/file/d/1GnrphWdqJz5gDeoFbg1kNbSNcDYPBU5/view?usp=sharing). 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 5). 
30.12.2021

SysV: Deadline for the second assignment is extendedI decided to extend the deadline for the second assignment until Tuesday January 4. 
16.12.2021

SysV: third assignment (Deadline January 14, 23:59)The third problem set on SysV is available now.
The deadline is January 14, 23:59. We wish you a happy and prosperous new year :) 
15.12.2021

SysV: Third Q&A sessionSo far there is no question on Askbot, which means again there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link... Read more So far there is no question on Askbot, which means again there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09 The problem set for the third lecture will be posted tomorrow. 
12.12.2021

SysV: Notes on the third question of Problem set 2The 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 interactions between these three components are clearly stated... Read more 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 interactions between these three components are clearly stated in the third lecture so if you have not heard about them before please refer to the third lecture. 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 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). 
12.12.2021

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

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 "" guarantees that initial states of the two transitions are related by the property 
12.12.2021

SysV: the third lecture is outThe third lecture is available now: link (https://drive.google.com/file/d/192NHl94rTGki3Qedtq4BSvxKsxX2qFZY/view?usp=sharing). This lecture we talk about refinement based reasoning and learn how to use a stepwise approach to simplify verification of a large scale... Read more The third lecture is available now: link (https://drive.google.com/file/d/192NHl94rTGki3Qedtq4BSvxKsxX2qFZY/view?usp=sharing). 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. 15). 
09.12.2021

SysV: second assignment (Deadline December 30, 23:59)The second problem set on SysV is available now. The deadline is December 30, 23:59. 
08.12.2021

SysV: Second Q&A sessionSo far there is no question on Askbot, which means there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link... Read more So far there is no question on Askbot, which means there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09 The problem set for the second lecture will be posted tomorrow. 
05.12.2021

SysV: the second lecture is outThe second lecture is available now: link (https://drive.google.com/file/d/1UyTwzaubGD_A9YU4_cG1M8Z15sWAvnN/view?usp=sharing). This lecture we talk about compositional reasoning and learn about some of the techniques that are used in practice to decompose large... Read more The second lecture is available now: link (https://drive.google.com/file/d/1UyTwzaubGD_A9YU4_cG1M8Z15sWAvnN/view?usp=sharing). 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. 8). 
02.12.2021

SysV: first assignment (Deadline December 17, 23:59)The first problem set on SysV is available now. The deadline is December 17, 23:59. 
01.12.2021

SysV: First Q&A sessionSo far there is no question on Askbot, which means there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link... Read more So far there is no question on Askbot, which means there will be no Q&A session today. However, I will be in the room for a few minutes to answer random questions. Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09 The problem set for the first lecture will be posted tomorrow. 
28.11.2021

SysV: the first lecture is outThe first lecture is available now: link (https://dl.cispa.de/s/qDoPwpjRwwfcLXr). 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/qDoPwpjRwwfcLXr). 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. 1). 
26.11.2021

Second part of the course starts next week ...Next 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 Next 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. You have 3 days to check the lecture before our Q&A session. On Wednesday will meet at 15pm to answer questions (if any) that pop up on Askbot (see the menu of the course page). Please DO ask your questions on Askbot: no questions (up until the Q&A session) means no Q&A. Organisation of the course is available here, where we also publish links to the course materials. 
24.11.2021

IFC class 4 + exam linksHello students,
Also, here are the zoom links for the exams: Friday 9th we'll use this room: Saturday... Read more Hello students,
Also, here are the zoom links for the exams: Friday 9th we'll use this room: Saturday 10th we'll use this room:
cheers, 
17.11.2021

IFC exam doodleHello students, the doodle for the IFC exam is out (https://doodle.com/poll/gttyqtyga93xrins?utm_source=poll&utm_medium=link) , please select your slots. 
10.11.2021

IFC class 3Hi students, the recording of today's lecture is up! 
03.11.2021

IFC Class 2Hi students, the link for the class recording for today is up. Please let us know if you have any issue accessing it, and as always, post your questions on askbot so we'll go through them on friday.

29.10.2021

IFC assignment 1Hello students, the first IFC assignment is out, you can find it in the materials section. Pleaseheck the course page for the deadline.

29.10.2021

IFC Q&A 1Hello students, there's been a mismatch between the date as indicated in the IFC page for the Q&A Now they're in sync: Q&A will be at 10:00 am in the future. I've answered the questions that popped up on... Read more Hello students, there's been a mismatch between the date as indicated in the IFC page for the Q&A Now they're in sync: Q&A will be at 10:00 am in the future. I've answered the questions that popped up on askbot and uploaded the video: please find the link in the IFC page.
see you next week in class 
27.10.2021

Participation and Lecture 1 updateDear students, there were only 6 students today, dropping to 3 when asked to split up in groups for exercises.
Dear students, there were only 6 students today, dropping to 3 when asked to split up in groups for exercises.
For those that do want to continue with the course:
