17:41 <twold> Hello. I am very new to Mirage and while I love the idea, I have trouble deploying it. Is there some "getting started" guide for deploying to e.g. EC2 (or any other cloud)? I've seen one but it was very much outdated and I didn't get far. Has any new tutorial been released with 3.0? Thanks.

17:42 <twold> [For the record, I'm very much new to hypervisors too, which is probably where most of my confusion stems from.]

20:04 <kensan> Hi

20:05 <kensan> I mucked around with Solo5/UKVM this weekend and got it to run on our kernel.

20:05 <kensan> Small teaser: https://twitter.com/Kensan42/status/835941733359882240

21:41 <hannes> kensan: neat!

22:02 <kensan> hannes: thanks, with the Solo5 code it was pretty much straight forward for get a console and clock implementation working.

22:02 <kensan> ah forgot to mention, the kernel is Muen, see https://muen.sk.

22:08 <hannes> I've been skimming over muen some time ago

22:08 <hannes> that's very nice to hear!

22:09 <kensan> ah really? How did you hear about it?

22:09 <hannes> good question... not sure

22:10 <hannes> maybe a research paper, a talk (or submission) somewhere, or wikipedia :)

22:10 <hannes> i got excited that it has some formal methods applied to it :)

22:11 <hannes> (have some coq+separation logic background)

22:11 <kensan> We hope to work more in that direction.

22:12 <hannes> twold: I've no clue, never deployed on EC2... it is likely if you ask on the mirageos mailing list, you'll get an answer

22:12 <kensan> Currently we use SPARK to show absence of runtime errors plus a few invariants which it can handle.

22:13 <hannes> kensan: do you have device drivers developed for muen? or how do you deal with hardware? pci passthrough to guests?

22:13 <hannes> (sorry for not knowing too much detail about muen)

22:13 <kensan> hannes: We use VT-d DMA and Interupt Remapping for secure device passthrough to guest.

22:14 <kensan> hannes: basically we use Linux for drivers.

22:14 <hannes> a sensible solution

22:14 <kensan> hannes: but we also ported Genode which also has drivers (and much more).

22:15 <twold> hannes: thank you for the tip, I'll try that later. there are couple partial answers on the internet but no definitive guide AFAICT. if I manage to figure it out, I'll deploy a unikernel with a blogpost on how to do it :)

22:15 <hannes> kensan: yes.. i've never used genode though.. too big of a C++ monster

22:16 <kensan> hannes: Yeah that is true, but they know which parts of the language to avoid.

22:16 <hannes> twold: I know some did something for Mirage2, but I'm not aware of any Mirage3 scripts (though not sure whether anything in the deployment changed)

22:16 <kensan> hannes: Plus since we run it as a guest we do not have to trust it ;)

22:16 <hannes> kensan: true... is muen a research project, or already used in industry?

22:16 <kensan> hannes: Originally we ported Genode because of their VirtualBox support.

22:17 <hannes> kensan: IIRC I got to it from you following me on twitter and me looking on your profile ;)

22:17 <kensan> hannes: We work with industrial partner

22:17 <twold> I tried following something for Mirage2 but it was a lot of pain and it used prehistoric AWS tools, so I decided to give up that path for the moment.

22:17 <kensan> hannes: ah, sneaky :)

22:17 <hannes> twold: sounds sensible... I deploy only on my own FreeBSD bhyve machine..

22:18 <hannes> kensan: ah, that explains GPL? that actually keeps me away from looking deeper into muen

22:18 <kensan> hannes: I do not know if Muen makes much sense with Unikernels since I have the impression they show their strength when you can dynamically spawn them.

22:19 <kensan> hannes: GPL is for the kernel but does obviously not cover guests etc.

22:20 <kensan> hannes: Similar to Linux and userspace programs.

22:20 <hannes> kensan: sure, but muen is mainly the hypervisor/kernel, isn't it?

22:21 <hannes> kensan: there's a reason I use FreeBSD and no linux ;) (mainly because GPL is too long to read for me, and I don't understand its details)

22:21 <kensan> hannes: A big part is also the toolchain and system integration stuff.

22:22 <kensan> hannes: Yeah, I hear you. Licensing stuff is a pain.

22:22 <hannes> kensan: I go for the simple solution: BSD2. I enjoy writing code enough that I don't care what happens later with it ;)

22:22 <kensan> hannes: Some libraries that may be of interest when implementing a guest, we put under BSD.

