hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me
[I added a subject to the thread.] At 2020-01-10T15:19:17+0300, abdi mahmud haji wrote:
hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me
Hi Abdurahman, The short answer is that you'll need to write or obtain a lot more infrastructural components before you can put anything resembling a Unix shell, or even an old-fashioned MS-DOS prompt, on top of the seL4 microkernel. Here's a longer answer. If you study operating systems or systems programming you will become aware of a great many services that are provided by a fully-fledged "OS personality" (like Unix or Windows NT), and the standard libraries of a programming language. There is a great deal just to the C standard library as set forth by the ISO, and the Austin Group's POSIX standard is even thicker. Most of what is described there, like string-handling functions, dynamic memory allocation, date and time services, signal handlers, Unix processes, terminal I/O, filesystems, and much more is stuff that doesn't need to be in a microkernel. What does not need to be in a microkernel does not go into seL4; as Jochen Liedtke, lead developer of the L3 and L4 microkernels, put it: "A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e., permitting competing implementations, would prevent the implementation of the system's required functionality."[1] The Linux, *BSD (including Darwin), and Windows NT kernels are all immensely bloated by this standard. The Mach microkernel, an attempt to do a leaner Unix kernel in the 4.3BSD era (the 1980s), did not follow it and harmed the reputation of microkernels for a generation. (Admittedly, Liedtke articulated his principle in 1995, in retrospect at the relative failure of Mach.) When you also consider the fact that seL4 is designed for system implementers who want strong isolation guarantees between programs hosted on it, anything like a traditional Unix shell starts to make less sense. A Unix command like "ps" might not make very much sense, as the mere presence of other processes on the system should not be observable except by explicit intention. seL4 lacks even the concept of a "root" or administrative user who gets to override the privacy protections of unprivileged users. Instead seL4 has only specific capabilities; a superuser who has all capabilities is a tempting target for attacks on security, so seL4 does not implement one. That said, for design and debugging purposes, as well as educational purposes to help people learn the system, a shell-like monitor for seL4 might be a good idea. It's something I'd like to see. But it would probably not feel very familiar to a Unix (or even Windows CMD.EXE) user. Gernot Heiser, one of the lead designers of seL4, has told me that the kernel's API is designed to be virtualizable, in the sense that you could design and configure a system that interposed a layer between the seL4 kernel and threads running on it; this layer could perform logging operations, do event reporting through a serial device, or even supply a shell/monitor that permitted interactive exploration of the system. My instinct is that such a thing would be highly useful for learning one's way around the system and designing applications for it. Then, when you went to production builds, the interposed layer could be disabled, reducing the system's memory footprint, improving performance, and restoring information-flow properties that monitoring is, in part, designed to violate. It takes some time to get "microkernel brain", as I call it. Keep asking questions--this community is happy to try answering them. Regards, Branden [1] https://en.wikipedia.org/wiki/L4_microkernel_family
On Fri, Jan 10, 2020 at 1:36 PM G. Branden Robinson
[I added a subject to the thread.]
At 2020-01-10T15:19:17+0300, abdi mahmud haji wrote:
hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me
Hi Abdurahman,
Hi all, I'm not really affiliated with the sel4 project, but also wanted to chime in on the subject. I don't think enough ink has been spilled on it. Branden's response focused on a lot of things which don't belong in the microkernel itself, and I totally agree. I want to focus on designs for a "native" shell for a capability system rather than anything which is going to be resembling a posix shell. There is a picture here, on page 24 describing the various trust layers involved in the eros-os shell mechanism[1]. [1]:( https://www.cl.cam.ac.uk/teaching/2003/AdvSysTop/Capabilities.pdf ) This implements what i'm going to call a "pull model". The green Open/Save agent represents a power box, and the arrows from the red applications have a reference to this capability through which they request resources. Through this mechanism, you basically just start up the process, and give it that power box reference. At this point the program becomes something akin to it's own sub-shell through which it acquires arguments. This saves the shell(or user) from having to know about each message expected by the process, and the contents of each capability register. This would be what i'll call the "push model". In the push model we could even drop the powerbox, and the shell sends messages to the red process, perhaps without even a way for the process to send messages back to the shell. I think from the perspective of sel4, we can consider what he calls "SystemTCB" would correspond to sel4's "root process". The green window system, being IO. The simplest directory being an array or vector of (string, capability) pairs. For the green "Window system", i'm considering this basically nothing fancier than a terminal IO multiplexer. That is it's the thing receiving keyboard interrupts, which has some control mechanism for switching which process is currently receiving input. eTerm seems to be the process receiving input from the Window system for the shell. This is likely because eros did not have asynchronous notifications, and so you needed to spin up another process to avoid the shell being blocked, with sel4 we can likely roll this process into shell directly (with async notifications), maybe there is a reason to keep it separate that I can't think of. Using the pull model it would seem you greatly simplify the shell itself, that complexity ends up in the input/output interaction. Where the user is now interacting with multiple processes (the shell, powerbox, and untrusted process). I'm sorry this is all rather hand wavy, I have in the past had a go at implementing a simple terminal multiplexer for "Window system", It's not compiling with recent sel4's, but can have a go at updating it if that is of any help. There may even be one available in sel4 repositories somewhere by now, i am not sure. In my opinion starting out with the pull model is the quickest way to a working shell, interleaving output from each process into the output stream, and switching which application has the input cursor during program startup/option specification/argument passing, between shell/program/powerbox. Which tends to reflect how graphical applications run, formatting messages to themselves and calling system API's for filesystem dialogs. a "native" shell for systems like sel4 might be a very different beast than a unix-like shell which only ever passes arguments through initial argv. But in a system like sel4 it should be no problem to startup programs with zero, or only potential access to request capabilities, before we even know which arguments to pass it -- relegating the shell to starting up all programs with the same startup sequence. This doesn't actually give you any form of persistence/filesystem for our directory capability, but that is a whole other topic, and you can implement a shell without it. This has probably gotten too long, there is lots of details missing, like how we get such a thing to resemble the familiar interface a shell provides. It would probably also be helpful if i tried to write it in a non-email format where I could embed diagrams and the like, for visualizing the separate models independently of one another. But let me if I can clarify things or how I can help.
Thanks Banden and Matt. Raising the level of abstraction of the discussion somewhat, I’d say that the traditional notion of a “shell” is really a command-line interface (aka primitive UI) to an OS’es syscall interface. This is certainly how the Unix shell started out (before it was turned into a full programming language and the kitchen sink). Viewed that way, it’s clear that such a minimalist notion of a shell makes not much sense for a microkernel like seL4. Having a US to deal with raw caps doesn’t buy you much, and besides, you don’t even have the system services to implement that UI. Hence, you need a layer of system services between the shell and the kernel. You’ll want at least a process concept, a concept of I/O (which in seL4 doesn’t exist at all) and communication that’s more than a few raw bytes and caps. In short, you need a minimal OS personality. Matt has outlined one way to do it. Our Advanced OS course (https://www.cse.unsw.edu.au/~cs9242/19/project/) builds a simple OP personality on seL4, and a shell to drive it. That shell looks quite different from what Matt’s shell would look like. Basic observation is then that a shell will be strongly tied to the OS personality on which it is based, and that OS personality will define a whole lot of policies on how the system and its resources are managed. In that sense, there cannot be a unique “seL4 shell”. But for any OS personality you build, you’d almost certainly want a shell. Gernot PS: This is probably one for our FAQ...
participants (4)
-
abdi mahmud haji -
G. Branden Robinson -
Heiser, Gernot (Data61, Kensington NSW) -
Matt Rice