This is the 2022-2023 list of topics for master’s theses (partly) under my supervision at DistriNet/Computer Science, KU Leuven. I’m of course open for individual proposals in embedded security and sustainable ICT. Some of these topics might be a good fit for summer internships with us. I’m also open for students who want to work on technology-and-migration topics.

Sustained Privacy and Security in Cloud-Based Office Solutions

Supervisor

  • Jan Tobias Muehlberg
  • Wouter Joosen

Daily advisor

  • Yana Dimova
  • Shirin Kalantari
  • Lennart Oldenburg (ESAT)
  • Jan Tobias Muehlberg

Description

A large part of the internet economy is funded through advertising networks which rely on collecting consumer data, identifying and tracking consumers over time, and predicting their behaviour in order to display targeted advertisements [1]. The large-scale advertising machinery has generated substantial revenue and produced some of the richest corporations ever to exist, but also spawned concerns over data protection and user privacy from its exploitative practices. More recently, concerns over the environmental impact of user tracking, data collection, and advertising content have been raised [2, 3]. With this thesis project, we aim to quantify planetary impacts with a focus on cloud-based office suites, and compare the footprints of services operated by the main players (advertising- and surveillance-driven, e.g.: Google Mail & Docs, Microsoft Office 360) with services that follow a privacy-by-design approach and offer end-to-end encryption to their users (e.g.: Protonmail, Cryptpad).

The research hypothesis for this thesis is that using advertising- and surveillance-driven cloud-based office service leads to a substantial accumulation of personal data, which demand strong protections that need to be maintained for the long run. Functionally equivalent services with a focus on privacy-by-design reduce the number of long-term assets that require strong protections service-side and thus come with lighter requirements on asset protections and reduced risks in case of data leaks. This may give these privacy-focused services a distinct advantage regarding environmental sustainability but also for sustaining operations and data security, albeit likely requiring different business models.

To start this thesis, you will study literature on data accumulation in cloud-based office solutions (e.g., [4, 5] and the impacts of using this data, e.g., in the context of advertising [2, 3]). In addition, you may measure the actual client-side resource consumption (bandwidth, CPU usage, etc.) of different services under common usage profiles. Combining this with studies on the global trends of environmental impacts of internet services [6] might give us the background and methodology to see if our estimates are coherent with them. Such a comprehensive study may very well reveal that privacy-preserving office solutions are resource-heavy themselves, necessitating a long-term evaluation of the different approaches to sustainably maintain security and privacy of user data [7]. The final challenge then is to put the results in perspective regarding service costs and business opportunities, privacy and security and environmental sustainability, and to envision an operational model that strives to benefit different interests without, e.g., playing out privacy against sustainability.

Relevant research questions for this topic are:

  • Can we compare the footprint and environmental impacts of cloud services based on measuring communication and estimating data accumulation by the service?
  • We can only measure impact at the end user side. How do we estimate the impact of server-side/backend/cloud processing? What existing models would be useful here?
  • How do Privacy-Enhancing Technologies and their footprints correlate with environmental sustainability in the long run? Can we visualise this to raise awareness?
  • To what extent do cloud office solutions follow the criteria for sustainable security from Pavert et al. [7].
  • Are the findings of this study relevant for end users and how can we best communicate the results of the impact assessment, e.g., with visualisations?

Literature

  1. Evans, D.S., 2009. The online advertising industry: Economics, evolution, and privacy. Journal of economic perspectives, 23(3), pp.37-60.
  2. Parssinen, M., Kotila, M., Cuevas, R., Phansalkar, A. and Manner, J., 2018. Environmental impact assessment of online advertising. Environmental Impact Assessment Review, 73, pp.177-200.
  3. Cucchietti, F., Moll, J., Esteban, M., Reyes, P., & Garcia Calatrava, C. (2022). “Carbolytics, an analysis of the carbon costs of online tracking.” Retrieved from http://carbolytics.org/report.html
  4. https://digitalcontentnext.org/wp-content/uploads/2018/08/DCN-Google-Data-Collection-Paper.pdf
  5. https://www.microsoft.com/en-us/microsoft-365/blog/2020/10/29/power-your-digital-transformation-with-insights-from-microsoft-productivity-score/
  6. Freitag, C., Berners-Lee, M., Widdicks, K., Knowles, B., Blair, G.S. and Friday, A., 2021. The real climate and transformative impact of ICT: A critique of estimates, trends, and regulations. Patterns, 2(9), p.100340. https://doi.org/10.1016/j.patter.2021.100340
  7. Pavert, A., Voelp, M., Brasser, F., Schunter, M., Asokan, N., Sadeghi, A.-R., Esteves-Verissimo, P., et al. (2019). “Sustainable Security & Safety: Challenges and Opportunities.” 4th International Workshop on Security and Dependability of Critical Embedded Real-Time Systems (CERTS 2019).

