# Formal Methods in Security Patrignani, Nemati, Künnemann

## News

30.01.2022

#### SysV: Oral exam

Please 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 session

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.

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.

03.01.2022

#### PROTO parts start at 16:00 and materials online

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.
The lecture script is available on the Materials page. Remember to read it before... Read more

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.
The lecture script is available on the Materials page. Remember to read it before the lecture – we want to discuss it.

Cheers, Robert

02.01.2022

#### SysV: the fourth lecture is out

The fourth lecture is available now: link (https://drive.google.com/file/d/1GnrphWdqJz5gDe-oFbg1kNbSNcDYPBU5/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/1GnrphWdqJz5gDe-oFbg1kNbSNcDYPBU5/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 low-level systems.

Supplementary materials:

• Validation of obs. models (link)

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 extended

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

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.

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.

The problem set for the third lecture will be posted tomorrow.

12.12.2021

#### SysV: Notes on the third question of Problem set 2

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

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 refinement

Some notes on confidentiality preserving refinement stated in the following theorem:

$\text{Theorem:&space;we&space;say}&space;\mathit{T_{impl}\&space;\mathcal{P}\!-\!refine\&space;T_{spec}}&space;\text{&space;if&space;}&space;T_{spec}&space;\lesssim&space;T_{impl}&space;\text{&space;and&space;all&space;behaviours&space;of&space;}&space;T_{impl}&space;\text{&space;are&space;possible&space;behaviours&space;of&space;}&space;T_{spec}.$

where   $T_{spec}&space;\lesssim&space;T_{impl}$  means "T_impl simulates T_spec" and it is define as follows:

$\forall&space;s_1&space;\lesssim&space;s'_1&space;\text{&space;and&space;}&space;\alpha&space;\in&space;\mathcal{P}&space;\text{&space;if&space;}&space;s_1&space;\in&space;\alpha&space;\text{&space;then&space;}&space;s'_1&space;\in&space;\alpha&space;\text{&space;and&space;for&space;all&space;}&space;s_2&space;\text{&space;and&space;}&space;a&space;\in&space;\mathbb{A}&space;\text{&space;such&space;that&space;}&space;s_1&space;\xrightarrow[]{a}&space;s_2&space;\text{&space;then&space;there&space;exists&space;}&space;s'_2&space;\text{&space;such&space;that&space;}&space;s'_1&space;\xrightarrow[]{a}&space;s'_2&space;\text{&space;and&space;}&space;s_2&space;\lesssim&space;s'_2.$

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  $Tr(T_{impl})&space;\subseteq&space;Tr(T_{spec})$ .

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 "$\text{if&space;}&space;s_1&space;\in&space;\alpha&space;\text{&space;then&space;}&space;s'_1&space;\in&space;\alpha$" guarantees that initial states of the two transitions are related by the property $\alpha$

12.12.2021

#### SysV: the third lecture is out

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 step-wise 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 step-wise approach to simplify verification of a large scale system.

Supplementary materials:

• Simulation based refinement (link). Important sections are :
• section 2.1: Notions of semantic preservation
• section 3.4: Traces
• section 3.5: Transition semantics
• [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. 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 session

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.

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.

The problem set for the second lecture will be posted tomorrow.

05.12.2021

#### SysV: the second lecture is out

The second lecture is available now: link (https://drive.google.com/file/d/1-UyTwzaubGD_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/1-UyTwzaubGD_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 session

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.

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.

The problem set for the first lecture will be posted tomorrow.

28.11.2021

#### SysV: the first lecture is out

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:

• Formalisation  of the noninterference... Read more

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:

• 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. 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 links

Hello students,
the recording for today's class is out.

Also, here are the zoom links for the exams:

Friday 9th we'll use this room:
Join URL: https://cispa-de.zoom.us/j/98062819490?pwd=YnFhMUprSW12dFdXM25HVkQ3b1ZwUT09

Hello students,
the recording for today's class is out.

Also, here are the zoom links for the exams:

Friday 9th we'll use this room:
Join URL: https://cispa-de.zoom.us/j/98062819490?pwd=YnFhMUprSW12dFdXM25HVkQ3b1ZwUT09

Saturday 10th we'll use this room:
Join URL: https://cispa-de.zoom.us/j/94994203176?pwd=WjVzVVFEMmwxN1RLbWxBRHJRMDVtdz09

cheers,
marco

17.11.2021

Hello students,

10.11.2021

#### IFC class 3

Hi students,

the recording of today's lecture is up!

03.11.2021

#### IFC Class 2

Hi 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 1

Hello students,

the first IFC assignment is out, you can find it in the materials section.

29.10.2021

#### IFC Q&A 1

Hello students,

there's been a mismatch between the date as indicated in the IFC page for the Q&A
and the date in the calendar used to run the events.

Now they're in sync: Q&A will be at 10:00 am in the future.

Hello students,

there's been a mismatch between the date as indicated in the IFC page for the Q&A
and the date in the calendar used to run the events.

Now they're in sync: Q&A will be at 10:00 am in the future.

see you next week in class

27.10.2021

#### Participation and Lecture 1 update

Dear students,

there were only 6 students today, dropping to 3 when asked to split up in groups for exercises.
We'd like to point out a couple of things then:

• if you are not interested in the class, please deregister
• class participation is an element of... Read more

Dear students,

there were only 6 students today, dropping to 3 when asked to split up in groups for exercises.
We'd like to point out a couple of things then:

• if you are not interested in the class, please deregister
• class participation is an element of evaluation: we expect you to *BOTH* attend class and be active in it, not just one of the two
• there is little chance you are able to pass the assignments and the exam if you do not participate during class exercises and tests

For those that do want to continue with the course:

• apologies for today's heavy cough
• the recording is up and the link is in the ifc page.
The audio there does not seem corrupted. I'll resort to the better laptop in the future to avoid similar issues
• i've added the derivation for the missing exercise too -- i got confused during class and thought we were doing the wrong derivation, but the derivation there is correct
• remember that the friday Q&A is only done if there are questions on askbot