[seL4] Re: A few questions regarding seL4
On Tue, 28 Nov 2023 at 07:52, Gernot Heiser via Devel wrote: > On 28 Nov 2023, at 12:43, Benjamin J. Kelly > wrote: > > > > Forgive me for thinking out loud here but I think that a unikernel > application is simply a monolithic application with zero or minimal > traditional OS system calls, i.e., an application that runs 100% (or very > near it) in User Space. If seL4 is used as a highly secure > scheduler/executive then there should be no issues I can see with seL4 > scheduling 'unikernel' apps. > > Sorry, forgot to add the link: > https://trustworthy.systems/publications/abstracts/Elphinstone_ZMH_17.abstract > > Gernot > ___ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems > What I meant is that making a unikernel in firmware with seL4 will be difficult due to its inherent design. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: A few questions regarding seL4
On 28 Nov 2023, at 12:43, Benjamin J. Kelly wrote: > > Forgive me for thinking out loud here but I think that a unikernel > application is simply a monolithic application with zero or minimal > traditional OS system calls, i.e., an application that runs 100% (or very > near it) in User Space. If seL4 is used as a highly secure > scheduler/executive then there should be no issues I can see with seL4 > scheduling 'unikernel' apps. Sorry, forgot to add the link: https://trustworthy.systems/publications/abstracts/Elphinstone_ZMH_17.abstract Gernot ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: A few questions regarding seL4
On 28 Nov 2023, at 12:43, Benjamin J. Kelly wrote: > > Forgive me for thinking out loud here but I think that a unikernel > application is simply a monolithic application with zero or minimal > traditional OS system calls, i.e., an application that runs 100% (or very > near it) in User Space. If seL4 is used as a highly secure > scheduler/executive then there should be no issues I can see with seL4 > scheduling 'unikernel' apps. In fact, it’s been done (quite a while ago, in fact). Gernot ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: A few questions regarding seL4
Pritvi, Thank you for your prompt response. Forgive me for thinking out loud here but I think that a unikernel application is simply a monolithic application with zero or minimal traditional OS system calls, i.e., an application that runs 100% (or very near it) in User Space. If seL4 is used as a highly secure scheduler/executive then there should be no issues I can see with seL4 scheduling 'unikernel' apps. Very Respectfully, Benjamin J. Kelly President Windsor Lake Computing LLC http://windsorlake.llc/ Sent with [Proton Mail](https://proton.me/) secure email. On Wednesday, November 22nd, 2023 at 7:54 AM, Jheengut Pritvi wrote: > Hi Ben, > > Firstly, I do not believe that unikernel is possible with a microkernel like > seL4. > > Secondly, seL4 is a mathematically proven secure OS with good performance, a > lot of research must be performed to push the performance. > > Thirdly, from a firmware point of view, how do you intend to manage storage > of a web server if it is a dynamic one. > > Fourthly, do you intend to install seL4 on a server firmware like libreboot? > > Fifthly, you can scroll down the announce@sel4.systems seL4 Mailing list to > find companies who might be interested. > > Pritvi Jheengut > > On Fri, 17 Nov 2023 at 03:55, Benjamin J. Kelly > wrote: > >> To Whom It May Concern, >> >> My name is Ben Kelly. Myself and my partner James Briscoe - CC'd on this >> email - are in the beginning stages of starting a company that will host >> websites and web services for clients requiring high security on hardware >> that we control from the firmware up. We haven't decided which OS we want to >> use yet. Our initial goal is a customizable OS that contains only the >> minimum services to host a web server and nothing else. We will be >> evaluating the seL4 Microkernel. >> >> We're also intrigued by the possibilities of enhanced application >> performance and security that can be had from a unikernel approach. >> >> Is there anything that would forbid using the seL4 MicroKernel acting as a >> 'hypervisor/scheduler' for highly isolated and performant unikernel >> applications? >> >> If not, seL4 and Unikernel technology could potentially deliver the maximum >> amount of performance and security possible for hardware running >> seL4-compatible CPUs. >> >> In the following video Boyd Multerer, >> https://youtu.be/YG5BaoB24eA?si=TcxHq51Q5HLC0m1_ was asked the question if >> seL4 would "make sense on servers." Boyd replied that "I think it would but >> it's not something that we are targeting ... yet." He also said that "Yeah, >> I do think seL4 would be perfect at the bottom of the server once the >> multi-core thing gets figured out. But we don't need to solve that right >> away." Do you think seL4 is mature enough for our purpose? If we were to >> invest our time doing a deep dive into understanding seL4 do you know of any >> companies that are willing to pay for our acquired knowledge? >> >> Very Respectfully, >> >> Benjamin J. Kelly >> President >> Windsor Lake Computing LLC >> http://windsorlake.llc/ >> >> Sent with [Proton Mail](https://proton.me/) secure email. >> ___ >> Devel mailing list -- devel@sel4.systems >> To unsubscribe send an email to devel-leave@sel4.systems ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: A few questions regarding seL4
Hi Ben, Firstly, I do not believe that unikernel is possible with a microkernel like seL4. Secondly, seL4 is a mathematically proven secure OS with good performance, a lot of research must be performed to push the performance. Thirdly, from a firmware point of view, how do you intend to manage storage of a web server if it is a dynamic one. Fourthly, do you intend to install seL4 on a server firmware like libreboot? Fifthly, you can scroll down the announce@sel4.systems seL4 Mailing list to find companies who might be interested. Pritvi Jheengut On Fri, 17 Nov 2023 at 03:55, Benjamin J. Kelly wrote: > To Whom It May Concern, > > My name is Ben Kelly. Myself and my partner James Briscoe - CC'd on this > email - are in the beginning stages of starting a company that will host > websites and web services for clients requiring high security on hardware > that we control from the firmware up. We haven't decided which OS we want > to use yet. Our initial goal is a customizable OS that contains only the > minimum services to host a web server and nothing else. We will be > evaluating the seL4 Microkernel. > > We're also intrigued by the possibilities of enhanced application > performance and security that can be had from a unikernel approach. > > Is there anything that would forbid using the seL4 MicroKernel acting as a > 'hypervisor/scheduler' for highly isolated and performant unikernel > applications? > > If not, seL4 and Unikernel technology could potentially deliver the > maximum amount of performance and security possible for hardware running > seL4-compatible CPUs. > > In the following video Boyd Multerer, > https://youtu.be/YG5BaoB24eA?si=TcxHq51Q5HLC0m1_ was asked the question > if seL4 would "make sense on servers." Boyd replied that "I think it would > but it's not something that we are targeting ... yet." He also said that > "Yeah, I do think seL4 would be perfect at the bottom of the server once > the multi-core thing gets figured out. But we don't need to solve that > right away." Do you think seL4 is mature enough for our purpose? If we were > to invest our time doing a deep dive into understanding seL4 do you know of > any companies that are willing to pay for our acquired knowledge? > > Very Respectfully, > > Benjamin J. Kelly > President > Windsor Lake Computing LLC > http://windsorlake.llc/ > > Sent with [Proton Mail](https://proton.me/) secure email. > ___ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems > ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
