Formal Methods in Security Vassena, Nemati, Künnemann

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

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.

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

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

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.     

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  

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.

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 n_l1 has type (ref τ)^l2 where τ = s^l1. 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 e₁ e₂). 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 e₁ e₂ we need to consider both the case where the function closures evaluated from e₁ 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.

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

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

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., e₁ := e₂, 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 e₁ else e₂, e₁ e₂, !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₁ ⊑ l₂, 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₁ ⊑ l₂ 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). 

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

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

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.

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.

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.

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