You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Going forward a few years I still did some engineering work to support my poorly paid job as a security researcher doing crypto and network specs, papers, attacks etc. -- one of the projects I've got to know due to this was because of a paper written about a TLS and other crypto stacks for a single purpose: being correct and properly implemented. being verifyable. it was called nqsb (not quite so broken) - this in turn led me back to unikernels, OCaml as a functional OOP language that you can verify (langsec being a hot topic back then in security) and mirage os. mirage.io
Mirage OS has a core community, is being actively developed and deployed for real world use cases, although a bit academic, it is a really neat project. in the past it was run on xen, bhyve, solo5 and other hypervisors. By now it can be built reproducible. As it's Ocaml - of course it's fully verifiable - meaning you can mathematically proof that your code - say your TCP/IP or XMPP or SMTP implementation is correct. A big topic in security and operating systems design, and the reason behind some recent advances of programming languages like Go, Rust etc.: although they don't have solvers, they use very strict, strongly typed models to ensure core userspace or e.g. driver code can't be implemented in an unsafe way. Ocaml is very similar in that regard. And MirageOS even more so. If one of your examples would be running a tiny linux VM just for nginx: why not run a library unikernel OS that just serves HTTP over TLS for a blog? or a load-balancer etc.? doesn't get much slicker than that. And you can pretty much guarantee that it will be almost always bug free. Which typically isn't the case with any kernel, microkernel, unikernel or whatever written in C. Even Rust projects at that level use unsafe a fair amount to expose HW efficently.
MirageOS should defintely be supported: it has great use cases, being able to deploy it on your platform would probably also get you great insight from the core development team, which includes some extremely smart people knowing the ins and outs of operating systems, virtual memory, file systems and the network stack by heart. I had the pleasure of attending a MirageOS retreat in 2017 and was awestruck by the people this community managed to collect, and fellow interested hackers that work on different / often related projects or languages some of which are among the best in their field.
What's would e cooler than having a single kernel server a page over HTTPS? well it's totally possible:
What do you think? Thanks for your time.
Aaron / azet (not an OCaml developer nor related to MirageOS directly)
(edit: updated with current links to the kitten LWK and similar projects, kitten in it's original form seems to have been picked up again and ported forward with improvements, mckernel, mOS etc. have similar goals - but are catered to specific architectures i.e. specific supercomputing sites running a certain CPU vendor&version, MPI etc.)
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
Hi,
I've searched the doc., website and issues on GitHub but this hasn't come up yet, so I'll bring it up as an Idea (nice way to choose issue types btw):
Backstory [if you're already thinking TL;DR - just jump over the next 1.5-2 paragraphs]:
I like this idea and I came across this projects and company due to the talk at SREcon. In any case, for some time now I've been following different os architecture and development. One very interesting one for me at least was unikernels, microkernels etc. - I used to work in HPC and big top10 sites like LLNL would sometimes build their own purpose built tiny linux distro with a kernel, everything ripped out except the bare few things they need (scheduler, tcp stack - or RDMA/infiniband), VM, VFS etc. - but often going as far as not even having support for disk drivers or more than a very specific file system. because the linux fork would only do one thing: run a single app as pid 1 very very very fast at extremely low jitter. hundereds of tausends of times in a huge HPC machine. I love the idea and hacked on it a bit. but it was based on 2.4 and never further developed because of different trends in HPC.
Going forward a few years I still did some engineering work to support my poorly paid job as a security researcher doing crypto and network specs, papers, attacks etc. -- one of the projects I've got to know due to this was because of a paper written about a TLS and other crypto stacks for a single purpose: being correct and properly implemented. being verifyable. it was called nqsb (not quite so broken) - this in turn led me back to unikernels, OCaml as a functional OOP language that you can verify (langsec being a hot topic back then in security) and mirage os. mirage.io
MirageOS & supporting running on your stack
Mirage OS has a core community, is being actively developed and deployed for real world use cases, although a bit academic, it is a really neat project. in the past it was run on xen, bhyve, solo5 and other hypervisors. By now it can be built reproducible. As it's Ocaml - of course it's fully verifiable - meaning you can mathematically proof that your code - say your TCP/IP or XMPP or SMTP implementation is correct. A big topic in security and operating systems design, and the reason behind some recent advances of programming languages like Go, Rust etc.: although they don't have solvers, they use very strict, strongly typed models to ensure core userspace or e.g. driver code can't be implemented in an unsafe way. Ocaml is very similar in that regard. And MirageOS even more so. If one of your examples would be running a tiny linux VM just for nginx: why not run a library unikernel OS that just serves HTTP over TLS for a blog? or a load-balancer etc.? doesn't get much slicker than that. And you can pretty much guarantee that it will be almost always bug free. Which typically isn't the case with any kernel, microkernel, unikernel or whatever written in C. Even Rust projects at that level use
unsafe
a fair amount to expose HW efficently.MirageOS should defintely be supported: it has great use cases, being able to deploy it on your platform would probably also get you great insight from the core development team, which includes some extremely smart people knowing the ins and outs of operating systems, virtual memory, file systems and the network stack by heart. I had the pleasure of attending a MirageOS retreat in 2017 and was awestruck by the people this community managed to collect, and fellow interested hackers that work on different / often related projects or languages some of which are among the best in their field.
What's would e cooler than having a single kernel server a page over HTTPS? well it's totally possible:
https://github.com/mirage/mirage-skeleton/blob/8c9990b4fbe050e16f0e347fc3a87533d73ca7b8/applications/static_website_tls/dispatch.ml#L45-L57
https://github.com/mirage/mirage-skeleton/blob/3aa77601a1741d2c86cea308ccf9105c3b0e7b35/applications/http/unikernel.ml#L117
Or a full DHCP server for your cloud env.? Same:
https://github.com/mirage/mirage-skeleton/blob/8c9990b4fbe050e16f0e347fc3a87533d73ca7b8/applications/dhcp/unikernel.ml#L21-L45
What do you think? Thanks for your time.
Aaron / azet (not an OCaml developer nor related to MirageOS directly)
(edit: updated with current links to the kitten LWK and similar projects, kitten in it's original form seems to have been picked up again and ported forward with improvements, mckernel, mOS etc. have similar goals - but are catered to specific architectures i.e. specific supercomputing sites running a certain CPU vendor&version, MPI etc.)
Beta Was this translation helpful? Give feedback.
All reactions