Formal Methods for Security

The course can be part of the following programmes:

1. Computer Science, Master's Programme (N2COS)

A Bachelor degree in computer science or a related subject.

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, and allow for automated verification to detect flaws that may be overlooked by traditional testing. By applying formal techniques such as model checking, and theorem proving, and using formal specification languages, developers can build systems with provable security guarantees. The course consists of a series of lectures on different formalisms and verification methods that have been developed to reason about security and privacy properties.

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

Knowledge and understanding

• Explain the role of formal methods in specifying and verifying security-critical systems

Skills and abilities

• Formally define and reason about key security and privacy properties using formal specification languages
• Use automated verification tools to verify compliance with security policies and detect potential vulnerabilities

Judgement ability and approach

• Critically assess the strengths and limitations of various formal techniques.

The course includes lectures and a project component. The lectures include a compulsory part in the form of quizzes. The project work entails implementing and experimenting with topics related to concepts introduced in the course. Completing and presenting the project, writing a report, and taking part in a code-review session is compulsory.

Language of instruction: English

Passing the course requires:

1. Passing quizzes
2. a passable individual contribution to the project including:
   • Implementation
   • Presentation
   • In-person code review
   • Submission of written report documenting the project

If a student who has been failed twice for the same examination element wishes to change examiner before the next examination session, such a request is to be granted unless there are specific reasons to the contrary (Chapter 6 Section 22 HF).

If a student has received a certificate of disability study support from the University of Gothenburg with a recommendation of adapted examination and/or adapted forms of assessment, an examiner may decide, if this is consistent with the course’s intended learning outcomes and provided that no unreasonable resources would be needed, to grant the student adapted examination and/or adapted forms of assessment.

If a course has been discontinued or undergone major changes, the student must be offered at least two examination sessions in addition to ordinary examination sessions. These sessions are to be spread over a period of at least one year but no more than two years after the course has been discontinued/changed. The same applies to placement and internship (VFU) except that this is restricted to only one further examination session.

If a student has been notified that they fulfil the requirements for being a student at Riksidrottsuniversitetet (RIU student), to combine elite sports activities with studies, the examiner is entitled to decide on adaptation of examinations if this is done in accordance with the Local rules regarding RIU students at the University of Gothenburg.

Sub-courses

1. Project, 6 credits
   Grading scale: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U)
2. Quiz, 1,5 credits
   Grading scale: Pass (G) and Fail (U)

The grading scale comprises: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U).

• Grade 3: Passing of quizzes, successful completion of project with the submission of a functional artifact, the delivery of a good report and presentation, and passing a code review
• Grade 4 and 5: in addition to the criteria stated for Grade 3, these grades will be granted based on the quality of implementation, results, presentation, and report.

The course is evaluated through meetings both during and after the course between teachers and student representatives. Further, an anonymous questionnaire is used to ensure written information. The outcome of the evaluations serves to improve the course by indication which parts could be added, improved, changed or removed.

The course is a joint course together with Chalmers.

To attend the course, we recommend having completed one of the following courses:

• Formal Methods for Software Development
• Logic in Computer Science