Formal Methods in Security

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. 

Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09

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

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.

To help you further with answering this question I ask you to check the section 4 of this paper (link).

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 "" guarantees that initial states of the two transitions are related by the property   

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:

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

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.

Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09

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

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:

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

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.

Here is the link (3:00pm): https://stanford.zoom.us/j/98571696846?pwd=NzF3N3E0aDJnSkxuUUo1TS8vbitqQT09

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

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:

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

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.

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

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

cheers,
marco

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.

I've answered the questions that popped up on askbot and uploaded the video: please find the link in the IFC page.

see you next week in class

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