Adding compiler support for hardware-software security defence mechanisms

Supervisor

  • Frank Piessens
  • Jan Tobias Muehlberg

Daily advisor

  • Lesly-Ann Daniel
  • Hans Winderix
  • Marton Bognar

Description

Microarchitectural attacks [1] enable an adversary to infer information about the internal state of a program by observing the execution of that program. For example, an attacker can extract secrets by observing the time it takes a system to perform some computation, or even extract information about the memory access pattern of a victim by observing the state of a shared cache memory. There are multiple ways to prevent these vulnerabilities, and the DistriNet research group has been exploring modifications to processor designs, as well as additional compiler passes that can automatically harden code at compile-time [2]. In this thesis, you will implement compiler support needed by hardware-based security defences that rely on software modifications such as changing the memory layout of the binary, or injecting instructions into the compiled program.

Background

Constant-time programming [5] is a popular defence against microarchitectural attacks used in many cryptographic libraries. It consists in writing a program so that computations on secret data do not impact the execution time or the microarchitectural state (in particular the state of the cache memory). More concretely, a program is constant-time if the sequence of executed instructions and the address of memory accesses are independent of the secret data.

However, reasoning about constant-time only at the source level can miss violations introduced by the compiler [6] or overlook subtleties in hardware design (such as Spectre attacks [7] that additionally exploit processor optimisations). Moreover, writing constant-time code comes with performance costs (especially when considering Spectre attacks). On the contrary, including support from the compiler and the hardware can assist in protecting the code and make defences more efficient.

In the DistriNet research group, we have been exploring modifications to a RISC-V research processor (called Proteus) in order to provide end-to-end security guarantees against microarchitectural attacks. Concretely, developers annotate secret data in the source code, and this information is used by the compiler and by the hardware to provide efficient protection against microarchitectural attacks.

Goal

You will implement compiler support for two hardware security features, which have recently been developed at the DistriNet research group, to protect secret data from microarchitectural attacks. You will extend the LLVM compiler [3] to 1) support annotation of secret variables in C programs, 2) track the propagation of secret data using information flow analysis, and 3) use the result of the information flow analysis to implement support for two hardware-software security defences in the LLVM RISC-V backend.

The first defence requires isolating (annotated) secret data from public data in the memory and, in particular, preventing secret data from being written to the (public) stack due to register allocation or initialisation of local variables. The second defence consists of implementing program transformations to harden code against microarchitectural attacks. In particular, the defence selectively 1) transforms secret-dependent conditional branches to equivalent branch-less code [4], or 2) uses dummy instructions to balance secret-dependent conditional branches.

Approach

This project requires students to have an interest in compilers, low-level security, and computer architecture. During this thesis, you will mostly work on program analysis and compiler transformations, and integrate your program transformations into the popular LLVM code base. You will also learn the theory behind microarchitectural side channel attacks [1] and the constant-time policy [5], a popular defence against these attacks. The research challenge for this thesis topic comes with understanding the tradeoffs between manual annotation and automatisation, and also with understanding to what extent the required analyses offer sufficient precision without compromising soundness. You will be able to evaluate your results through understanding how well the defence works and which programs can be hardened automatically, and also by studying performance aspects of the resulting programs.

Literature

  1. Ge Q, Yarom Y, Cock D, Heiser G. A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. Journal of Cryptographic Engineering. 2018 Apr;8(1):1-27.
  2. Winderix, H., Muehlberg, J. T., & Piessens, F. (2021). “Compiler-Assisted Hardening of Embedded Software Against Interrupt Latency Side-Channel Attacks.” In EuroS&P ’21 (pp. 667–682). Washington, DC, USA. IEEE.
  3. Lattner, Chris, and Vikram Adve. “LLVM: A compilation framework for lifelong program analysis & transformation.” International Symposium on Code Generation and Optimization, 2004. CGO 2004. IEEE, 2004.
  4. Borrello P, D’Elia DC, Querzoni L, Giuffrida C. Constantine: Automatic side-channel resistance using efficient control and data flow linearization. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security 2021 Nov 12 (pp. 715-733).
  5. Almeida, Jose Bacelar, et al. “Verifying Constant-Time Implementations.” 25th USENIX security symposium (USENIX security 16). 2016.
  6. Simon, Laurent, David Chisnall, and Ross Anderson. “What you get is what you C: Controlling side effects in mainstream C compilers.” 2018 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2018.
  7. Kocher, Paul, et al. “Spectre attacks: Exploiting speculative execution.” 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 2019.

