Backwater
From AWiki
Contents |
What is Backwater?
Backwater is an experimental operating system kernel whose interesting parts are written in the Tamed Pict programming language. That language was developed by Benjamin C. Pierce and David N. Turner.
More information concerning this kernel:
The main goal is to design and prototype a monolithic kernel that is robust. If it sounds as an oxymoron to you then check out capability-secure languages. We do not need "security" mechanisms provided by hardware designers at all. In fact, using proper programming languages enables us to enforce any describable security policy over untrusted components.
Related documents
- Taming of Pict. SOFSEM 2008
- Concerning Untrusted Code. IIT.SRC 2007.
Related Discussions
January 2007: powerboxed device drivers; language-based or OS based capablities?
April 2007: Backwater, some small progress
Some Simple Demos
- Sandboxed ClockMorph --- Untrusted component running sandboxed in kernel-space.
- Sandboxed ClockMorph and GameOfLifeMorph --- More untrusted components running sandboxed in kernel-space.
Do you want to run it?
Appendix A of the Backwater documentation describes how to compile and boot this experimental kernel. Both, in QEMU virtual machine and on the bare hardware.
Related Dissertations
- David N. Turner: The Polymorphic Pi-calculus: Theory and Implementation, 1995
- Mark Samuel Miller: Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control, 2006
Related Projects
Robust operating systems based on OS-based capabilities
Robust operating systems based on language-based security
Also interesting:
Other efforts:
