News
Final GradeWritten on 12.10.23 (last change on 12.10.23) by Raven Beutner Dear students, You can now find your final grade on your personal status page. |
Final Summary SubmissionWritten on 21.09.23 by Raven Beutner Dear Students, The deadline for submitting the final version of your summary is tomorrow (22.09.2023, 23:59). Please submit your final version using the submission form in the CMS on your personal status page.
|
Summary Draft DeadlineWritten on 05.09.23 (last change on 05.09.23) by Raven Beutner Dear Students, As a reminder, the deadline for submitting your (draft) summary to get feedback from your advisor is the 8th of September (this Friday). The submission of this draft version is mandatory. We look forward to reading your summaries. |
Today's seminar starts at 14:00Written on 20.06.23 by Raven Beutner Dear students, Please remember that we start today's seminar at 14:00 sharp.
|
Updated Schedule - No Seminar Next Week, Three Talks on June 20Written on 06.06.23 by Norine Coenen 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… 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. |
Advisor for Individual Talks and First Group TalkWritten on 16.05.23 by Raven Beutner 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… 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. |
Paper AssignmentWritten on 28.04.23 by Raven Beutner 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… 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