E-mail senden E-Mail Adresse kopieren
Forschungsgruppenleiter:in

Hamed Nemati

E-Mail

Adresse

450 Jane Stanford Way
94305 Stanford (United States)

Gruppenmitglied in

Kurzbiografie

I am an Independent Research Group Leader at the Helmholtz Center for Information Security (CISPA). Prior to this, I was a Post-Doctoral researcher at CISPA working in the Secure & Privacy-friendly Information Processing group lead by  Prof. Michael Backes. I did my PhD in computer science at the School of Computer Science and Communication at Royal Institute of Technology (KTH) under Prof. Mads Dam. My research interests include security of systems software, formal methods and program logics, interactive theorem proving and machine code analysis.

CV: Letzte vier Stationen

September 2019 - now
Research Group Leader at CISPA
2017 - 2019
Post-Doc at CISPA
2012 - 2017
PhD student at KTH Stockholm

Veröffentlichungen von Hamed Nemati

Jahr 2022

Konferenz / Medium

CCS
Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS ’22)CCS 2022

Konferenz / Medium

ISCA
{ISCA} '22: The 49th Annual International Symposium on Computer ArchitectureThe 49th International Symposium on Computer Architecture.

Jahr 2021

Konferenz / Medium

MICRO
54th Annual IEEE/ACM International Symposium on MicroarchitectureMICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, Virtual Event, Greece, October 18-22, 2021

Konferenz / Medium

USENIX-Security
30th USENIX Security Symposium (USENIX Security '21)30th USENIX Security Symposium (USENIX Security '21)

Konferenz / Medium

CSF
IEEE Computer Security Foundations Symposium34th IEEE Computer Security Foundations Symposium

2021-05-23

Input Algebras

Konferenz / Medium

ICSE
International Conference on Software Engineering (ICSE)International Conference on Software Engineering (ICSE)

Jahr 2020

Konferenz / Medium

ESORICS
25th European Symposium on Research in Computer Security, {ESORICS} 2020Computer Security - ESORICS 2020 - 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II

Konferenz / Medium

CAV
Computer Aided Verification - 32nd International ConferenceComputer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I

Konferenz / Medium

TAP
Tests and Proofs - 14th International ConferenceTests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings postponed

Lehre von Hamed Nemati

Winter 2021/22

Formal Methods in Security

Despite decades of research in computer security, security vulnerabilities still plague computer systems with an ever-growing number of new vulnerabilities discovered every day. How can we ensure that computer systems are really secure? Formal methods offer a promising approach towards this goal: they can guarantee the absence of specific security vulnerabilities with mathematical certainty and therefore help us develop mode reliable systems.

In this course, we will study how formal methods can be applied to verify that the design and implementation of computer systems respect their intended security policies. The course is structured in three independent parts, which focus on specific techniques for different domains: language-based information-flow control, security protocols, and system-level verification. As a whole, the course will give you hands-on experience in reasoning about security at different layers of abstraction through established principled techniques and a broad introduction to state-of-the-art research in the area.

Topics and Instructors

  1. Introductory Lecture (20 October 2021)  
    We'll give an overview of the three parts. Marco will give it live (find the zoom link in the calendar entry, calendar link is below -- not in the CMS timetable). Hamed and Robert prepared videos for the occasion given their travel obligations:
     - Hamed's Video: https://dl.cispa.de/s/8Z5kbp8yifL7tsg
     - Robert's Video: https://dl.cispa.de/s/LJFsXzfr8xWoT7Y
    - Class Recording: https://dl.cispa.de/s/ZMT3oCqPTyxgHcd

  2. Language-based Information-Flow Control (Marco Patrignani

    In the first part of the course, we will study information-flow control techniques that track how data flows in a program to enforce data confidentiality and integrity. We will discuss both static and dynamic IFC techniques based on security type systems and taint tracking, as well as techniques that track data flows in a program at a different granularity (for example per program variable or per program block). Finally, we will see how programming languages principles can be applied to formally verify that these techniques enforce security. Basic knowledge of programming languages theory is preferred, but not required.

  3. Proof techniques for system verification (Hamed Nemati)

    The main goal of the second part of this course is to show you how we should approach verification of large scale  systems like  micro-kernels and hypervisors. This is a very challenging task in practice. We will study abstraction, decomposition and refinement as techniques that usually used in practice to facilitate verification of such systems. Finally, in our last lecture we see how we can combine fuzzing and formal verification to validate systems that their verification is not feasible in practice.  

     

  4. Protocol Verification (Robert Künnemann)
    Protocol verification assumes that the cryptography is perfect and tries to ensure that they are used correctly. It is not about defending against super smart mathematicians exploiting biases in key streams, but equally smart hackers confusing one party about the state of another party.

    We will discuss how to get from the Alice-bob notation to a minimalistic, precise specification of the protocol and its setup

    how to formulate our security requirements and how to verify that these requirements hold, using tools that have by now reached an impressive degree of automation.

Organization

Registration: open now! (Once you are registered here, don't forget to register in the LSF.)

When: Wed 10h-12h (official starting time is 10:15)

Where: (all links also appear in the calendar events)

Calendar & Lecture planlink (Click "..." next to calendar for subscription link for your favorite application) (work in progress)

Mode:

  1. IFC (Marco): Zoom+Miro lectures on Wednesday 10-12, Q&A session on Friday 10-12 based on the askbot content (see IFC page)
  2. SYSV (Hamed): flipped classroom: recorded lectures on Monday, Q&A session on Wednesday.
  3. PROTO (ROBERT): live lectures on Wednesday 10-12, Q&A session on Friday 10-12, detailed lecture script.

Exam requirements: three exercise sheets per part, 50% of total points, work in groups allowed

Exam: two oral exams (first and second part), and one project (third part). Passing requirement is >4.0 on two of the three.

Official exam date : tbd.

Course Goals

  • Understand the challenges of some open problems in computer security

  • Learn state-of-the-art techniques to address these problems and how to apply them (as a programmer, protocol designer, web developer etc.)

  • By-product: a taxonomy of where things can go wrong in security on different layers

Learning Objectives

After the course, students will be able to:

  • Apply Information-Flow Control (IFC) techniques to the design of secure programming languages.

  • Analyze the security guarantees of IFC languages through programming languages principles.

  • Discuss problems, solutions, and open challenges presented in IFC research papers.

  • Understand fundamental concepts in verification. 

  • Learn how to use formal techniques to find vulnerabilities in low-level systems.

  • Gain knowledge to be able to read and understand papers in system verification.

  • Model protocols and cryptographic assumptions in the applied-pi calculus.

  • Express authentication and secrecy properties via correspondence and reachability.

  • Exploit automated tools to verify protocols.

Target Audience

Mainly M.Sc students and interested graduate students. Interested and motivated B.Sc students should contact us and argue that (a) they are particularly interested and (b) they have the necessary background in logical reasoning to follow the course.