Thesis Topic Details

Topic ID:
3343
Title:
Preventing cache-based covert channels without flushing
Supervisor:
Gernot Heiser
Research Area:
Operating Systems
Associated Staff
Assessor:
Kevin Elphinstone
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP9242 or outstanding result in COMP3231
Description:
Caches, like other shared hardware, present a potentially high-bandwidth covert timing channel. The normal approach to preventing this channel is to flush all caches on every context switch. As context switches are frequent in microkernel-based systems, this mitigation strategy has a desastrous performance impact.

This project is to explore an alternative approach to flushing, namely preventing sharing of the cache. This is made possible by a unique aspect of the design of seL4, which separates kernel data similarly to user data, and has almost not shared kernel data structures (a covert channel analysis of those shared kernel data structures is subject to a different project).

Specifically, page colouring can be used to partition the L2 cache between two security compartments so that they never use the same cache line. Cache pinning can be used to achieve the same for the L1 D-cache, both are straightforward. Sharing of I-cache lines can be prevented by replicating the kernel code, so that each partition executes its own copy of kernel instructions, and using cache pinning to keep them separate. This part requires careful design to get right (e.g. how do you boot?)
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.