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

## News

01.02.2021

#### PROTO: project assignment deadline

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.

01.02.2021

#### SysV: Oral exam

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

19.01.2021

#### SysV: Sheet 3 Solutions and Grade

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.

11.01.2021

#### SysV: Oral exam date

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.

11.01.2021

#### SysV: [Update] Problem set 3

There 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 exam

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.

09.01.2021

#### SysV: Q&A session video

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

09.01.2021

#### SysV: Sheet 2 Solutions and Grade

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.

07.01.2021

#### IFC - Oral Exam Results

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.

06.01.2021

#### SysV: fourth Q&A session starting soon

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

04.01.2021

#### Register in LSF by Feb. 1

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!

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

03.01.2021

#### SysV: the fourth lecture is out

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

28.12.2020

#### SysV: Sheet 1 Solutions and Grade

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.

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 video

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

16.12.2020

#### SysV: third Q&A session starting soon

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

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 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 "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 refinement

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!

13.12.2020

#### SysV: the third lecture is out

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

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 video

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

09.12.2020

#### [IFC] - Sheet 3 Solutions and Grade

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.

• Also the third assignment went pretty well:... 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.

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

#### SysV: second Q&A session starting soon

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

06.12.2020

#### SysV: the second lecture is out

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.

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

03.12.2020

#### SysV: Q&A session video

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

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.

• Also the second assignment went pretty well:... 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.

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

#### SysV: first Q&A session starting soon

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

01.12.2020

29.11.2020

#### SysV: the first lecture is out

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

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 Published

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.

28.11.2020

#### Material for IFC Q&A 4

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

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 Uploaded

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

24.11.2020

#### IFC Sheet 1 - Solutions and Grade

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.

19.11.2020

#### IFC Lecture 3 - Material Uploaded

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

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

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

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

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

Where: Zoom (links will appear in the calendar)

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

Mode:

1. First part (Marco): live lectures on Wednesday 10-12, Q&A session on Friday 10-12.
2. Second+Third part (Hamed + Robert): flipped classroom: recorded lectures on Monday, Q&A session on Wednesday.

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 8 2021 (register in LSF by February 1 2021)

RocketChat: Since the course is entirely virtual, we invite students to join these RocketChat channels to discuss the content of the lectures with the instructors.

• Information-Flow Control: channel #ifc, password: non-interference
• System Verification : channel #sysv, password: non-interference
• Protocol Verification (TBA)

To log in to RocketChat, use your SIC accountnot the university account.

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