Selected Topics in Formal Methods for Security

Dear students,

on April 1-5, CISPA is organizing a one-week meeting of young researchers (Bachelor/Master level) with presentations from CISPA faculty in different areas of cybersecurity: https://cispa.saarland/secon/

The meeting is intended for international students that come and see CISPA for the first time, but we still have a few spots left to be filled. If you are interested, you can apply for one of these spots by following the "Register Now!" link on the page. Your application should arrive by the end of this week (sooner is better) - if you have questions feel free to contact me.

P.S.: As a local student you will not get a travel grant, but we will reimburse the participation fee.

Dear students,

I have now made available (under Materials) the slides of your talks, as well as photos of the whiteboard from our discussions. Both should help you in writing your final report that is due February 28.

As explained on the introductory slides, the report should contain at the very least a short summary of all papers you read (about half a page per paper). To get full points, it should also include an analysis of the papers (strengths, weaknesses, possible extensions,...) and a comparison between them. You are free to choose an appropriate structure yourself (e.g., each summary directly followed by an analysis and comparison, or first all the summaries and then a separate part on analysis and comparison). None of this has to go into the formal details, and the expected length of the report is 8-12 pages.

Dear students,

the dates of paper presentations (together with paper titles) are now available under Information -> Timetable.

I have also added the template for the final report, as well as scoresheets for report and presentation, under Information -> Materials. Please use the template and take the scoresheets into consideration when preparing your presentation and report.

Dear students,

the presentation topics have finally been assigned (there has been some trouble figuring out who still participates in the seminar, sorry for that).

In the next meeting, Karl Schrader will give an informal presentation of the paper Secure Information Flow by Self-composition.

It would be great if we had one or two volunteers for the other paper, Automated Analysis of Cryptographic Protocols Using Murphi. Please let me know if you would be willing to present it on Thursday. If that works, we will not have additional reading group papers and will directly proceed to your full presentations, probably starting on December 6.

See you next week!

 

Dear students,

for those of you who have not had a course on verification (or similar) or who want to refresh their memory, I have added another resource under Information->Materials->Background: the book "Principles of Model Checking".

Necessary for our seminar is only Section 2.1, which explains what a transition system is and how its reachable states are defined, as well as Section 2.2 up to (including) Section 2.2.1, which explains the concurrent execution of multiple transition systems - a special case of that will be important for model checking information-flow properties.

To get a better background, Chapter 1 and Sections 3.1 to 3.3 are also useful. The rest of the book goes beyond what we will need in the seminar.

Dear students,

for those of you that do not have a background in model checking, I have added a link to a course "Introduction to Model Checking" in the Materials.

To get the basic ideas of system models, Lecture 1 and the first half of Lecture 2 should be enough.

Based on these models, we are interested in safety model checking, which is fairly simple: does there exist a finite trace in the model with certain properties? (in the easiest case: a trace that ends in a state with a certain given label)