Thesis Topic Details

Topic ID:
3342
Title:
Port Google Go to seL4
Supervisor:
Gernot Heiser
Research Area:
Operating Systems, Programming Languages
Associated Staff
Assessor:
Kevin Elphinstone
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP9242 or outstanding result in COMP3231, strong programming skills
Description:
Google Go is a small but managed programming language. It is type- and memory-safe, has a syntax based on C but is aims to support concurrent programming and as such has constructs similar to Ada.

These features make it suitable for programming high-assurance systems, particularly in combination with a high-assurance operating system and run-time environment.

This opportunity exists with the formally-verified seL4 microkernel, which provides a rock-solid foundation for software, Porting Go, particularly its lightweight "native" run-time, to seL4 is the first step towards making this a reality. It may enable verification of the small run-time, and thus provide a programming environment of unprecedented dependability.
Comments:
--
Past Student Reports
  Andrew Alexander REIMERS in s2, 2013
Port Google Go to seL4
 

Download report from the CSE Thesis Report Library

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