You need to take the following steps to sign up for the capstone sequence:
Many organisations run business applications on server-class machines, with the applications themselves implemented using several loosely-coupled components that run across many machines. With ever growing threats to cyber infrastructure, it is paramount to ensure that each component complies with security policies, for example policies which require that applications act within the capabilities and limitations of the principals that they represent. For example, only an authenticated user of a bank application can initiate a transaction that changes an account balance. Today, ensuring such compliance can be tedious, manual, error prone, and the processes are often unable to keep up with the dynamism in the software and the deployment environment.
This project explores the design of (i) a language to specify a wide range of security policies regarding the interactions between application components and the outside world (for example, anything involving system calls, network communication, and so on), along with (ii) run time mechanisms to enforce such policies through emerging kernel instrumentation technology (eBPF). Further, the project will (iii) evaluate the performance overheads of such enforcement mechanisms, and (iv) implement ways to reduce these overheads.
The operating system kernel is critical infrastructure for computing. It is often desirable to enhance kernel software to implement novel and experimental features, such as new system profilers, runtime security enforcement mechanisms, optimised network transport protocols, and process schedulers. Today, such enhancement is often carried out through a verified kernel extension mechanism, eBPF. In eBPF, users can write high-level programs that extend kernel functionality. The program is first checked by an in-kernel _verifier_ to ensure that the program is safe run in kernel context, e.g., the program does not crash the kernel or corrupt kernel memory. Once checked, the program can be incorporated into an already running kernel with native high performance.
Unfortunately, the kernel verifier itself has had bugs in the past, which has led to the development of high-severity exploits using eBPF. This project is part of a larger effort to check the correctness of key properties of the in-kernel verifier. Specifically, this project will (i) design and develop new software pipelines to check the soundness of the verifier, building on our existing framework, (ii) perform a rigorous comparative performance evaluation of different logic solvers which are integral components of these pipelines, and (iii) time permitting, extend our results to parts of the verifier not previously considered, enabling us to provide guarantees for a larger class of eBPF programs.
Is it possible to automatically optimize program performance while ensuring that the program is safe to run? This question is particularly important for a class of software called kernel extensions -- software written to extend operating system kernels like Linux -- and run in settings that are both safety and performance-sensitive. Classic approaches to improving program performance, such as using optimizing compilers (like gcc or clang), leave performance improvements on the table, since they take a conservative approach that avoids safety risk at all costs. This project will explore new algorithms and rigorous evaluation methods to optimize program performance with safety guarantees for kernel extensions.
Homomorphic encryption allows computation to be performed on encrypted data without the need for decryption. It can be used for privacy preserving computation allowing the data to be encrypted both in transit and during compute on a cloud device. Although the community has made substantial progress, it still has several orders of magnitude overhead compared to a regular computation. The goal of this project is to explore the sources of overhead, design transformations, accelerators, and verification techniques to both make homomorphic encryption practical and provably correct.
Project Description
Note: The description includes citations with DOI (Digital Object
Identifier) that can be converted to URLs by prefixing with
"http://doi.org/"
For example, the DOI "10.3390/life12050759"
transforms to the URL
http://doi.org/10.3390/life12050759
Prof. Olson is not accepting any more students
Project Description
Note: The description includes citations with DOI
Prof. Olson is not accepting any more students
Project
Description
Note: The description includes citations with DOI
Prof. De is not accepting any more students
(You can see the projects that students worked on in 2022-23 here)