Hyperproperties Raven Beutner, Norine Coenen, Arthur Correnson, Matthias Cosler, Bernd Finkbeiner, Florian Kohn, Julian Siber

News

06.06.2023

Updated Schedule - No Seminar Next Week, Three Talks on June 20

Dear students, 

Due to scheduling conflicts, we adapted our talk schedule (see the updated timetable in the CMS). We will not meet next week for the first talk, instead we will have three talks the week after on June 20. To accommodate the extra talk, we will... Read more

Dear students, 

Due to scheduling conflicts, we adapted our talk schedule (see the updated timetable in the CMS). We will not meet next week for the first talk, instead we will have three talks the week after on June 20. To accommodate the extra talk, we will start at 2pm sharp that week and will probably overrun our time slot a bit. We appreciate your understanding and ask you to accommodate this, if at all possible.  

See you in two weeks. 

16.05.2023

Advisor for Individual Talks and First Group Talk

Dear students,

You can now see your advisor for your individual talk on your personal status page. Your advisor will reach out to you in the next few days.

We also fixed time slots for the individual talks. You can see the schedule on your personal status page... Read more

Dear students,

You can now see your advisor for your individual talk on your personal status page. Your advisor will reach out to you in the next few days.

We also fixed time slots for the individual talks. You can see the schedule on your personal status page and in the calendar. The first individual talk will take place on 13.06.

The first group talk will take place next week (23.05). Make sure that you have read the first key paper (which can be found in the Material Section) until then.

28.04.2023

Paper Assignment

Dear students,
 
we have finished the paper assignment in the CMS. You can see your assigned paper (given by the tutorial number) on your personal status page. We were able to assign everyone who indicated some preference to a paper that they rated good or... Read more
Dear students,
 
we have finished the paper assignment in the CMS. You can see your assigned paper (given by the tutorial number) on your personal status page. We were able to assign everyone who indicated some preference to a paper that they rated good or very good.
 
Your advisor for the group talk will reach out to you in the next few days. Everyone assigned to papers 01-05 is part of the “Basics of Information-Flow Control” group talk, and everyone assigned to papers 06-10 is part of the “Formal Methods 101" group talk. Your advisor will point you to appropriate reading material. We will upload the two key-papers (that should be read by everyone) in the Material section shortly.
 
The first group talk (on “Basics of Information-Flow Control”) will take place on 23.05.
 

Hyperproperties

Traditional specification languages for systems usually refer to single execution traces and are therefore insufficient in many security-critical applications. This is because attackers may use comparisons between several different system traces to infer hidden secrets. Hyperproperties address this problem: Instead of specifying permitted behavior on single traces, they do so for sets of traces. The importance of research on hyperproperty specification and verification methods has recently been demonstrated by high-profile attacks such as Spectre and Meltdown, which exploit systems that violate certain information-flow policies. Further details on these attacks and their relation to hyperproperties can be found in this blog post.

In this seminar, we will have a look at state-of-the-art research on hyperproperties. This ranges from research on logics that describe hyperproperties, over verification algorithms, which check whether a system satisfies a property, to practical applications such as (runtime) monitoring.

The seminar will start with a group phase where students will present basic concepts in informal presentations. Subsequently, students will give individual talks on a research paper and hand in a summary at the end of the semester.

 

Requirements

This seminar is open to Bachelor or Master students. There are no formal requirements to take this seminar. You should have an interest in logic and related topics (as discussed in lectures like “Verification,” “Semantics,” “Automata, Games and Verification,” or “Automated Reasoning,” although none of these lectures is a prerequisite). 

 

Important Details

  • Kickoff Metting on Tuesday, 18.04.2023, 14:15-16:00 in room 106 in E1.1
  • Regular seminar sessions on Tuesdays, 14:15-16:00 in room 106 in E1.1
  • Note that we will not offer a hybrid solution. We plan to have in-person meetings as long as possible and switch to fully online if the need arises

 



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators