STAR lab | Chalmers University of Technology

PhD Course, 7.5 credits
Study period 2 (November 2025 - January 2026)
Language: English
Maximum number of students: 20 (PhD students have priority)
Registrtation deadline: general LP2 25/26 course registration deadline
Instructor: Hazem Torfah

OVERVIEW

Formal methods are mathematical techniques for the specification, design, and verification of software and hardware systems. In the context of security, formal methods provide rigorous tools to model and analyze systems for potential vulnerabilities and ensure compliance with security policies. These methods enable the precise definition of security properties, such as confidentiality, integrity, and privacy, and allow for automated verification to detect flaws that may be overlooked by traditional testing. By applying formal techniques such as model checking, theorem proving, and formal specification languages, developers can build systems with provable security guarantees.

The course consists of a series of lectures on different formalisms and methods that have been developed to reason about security and privacy properties. Topics include program verification through relational Hoare logic and its probabilistic extensions, the specification and verification of hyperproperties, formal verification of cryptographic protocols, and techniques for quantitative information flow analysis and verification.

LEARNING OUTCOME

After completion of the course the student should be able to:

Explain the role of formal methods in specifying, designing, and verifying secure systems
Formally define key security and privacy properties using formal specification languages
Use automated verification tools to verify compliance with security policies and detect potential vulnerabilities
Critically assess the strengths and limitations of various formal techniques in the context of real-world security and privacy challenges.

PREREQUISITES

For PhD students:

Contact the course instructor with your background.

For Master students: We will be accepting a limited number of Master's students. To attend the course we expect to have successfully completed at least one of the following courses:

Language-Based Security (TDA602/DIT101)
Formal Methods for Software Development (TDA294/DIT272)
Logic in Computer Science (DAT060/DIT203)

ORGANIZATION

The course will be split into two parts:

Lectures:

The first part of the course will consist of a series of lectures introducing the foundational concepts and methods related to the topics listed above. We will have up to three lectures per week, and this part will span approximately 4-5 weeks. The exact schedule will be provided below. Participation in quizzes during this period is mandatory.

Project:

The second part of the course involves project work. In groups of up to two students, you will implement and experiment with a practical project that applies key concepts learned in the course. The project work will include the following tasks:

Task 1 - Choosing a topic: From a set of suggested research papers, carefully selected to build on the topics introduced in the course, you will be asked to implement the proposed approach and conduct a case study demonstrating its applicability and limitations. Alternatively, you may propose your own project (highly recommended), provided it is related to the themes of the course.
Task 2 - Presentation: The groups will give a 15-minute presentation on the topic and results of your project.
Task 3 - Report: You will write a 6-page report introducing your project, including your results and a discussion of its applicability and limitations, with comparisons to related work. The report must be accompanied by an artifact, which will undergo an artifact evaluation.

Project selection or proposals are due no later than the beginning of the fourth week of the course. Project work should begin immediately thereafter. Final presentations will take place in January.

REGISTRATION

For PhD students: please register by sending a registration email to the instructor

For masters students, this is an instance of the research-oriented course in Computer Science and Engineering (Chalmers: DAT235, GU: DIT577) with Ana Bove as examiner. Contact Ana Bove if you would like to be registered to this course. Note that you may not take the class for credit if you already have a result for this course code DAT235/DIT577 (e.g. from a previous iteration of the course). See the course plans at Chalmers and GU

EXAMINATION AND GRADING

To pass the course, students must successfully complete both the quizzes and the project. To pass the quizzes, a student must pass at least 3 out of the 4 quizzes. A quiz is considered passed if the student achieves at least 50% of the total points. To pass the project, students must complete all tasks 1, 2, and 3, present their project in class, meet the requirements for the written report documenting the project, and successfully pass the artifact evaluation.

Notice: The course examiner may assess individual students in other ways than what is stated above if there are special reasons for doing so, for example if a student has a decision from Chalmers about disability study support.

Final Grade:

Grade 3: Passing of quizzes, successful completion of project with the submission of a functional artifact, and delivery of a good report and presentation
Grade 4: Passing of quizzes, successful completion of project with the submission of a functional and reusable artifact, and delivery of a good report and presentation
Grade 5: Passing of quizzes, successful completion of project with the submission of a functional and reusable artifact, and delivery of a strong report and presentation

Definition of functional and reusable for the purpose of this course

Functional:

Is the artifact executable on a unix platform, on the benchmarks reported in the report and beyond?
Is the artifact complete, i.e., are all the results reported in the report replicable?
Is the artifact consistent with the results in the report?

Reusable:

Is the artifact with all dependencies and libraries well-documented?
Does the artifact include a README explaining how the artifact can be used in sufficient detail?
Are suffcient details also provided for the used benchmarks?

Formal Methods for Security