News

PROTO: project assignment deadline

Written on 01.02.21 by Robert Künnemann

Reminder: 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.

SysV: Oral exam

Written on 01.02.21 (last change on 01.02.21) by Hamed Nemati

Details and time table for the Oral exam is published on the SysV webpage. Please check it. 

SysV: Sheet 3 Solutions and Grade

Written on 19.01.21 by Hamed Nemati

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

SysV: Oral exam date

Written on 11.01.21 (last change on 19.01.21) by Hamed Nemati

Please pick the date(s) that suits you better for the oral exam from this Doodle table

The oral exam will be on February 5. Further details will be published on the course webpage soon. 

SysV: [Update] Problem set 3

Written on 11.01.21 (last change on 11.01.21) by Hamed Nemati

There was a minor typo (in using i and j) in the description of the second question from Problem set 3. Please check it!

SysV: Oral exam

Written on 09.01.21 (last change on 09.01.21) by Hamed Nemati

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

SysV: Q&A session video

Written on 09.01.21 by Hamed Nemati

The video for the fourth Q&A session is published: link.

SysV: Sheet 2 Solutions and Grade

Written on 09.01.21 by Hamed Nemati

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

IFC - Oral Exam Results

Written on 07.01.21 by Marco Vassena

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

SysV: fourth Q&A session starting soon

Written on 06.01.21 by Hamed Nemati

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:

  • Summarising the important points for the last lecture 
  • Taking your… Read more

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:

  • Summarising the important points for the last lecture 
  • Taking your questions

Please join :)

Register in LSF by Feb. 1

Written on 04.01.21 by Hamed Nemati

The 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! 

SysV: Notes on the third question of Problem set 2 (deadline is extended)

Written on 03.01.21 (last change on 03.01.21) by Hamed Nemati

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

SysV: the fourth lecture is out

Written on 03.01.21 by Hamed Nemati

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… 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:

  • Lecture notes (link)
  • Validation of obs. models (link)

Please make sure to check the lecture before our Q&A session on Wednesday (January 6).

SysV: Sheet 1 Solutions and Grade

Written on 28.12.20 (last change on 28.12.20) by Hamed Nemati

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

SysV: third assignment (Deadline January 15, 23:59)

Written on 19.12.20 (last change on 19.12.20) by Hamed Nemati

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

SysV: Q&A session video

Written on 19.12.20 by Hamed Nemati

The video for the third Q&A session is published: link.

SysV: third Q&A session starting soon

Written on 16.12.20 by Hamed Nemati

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:

  • Summarising the important points from the third lecture 
  • Taking your questions
  • Talking… Read more

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:

  • Summarising the important points from the third lecture 
  • Taking your questions
  • Talking briefly about the third problem set

Please join :)

SysV: note on "option simulation"

Written on 15.12.20 (last change on 15.12.20) by Hamed Nemati

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

SysV: notes on confidentiality preserving refinement

Written on 15.12.20 (last change on 15.12.20) by Hamed Nemati

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

Moreover, to rule out the problem stated in slide 39 (slide 44 in lecture notes) we used an additional constraint (stated as "all behaviours of T_impl are possible behaviors of T_spec" in the final Theorem) to make sure that there cannot be an implementation trace for which there is no corresponding specification trace. Please note that, in the supplementary paper this constraint is denoted as   .

These two conditions together help us to prove the theorem above and thus conclude that implementation does not leak more secret than the specification.

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  

SysV: note on confidentiality preserving refinement

Written on 14.12.20 (last change on 14.12.20) by Hamed Nemati

I 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!

SysV: the third lecture is out

Written on 13.12.20 (last change on 15.12.20) by Hamed Nemati

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:

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:

  • Lecture notes (link)
  • Simulation based refinement (link). Important sections are :
    • section 2.1: Notions of semantic preservation
    • section 3.4: Traces
    • section 3.5: Transition semantics
  • Confidentiality preserving refinement (link)
  • [Optional] Example on how to apply refinement based verification on a real system (link)