Building a precise side-channel finder for Sancus

Supervisor

  • Jan Tobias Muehlberg
  • Frank Piessens

Daily advisor

  • Sepideh Pouyanrad

Description

Side-channel attacks attempt to extract secrets from a program by observing the execution of that program. Several solutions in software and hardware are proposed to protect a system against these vulnerabilities, however, none of the existing techniques were able to remove the leaks completely. We have built a static analysis tool,Side Channel FinderMSP[1], which automatically verifies MSP430 assembly programs to detecting information leakage through novel interrupt-latency attacks (a.k.a. Nemesis [2]), timing side-channels, and undesired information flow. This thesis explores how techniques like symbolic execution-based analysis will improve the accuracy of the SCFMSP in tracking information flow.

Background

Side-channel attacks typically exploit information leaked by computer systems besides regular communication channels. Many side channels have been discovered in the past decades, commonly relying on timing information, power consumption, or caching behaviour of program execution to extract secrets such as cryptographic keys. Effective countermeasures against side-channel attacks are well known in theory, but in practice are challenging to implement properly. Hence, side-channel vulnerabilities continue to be uncovered in real-world security-critical systems. Recent research demonstrates that on embedded platforms with predictable execution times, certain classes of these vulnerabilities can be detected and mitigated automatically by means of language-based security techniques [3].

Recently, we have provided a security type system to statically analyse MSP430 assembly programs to prove the absence of certain information leakage through side channels. We have implemented our approach in a tool, SCFMSP, which automatically verifies MSP430 object-code programs to be free of such vulnerabilities. Like any other program static analysis tool, the SCFMSP is insensitive to the content of registers, and memory cells. More specifically, the entire memory is one unit w.r.t. security levels and only considers immediate values. This thesis aims to extend the SCFMSP with techniques like symbolic execution analysis [5] to address the static analysis limitations. This will help to improve the precision of the program analysis and allow us to correctly track information flow beyond register content and across protection domains provided by Sancus [4], a hardware-only embedded Trusted Execution Environment (TEE). An alternative path for this thesis could be to identify side channel leakage through symbolic execution directly, similar to [6, 7].

This thesis is perfect for you if you have some background or a strong interest in low-level security and computer architecture.

Possible research questions

  • How does symbolic analysis improve the precision of SCFMSP in tracking information flow between registers and protected memory vs. unprotected memory?
  • Can we apply it to a real-world programs, beyond artificial examples?
  • Is it possible to device a more general solution to identify side-channel issues in enclave programs, informed by symbolic execution?

Approach

  • Literature study on recent side-channel attacks in the embedded platform and novel ways to defend against these attacks
  • Obtain background knowledge on Trusted Execution Environments and Sancus
  • Familiarise with the existing static analysis techniques against these attacks
  • Propose an extended SCFMSP combined with Symbolic Execution
  • Implementation
  • Evaluation

Literature

  1. Pouyanrad, Sepideh, Jan Tobias Muehlberg, and Wouter Joosen. “SCFMSP: static detection of side channels in MSP430 programs.” Proceedings of the 15th International Conference on Availability, Reliability and Security. 2020.
  2. Jo Van Bulck, Frank Piessens, and Raoul Strackx. Nemesis: Studying microarchitectural timing leaks in rudimentary CPU interrupt logic. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 178–195. ACM, 2018.
  3. Florian Dewald, Heiko Mantel, and Alexandra Weber. 2017. AVR processors as a platform for language-based security. In Computer Security – ESORICS 2017. Springer, 427–445. https://doi.org/10.1007/978- 3- 319- 66402- 6_25.
  4. Job Noorman, Felix Freiling, Jo Van Bulck, Jan Tobias Muehlberg, Frank Piessens, Pieter Maene, Bart Preneel, Ingrid Verbauwhede, Johannes Goetzfried, and Tilo Mueller. 2017. Sancus 2.0: A low-cost security architecture for IoT devices. ACM Transactions on Privacy and Security (TOPS) 20, 3, Article 7 (September 2017), 7:1-7:33 pages. https://doi.org/10.1145/3079763.
  5. Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C. and Finocchi, I.,
    1. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3), pp.1-39.
  6. Pasareanu, C.S., Phan, Q.S. and Malacaria, P., 2016, June. Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In 2016 IEEE 29th Computer Security Foundations Symposium (CSF) (pp. 387-400). IEEE.
  7. Bao, Q., Wang, Z., Li, X., Larus, J.R. and Wu, D., 2021, May. Abacus: Precise side-channel analysis. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE) (pp. 797-809). IEEE.

