A type system for security and privacy

Potential supervisors: 
Description: 

How does one write programs that are secure and private by design?

This is the goal of language-based security, where programming tools such as compilers, type systems, and runtime systems are used to enforce security and privacy of programs. Many such tools are based on the idea of information flow control (IFC). Data is tagged with labels, such as "private" and "public", and the IFC mechanism is used to stop sensitive data from flowing between incompatible domains (e.g. from "private" to "public"). Traditionally, IFC has focused mostly on security applications, with the goal of stopping sensitive data from being leaked outside of a system (e.g. a hacker should not be able to download your social network posts). The goal of this project is to develop a prototype language that uses IFC principles to control the private flow of data within a secure application (e.g. the network should not be able to use your geo-location for unwanted advertising).

The project builds on existing principles from language-based security and IFC as well as a prototype language for language-based privacy.

There is a number of open problems to work on, depending on your interests:

  • programming a proof-of-concept implementation of the language as a library (e.g. in Haskell, Scala or Agda);
  • extending an existing IFC language or library with new privacy primitives (e.g. in Java, Haskell, Scala, etc.);
  • developing and mechanizing the theory/logic underlying the privacy type system (e.g. in Agda or Coq);
  • other tasks are possible (to be decided together with the supervisor).

Prerequisites. Depending on the tasks you want to work on, it is desirable (but not necessary) to have

  • familiarity with a functional programming language (e.g. Haskell, Agda, Scala);
  • familiarity with an existing IFC language or system (e.g. Jif, MAC, etc.);
  • taken the Types for Programs and Proofs course (DAT350 / DIT233);
  • taken the Language-based Security (TDA602 / DIT101) course.

If you have questions, do not hesitate to contact me: sandros (at) chalmers (dot) se.

 

Date range: 
June, 2021 to December, 2022