# 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

Formal Methods in Security

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

1. Introductory Lecture (20 October 2021)
We'll give an overview of the three parts. Marco will give it live (find the zoom link in the calendar entry, calendar link is below -- not in the CMS timetable). Hamed and Robert prepared videos for the occasion given their travel obligations:
- Hamed's Video: https://dl.cispa.de/s/8Z5kbp8yifL7tsg
- Robert's Video: https://dl.cispa.de/s/LJFsXzfr8xWoT7Y
- Class Recording: https://dl.cispa.de/s/ZMT3oCqPTyxgHcd

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

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

4. 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 setup
how 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 (official starting time is 10:15)

Where: (all links also appear in the calendar events)

Calendar & Lecture plan: link (Click "..." next to calendar for subscription link for your favorite application).

Mode:

1. IFC (Marco): Zoom+Miro lectures on Wednesday 10-12, Q&A session on Friday 10-12 based on the askbot content (see IFC page)
2. SYSV (Hamed): flipped classroom: recorded lectures on Monday, Q&A session on Wednesday.
3. PROTO (ROBERT): live lectures on Wednesday 10-12, Q&A session on Friday 10-12, detailed lecture script.

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 9, 2022.

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