Please make sure to check the lecture before our Q&A session on Wednesday (Dec. 16).

 

SysV: second assignment (Deadline January 3, 23:59)

Written on 11.12.20 by Hamed Nemati

The second problem set on SysV is available now.

The deadline is January 3, 23:59.

SysV: Q&A session video

Written on 11.12.20 (last change on 11.12.20) by Hamed Nemati

The video for the second Q&A session is published: link.

[IFC] - Sheet 3 Solutions and Grade

Written on 09.12.20 by Marco Vassena

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

A few general comments about this assignment:

  • Also the third assignment went pretty well: 71% of the submissions were scored >… Read more

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

A few general comments about this assignment:

  • Also the third assignment went pretty well: 71% of the submissions were scored > 19 points.
  • Most of you managed to do the proofs correctly, using the right proof technique and applying lemmas and induction appropriately): very good job!
  • I noticed only two common mistakes in the proofs:
  1. When reasoning about annotated references, we need to connect the label annotation from the evaluation rules with the label in the type of the reference from the typing judgment. (To do this formally, we apply type preservation, but this is less important). Importantly, an annotated label nl1 has type (ref τ)l2 where τ = sl1. Notice that the label annotation l1 corresponds to the label of the content of the reference, not to the label l2 that annotates the reference type.
  2. In the proof of L-equivalence preservation, we apply IH to the subterms and obtain proofs that the intermediate stores and values are L-equivalent (e.g., in case !e and e1 e2). Sometimes, we need to split on the L-equivalence judgment of the intermediate values (2 cases [L-Type] and [H-Type]) to complete the proof. For example, for function application e1 ewe need to consider both the case where the function closures evaluated from e1 are labeled secret (case [H-Type]) and when they are labeled public (case [L-Type]). In case [H-Type], we apply store confinement (twice) and the square lemma; in case [L-Type], we observe that the body of the function in the closures are the same and the environments are L-equivalent, and we can conclude the proof by IH.

SysV: second Q&A session starting soon

Written on 09.12.20 (last change on 09.12.20) by Hamed Nemati

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:

  • Summarising the important points for the second lecture 
  • Taking your… Read more

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:

  • Summarising the important points for the second lecture 
  • Taking your questions
  • talking briefly about the second problem set

Please join :)

SysV: the second lecture is out

Written on 06.12.20 by Hamed Nemati

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:

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:

  • Lecture notes (link)
  • Rely-Guarantee style reasoning (link)
  • Compositional noninterference (link)

Please make sure to check the lecture before our Q&A session on Wednesday (Dec. 9).

SysV: Q&A session video

Written on 03.12.20 by Hamed Nemati

The video for the first Q&A session is published: link. Unfortunately we managed to record only the second half of the session!

SysV: first assignment (Deadline December 18, 23:59)

Written on 03.12.20 by Hamed Nemati

The first problem set on SysV is available now. 

The deadline is December 18, 23:59.

IFC Sheet 2 - Solutions and Grade

Written on 02.12.20 (last change on 02.12.20) by Marco Vassena

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

A few general comments about this assignment:

  • Also the second assignment went pretty well: 71% of the submissions were scored… Read more

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