Verifying the consistency of security policies across the Kubernetes Stack

Supervisor

  • Wouter Joosen
  • Eddy Truyen
  • Jan Tobias Muehlberg

Daily advisor

  • Gerald Budigiri

Description

Kubernetes is the leading platform for container-based cluster orchestration, which includes support for managing both the cluster infrastructure and the applications running in this cluster as sets of containers. The REST-based Kubernetes API allows to manage the desired cluster and application state by means of creating and removing configuration objects, which are specified as YAML files.

The adoption of Kubernetes has skyrocketed in both the private cloud and public cloud. According to a recent survey of 500 relevant IT professionals [1], its adaption rate has spiked during the Corona pandemic: 68% of the respondents said to have increased their use of Kubernetes during the pandemic in order to achieve faster deployment cycles of their new applications. A quarter of respondents said that they achieved a cost reduction of at least 30% on an annual basis as a result of using Kubernetes.

A weakness of Kubernetes is however security. In the above survey, 54 % of the respondents said that security is the greatest challenge for their organisation. Although Kubernetes already supports cluster infrastructure and application-level security, Kubernetes deployments suffer from security vulnerabilities in the cluster and application state. One of the challenges is that many security policies need to be specified manually by the cluster administrator or application manager.

As such inconsistencies can arise between different security policies due to human error, or even worse security policies are specified incorrectly so that some attack surfaces of the cluster are left unprotected [2]. Formal verification or systematic coverage testing to prove the absence of security vulnerabilities in security policies is therefore of utmost importance, especially in mission-critical domains such as telecommunication, automobile and airplane systems.

Thesis Goal

Security is difficult to handle because it is not implemented by a single system component but by multiple system layers (cloud, clusters, containers, and application code) that each require specific security policies and specific security controllers for enforcing these policies. As a result, cross-layer inconsistencies may arise due to conflicting security policies and the lack of coordination among security controllers.

The goal of this thesis is to use existing formal modelling and verification methods to verify the consistency between security policies across multiple layers of the Kubernetes stack (Kubernetes cluster, and Cloud provider). In particular, the research group DistriNet has already selected two methods, Bitmatrix-based verification [3] and the Z3 SMT solver [4], for achieving this goal:

Research Questions

  • How can we verify the correctness or completeness of the access control model of a specific system layer of the Kubernetes stack?
  • How can we verify the consistency of different access control models across different layers of the Kubernetes stack?
  • How can we reduce the time to conduct the verification and ensure the verification process scales to large applications?

Getting Started

  1. Study of Kubernetes with a focus on security policies that govern interactions between containers
  2. Study of selected methods for formal verification of security policies that are easy to use and can deal with correctness and consistency verification.
  3. Develop the formal system model for specifying access control models within and across system layers of the Kubernetes stack
  4. Develop the verification method for checking consistency between access control models of different system layers
  5. Security validation of the access control models and verification method using a representative cloud-native application (e.g. Software-as-a-Service, Edge computing application)
  6. Performance evaluation of the access control models and formal system using the netperf benchmark [5]

You should have a solid understanding of operating system concepts and programming skills. You shouldn’t be afraid of formal languages and automata. Experience with containers and container orchestration can be helpful.

Literature

  1. https://www.purestorage.com/content/dam/pdf/en/analyst-reports/ar-portworx-pure-storage-2021-kubernetes-adoption-survey.pdf
  2. https://security.stackrox.com/rs/219-UEH-533/images/State_of_Container_and_Kubernetes_Report.pdf
  3. https://ieeexplore.ieee.org/abstract/document/9188284
  4. https://z3prover.github.io/api/html/
  5. https://hewlettpackard.github.io/netperf/

Last modified: 2022-06-08 16:16:25 +0200