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.
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 Benjamin.Kelly@windsorlake.llc 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
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 z.coldplayer@gmail.com 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 Benjamin.Kelly@windsorlake.llc 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
On 28 Nov 2023, at 12:43, Benjamin J. Kelly Benjamin.Kelly@windsorlake.llc 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
On 28 Nov 2023, at 12:43, Benjamin J. Kelly Benjamin.Kelly@windsorlake.llc 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.abstra...
Gernot
On Tue, 28 Nov 2023 at 07:52, Gernot Heiser via Devel devel@sel4.systems wrote:
On 28 Nov 2023, at 12:43, Benjamin J. Kelly Benjamin.Kelly@windsorlake.llc 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.abstra...
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.
-
Benjamin J. Kelly -
Gernot Heiser -
Jheengut Pritvi