22:22 <hannes> kensan: nice!

22:23 <kensan> hannes: We are mindful so people can build with it what they want under their license of choosing.

22:23 <kensan> hannes: at least that is our intention.

22:24 <hannes> kensan: sure. I've not enough knowledge to answer your question whether muen makes much sense with unikernels..

22:25 <kensan> hannes: Well I did the port so I could toy around with it and see what's going on in the unikernel/mirage world ;)

22:25 <kensan> hannes: or anybody else for that matter.

22:25 <hannes> in the end, what I'm looking for at some point, is a small hypervisor which just puts physical devices into vms, does not have a huge attack surface, and can manage mirageos vms

22:26 <hannes> kensan: and I'm excited to see a hello world from you! :) will definitively read up more on muen soon

22:26 <kensan> hannes: Muen can do that to some extent. "Manage" as in start/stop/restart is possible now.

22:27 <kensan> hannes: but resources and guests (what we call subjects) are statically allocated at integration/build time.

22:27 <hannes> ic

22:28 <hannes> thx for explaining

22:28 <kensan> hannes: ;) I will have to cleanup the code before I can put it somewhere.

22:29 <kensan> hannes: As for huge attack surface: the kernel itself does very little and there is no big hypercall API or something like that.

22:29 <hannes> kensan: once you did, pls tell the mirage mailing list :)

22:30 <kensan> hannes: I know sloc is a bad metric but just to give you an idea: Muen is currently ~5.5 kloc all in all.

22:30 <hannes> that is very small

22:30 <kensan> hannes: that includes the Ada/SPARK runtime plus contracts (flow & pre/post conditions).

22:31 <kensan> hannes: and we explicitly do not write our code so we have a small sloc count.

22:32 <hannes> similar for mirage... rather have a few more lines and readable code than as short as you can

22:32 <kensan> hannes: imho the static nature of a unikernel is more or less extended to the system-level when thinking of Muen.

22:33 <kensan> hannes: Ada/SPARK were designed to be readable and the compiler provides style-checks for consistency.

22:33 <kensan> hannes: Have to play around with Ocaml at some point.

22:34 <kensan> hannes: btw, I liked your nqsb tls paper. makes for an interesting read.

22:34 <hannes> yeah, i did some ada some decade ago...

22:34 <hannes> kensan: thx! :)

22:35 <hannes> (but only at university back when I was studying, no real project)

22:36 <kensan> hannes: Everybody seems to be running towards rust this time around ;)

22:37 <hannes> rust is nice.

22:38 <kensan> hannes: Unfortunately have not had time to take a look. It is on my ever-growing todo/to-read list...

22:39 <kensan> hannes: As was MirageOS/OCaml but the 3.0 release and Solo5 drew me in close enough to think "Hey, how hard can it be" ;)

22:40 <hannes> but then... OCaml is >25 years old and has a very nice runtime, soon multiprocessing, and is really stable. its numeric tower is unfortunately a bit sad (similar to C, fixed size integer types and overflow you've to check manually)

22:41 <kensan> What I like about Ada is that you can restrict certain language features and the compiler will enforce it.

22:42 <kensan> hannes: We have a bunch of those restriction pragmas for our kernel that is why we get away with a minimal runtime.

22:43 <kensan> hannes: and since we use SPARK the checks that would be runtime in Ada must be shown at compile time.

22:44 <hannes> yeah, in OCaml you get to do a lot at compile time, rather than runtime -- which is nice.. although expressivity is limited in the type system ;)

22:46 <kensan> hannes: With SPARK 2014 the language subset of Ada that is legal has significantly increased. Plus the tooling changed so since the verification conditions are translated to why3 you can use a bunch of provers be it automatic or interactive (e.g. Z3 or Isabelle).

22:48 <kensan> A prof who had his desk across from mine regularly reminded me to look more into functional prog, especially Haskell. Maybe mit Mirage/OCaml he will finally be happy :)

22:49 <hannes> imho it is worth a look.

22:50 <kensan> hannes: I agree and I have dipped my toes here and there but never actually done a project. Maybe Mirage will finally be the excuse.

22:55 <kensan> hannes: well it was nice and interesting talking to you.

22:55 <hannes> kensan: same here.. ttyl@

22:55 <hannes> s/@/!/

22:56 <kensan> hannes: Will let you know, when I make some more progress.