A few general comments about this assignment:

  • Also the second assignment went pretty well: 71% of the submissions were scored > 17 points.
  • A program leaks secret data if the *public* output of the program is influenced by secret inputs. Therefore, when you claim that a program is leaky you need to argue that (1) it is well-typed and the output is labeled public (e.g., bool^L) and (2) explain how different secret inputs produce different public outputs.
  • The purpose of the program counter label (pc) is to prevent implicit leaks through the value store (e.g., if secret then low := true else ()). Therefore, only constructs that write to the store (i.e., e1 := e2, new(e)) include security checks that involve the pc. In particular, when a program writes some data labeled "l" to the store, the data must be at least as sensitive as the "pc" label, i.e., pc ⊑ l.
    Reading from the store (i.e., !e) does not need checks that involve the pc label because the type of the result is labeled with the label of the data.
  • Expressions that "create" values (e.g., (), true, false, \x.e, new(e)) can be labeled with any label. All the security checks appear in the typing rules that "use" these values (e.g., if e then e1 else e2, e1 e2, !e, write(e)). This makes the type system more permissive (it accepts more secure programs). For example, in λSFG rule [New-T] allows "new(true)" to be typed both (Ref Bool^L)^H  (in a public context) and (Ref Bool^H)^L. Although rule [Read-T] prevents programs from reading from a reference typed (Ref Bool^H)^L,  we can still accept all programs that create such a reference but never read from it. (There are extensions to λSFG that would also allow to read from such references as well).
  • Even if we modify rule [New-T] to require that the label of the reference is at least as sensitive as the label of the content, e.g., l⊑ l2, we are not entitled to omit this constraint in the other rules (e.g., [Read-T]): the inputs of the program can be arbitrarily typed, so we could still have references where l⊑ l2 does not hold.
  • When you extend λSFG with a new type, remember that there are two categories of types: simple types and labeled types. New types (e.g., array \tau) typically belong to the category "simple type".
  • The label of unit can be chosen freely in rule [Write-T] because a value () does not contain any real information (this is the only possible value of type unit). 

SysV: first Q&A session starting soon

Written on 02.12.20 (last change on 02.12.20) by Hamed Nemati

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:

  • Summarising the important points for the first lecture 
  • Taking your questions
  • talking… Read more

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:

  • Summarising the important points for the first lecture 
  • Taking your questions
  • talking briefly about the first problem set

Please join :)

 

Final Q&A session starting soon

Written on 01.12.20 by Marco Vassena

Please join: https://cispa-de.zoom.us/j/99706408403?pwd=R3QyeVY0Y3RZU3ZxNDNnb1RZSGJKQT09
 

SysV: the first lecture is out

Written on 29.11.20 by Hamed Nemati

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:

  • Lecture notes (link)
  • Formalisation  of the noninterference property and the unwinding theorem… Read more

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:

  • Lecture notes (link)
  • Formalisation  of the noninterference property and the unwinding theorem (link)

Please make sure to check the lecture before our Q/A session on Wednesday (Dec. 2).

Second part of the course starts ...

Written on 29.11.20 by Hamed Nemati

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

Syllabus Published

Written on 28.11.20 by Marco Vassena

You can find the topics covered in each lecture and that can be asked at the the oral exam in the IFC page,
If you have questions about any of these topics, come to the final Q&A session on December 1, from 14 to 16 on Zoom.

Material for IFC Q&A 4

Written on 28.11.20 by Marco Vassena

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

The typing rule [LABEL] given in lecture 4 does not technically need the "no write-down" constraint.
In these notes I have explained why the rule would still be secure without the constraint.

IFC Sheet 3 Published (Deadline December 6, 23:59)

Written on 26.11.20 by Marco Vassena

The third exercise sheet on IFC is published here.

The deadline is December 6, 23:59.

IFC Lecture 4 - Material Uploaded

Written on 26.11.20 by Marco Vassena

I have uploaded the notes and the video of the 4th lecture on IFC.

IFC - Oral Exam & Final Q&A Session - ***Changed Dates***

Written on 24.11.20 (last change on 24.11.20) by Marco Vassena

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… 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 Dates

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

IFC Sheet 1 - Solutions and Grade

Written on 24.11.20 by Marco Vassena

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

Do not forget that assignment 2 is due tonight at 23:59.

IFC Lecture 3 - Material Uploaded

Written on 19.11.20 by Marco Vassena

I have uploaded the notes and the video of the 3rd lecture on IFC.

IFC Sheet 2 Published (Deadline Friday 24, 23:59)

Written on 17.11.20 (last change on 17.11.20) by Marco Vassena

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

Account for RocketChat

Written on 04.11.20 by Marco Vassena

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

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.