OSWebSec: Exokernels - Revision history

Falaca: /* Formal proof */

2012-10-17T18:20:19Z

Formal proof

← Older revision		Revision as of 18:20, 17 October 2012
Line 15:		Line 15:
	===Formal proof===		===Formal proof===
	The authors made some big compromises in order to make a formal proof for their exokernel possible:		The authors made some big compromises in order to make a formal proof for their exokernel possible:
	* They restricted themselves to a subset of the C language		* They restricted themselves to a subset of the C language (e.g., no function pointers)
	* Gimped concurrency		* Gimped concurrency
	* Interrupt handling		* Interrupt handling

Falaca: /* Portability */

2012-10-17T18:19:03Z

Portability

← Older revision		Revision as of 18:19, 17 October 2012
Line 6:		Line 6:
	Portability is a major concern with exokernels: In addition to the work required to port the exokernel to different hardware, you also have to port all programs to it since the exokernel provides a different API depending on what hardware it is running on.		Portability is a major concern with exokernels: In addition to the work required to port the exokernel to different hardware, you also have to port all programs to it since the exokernel provides a different API depending on what hardware it is running on.

	The goal of exokernels was to make the system minimal, but at the end of the day you end up adding onto it and providing things like POSIX semantics anyway.		The goal of exokernels was to make the system minimal, but at the end of the day you end up adding onto it and providing things like POSIX semantics anyway, and therefore introducing vulnerabilities into your system.

	Extensibility is mentioned as a key advantage of exokernels, but modern OSs are quite extensible anyway: You can write kernel modules/device drivers, file systems, etc.		Extensibility is mentioned as a key advantage of exokernels, but modern OSs are quite extensible anyway: You can write kernel modules/device drivers, file systems, etc.

Falaca at 18:17, 17 October 2012

2012-10-17T18:17:43Z

← Older revision		Revision as of 18:17, 17 October 2012
Line 1:		Line 1:
	[[File:ExterminateHWAbstractions.jpg]]		==Exokernels==

			[[File:ExterminateHWAbstractions.jpg\|thumb\|Key idea of Engler et al. in ''Exokernel: an operating system architecture for application-level resource managementp'']]

			===Portability===
			Portability is a major concern with exokernels: In addition to the work required to port the exokernel to different hardware, you also have to port all programs to it since the exokernel provides a different API depending on what hardware it is running on.

			The goal of exokernels was to make the system minimal, but at the end of the day you end up adding onto it and providing things like POSIX semantics anyway.

			Extensibility is mentioned as a key advantage of exokernels, but modern OSs are quite extensible anyway: You can write kernel modules/device drivers, file systems, etc.

			===Exokernels for what?===
			The authors mention that many of the hardware abstractions offered by the kernel end up slowing down some specialized applications. But for a monolithic kernel this is no problem: You can just add APIs for specialized tasks to reduce overhead. So who exactly will go through all the pain of using an exokernel, when they can just take an open source OS like Linux and modify it to suit their needs?

			===Formal proof===
			The authors made some big compromises in order to make a formal proof for their exokernel possible:
			* They restricted themselves to a subset of the C language
			* Gimped concurrency
			* Interrupt handling
			* Memory allocation (none)

			They designed their kernel for uniprocessor systems. How do you verify a multi-threaded kernel? Even without verification, modern kernels took '''a lot''' of work to reach a state where they work correctly.

			==Microkernels==
			Microkernel subsystems depend on each other to get things done. There are too many tightly coupled services passing around too much data. Compromising one component can allow you to compromise others. ''Where's the win?''

			All optimizations that are done to improve microkernels can also be done to monolithic kernels. In class we discussed [http://en.wikipedia.org/wiki/OpenBinder, binder], an IPC system originally designed for microkernels, which has now been implemented for Linux and is used in Android.

			==Microkernels vs. Exokernels==
			Exokernels appear as hardware to the applications running on it, whereas microkernels provide abstractions.

			Some barriers (e.g., user/kernel space) are natural, others aren't. If you try to create barriers where it doesn't make sense to do so, you simply end up breaking too many holes through them make things work correctly. From a security perspective, this brings you back to the same situation you started with because of all the holes that you've created.

Falaca: Created page with "File:ExterminateHWAbstractions.jpg"

2012-10-11T01:48:57Z

Created page with "File:ExterminateHWAbstractions.jpg"

New page

[[File:ExterminateHWAbstractions.jpg]]