avsm changed the topic of #mirage to: Good news everyone! Mirage 3.0 released!
rgrinberg has joined #mirage
brson has quit [Ping timeout: 268 seconds]
julio_ has quit [Quit: EliteBNC free bnc service - http://elitebnc.org - be a part of the Elite!]
rgrinberg has quit [Remote host closed the connection]
rgrinberg has joined #mirage
brson has joined #mirage
julio_ has joined #mirage
mattg_ has joined #mirage
sknebel_ has joined #mirage
smkz_ has joined #mirage
seliopou_ has joined #mirage
ptrf has quit [Ping timeout: 252 seconds]
mattg has quit [Ping timeout: 252 seconds]
sknebel has quit [Quit: No Ping reply in 180 seconds.]
smkz has quit [Ping timeout: 252 seconds]
seliopou has quit [Ping timeout: 252 seconds]
mattg_ is now known as mattg
brson has quit [Ping timeout: 240 seconds]
insitu has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
mort___ has joined #mirage
demonimin has quit [Ping timeout: 240 seconds]
demonimin has joined #mirage
mort___ has quit [Quit: Leaving.]
mort___ has joined #mirage
mort___ has quit [Quit: Leaving.]
insitu has joined #mirage
insitu has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
abeaumont has joined #mirage
ro6 has joined #mirage
mort___ has joined #mirage
abeaumont has quit [Ping timeout: 240 seconds]
mort___ has quit [Quit: Leaving.]
lobo has quit [Quit: WeeChat 1.0.1]
lobo has joined #mirage
ptrf has joined #mirage
brson has joined #mirage
insitu has joined #mirage
<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.
brson has quit [Ping timeout: 240 seconds]
<twold> [For the record, I'm very much new to hypervisors too, which is probably where most of my confusion stems from.]
copy` has joined #mirage
<kensan> Hi
<kensan> I mucked around with Solo5/UKVM this weekend and got it to run on our kernel.
mort___ has joined #mirage
insitu has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
mort___ has quit [Quit: Leaving.]
sknebel_ is now known as sknebel
sknebel has quit [Quit: sknebel]
sknebel has joined #mirage
<hannes> kensan: neat!
ro6 has quit [Quit: Connection closed for inactivity]
<kensan> hannes: thanks, with the Solo5 code it was pretty much straight forward for get a console and clock implementation working.
<kensan> ah forgot to mention, the kernel is Muen, see https://muen.sk.
<hannes> I've been skimming over muen some time ago
<hannes> that's very nice to hear!
<kensan> ah really? How did you hear about it?
<hannes> good question... not sure
<hannes> maybe a research paper, a talk (or submission) somewhere, or wikipedia :)
<hannes> i got excited that it has some formal methods applied to it :)
<hannes> (have some coq+separation logic background)
<kensan> We hope to work more in that direction.
<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
<kensan> Currently we use SPARK to show absence of runtime errors plus a few invariants which it can handle.
<hannes> kensan: do you have device drivers developed for muen? or how do you deal with hardware? pci passthrough to guests?
<hannes> (sorry for not knowing too much detail about muen)
<kensan> hannes: We use VT-d DMA and Interupt Remapping for secure device passthrough to guest.
<kensan> hannes: basically we use Linux for drivers.
<hannes> a sensible solution
<kensan> hannes: but we also ported Genode which also has drivers (and much more).
<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 :)
<hannes> kensan: yes.. i've never used genode though.. too big of a C++ monster
<kensan> hannes: Yeah that is true, but they know which parts of the language to avoid.
<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)
<kensan> hannes: Plus since we run it as a guest we do not have to trust it ;)
<hannes> kensan: true... is muen a research project, or already used in industry?
<kensan> hannes: Originally we ported Genode because of their VirtualBox support.
<hannes> kensan: IIRC I got to it from you following me on twitter and me looking on your profile ;)
<kensan> hannes: We work with industrial partner
<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.
<kensan> hannes: ah, sneaky :)
<hannes> twold: sounds sensible... I deploy only on my own FreeBSD bhyve machine..
<hannes> kensan: ah, that explains GPL? that actually keeps me away from looking deeper into muen
<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.
<kensan> hannes: GPL is for the kernel but does obviously not cover guests etc.
<kensan> hannes: Similar to Linux and userspace programs.
<hannes> kensan: sure, but muen is mainly the hypervisor/kernel, isn't it?
<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)
<kensan> hannes: A big part is also the toolchain and system integration stuff.
<kensan> hannes: Yeah, I hear you. Licensing stuff is a pain.
<hannes> kensan: I go for the simple solution: BSD2. I enjoy writing code enough that I don't care what happens later with it ;)
<kensan> hannes: Some libraries that may be of interest when implementing a guest, we put under BSD.
<hannes> kensan: nice!
<kensan> hannes: We are mindful so people can build with it what they want under their license of choosing.
<kensan> hannes: at least that is our intention.
<hannes> kensan: sure. I've not enough knowledge to answer your question whether muen makes much sense with unikernels..
<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 ;)
<kensan> hannes: or anybody else for that matter.
<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
<hannes> kensan: and I'm excited to see a hello world from you! :) will definitively read up more on muen soon
<kensan> hannes: Muen can do that to some extent. "Manage" as in start/stop/restart is possible now.
<kensan> hannes: but resources and guests (what we call subjects) are statically allocated at integration/build time.
<hannes> ic
<hannes> thx for explaining
<kensan> hannes: ;) I will have to cleanup the code before I can put it somewhere.
<kensan> hannes: As for huge attack surface: the kernel itself does very little and there is no big hypercall API or something like that.
<hannes> kensan: once you did, pls tell the mirage mailing list :)
<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.
<hannes> that is very small
<kensan> hannes: that includes the Ada/SPARK runtime plus contracts (flow & pre/post conditions).
<kensan> hannes: and we explicitly do not write our code so we have a small sloc count.
<hannes> similar for mirage... rather have a few more lines and readable code than as short as you can
<kensan> hannes: imho the static nature of a unikernel is more or less extended to the system-level when thinking of Muen.
<kensan> hannes: Ada/SPARK were designed to be readable and the compiler provides style-checks for consistency.
<kensan> hannes: Have to play around with Ocaml at some point.
<kensan> hannes: btw, I liked your nqsb tls paper. makes for an interesting read.
<hannes> yeah, i did some ada some decade ago...
<hannes> kensan: thx! :)
<hannes> (but only at university back when I was studying, no real project)
<kensan> hannes: Everybody seems to be running towards rust this time around ;)
<hannes> rust is nice.
<kensan> hannes: Unfortunately have not had time to take a look. It is on my ever-growing todo/to-read list...
<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" ;)
<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)
<kensan> What I like about Ada is that you can restrict certain language features and the compiler will enforce it.
<kensan> hannes: We have a bunch of those restriction pragmas for our kernel that is why we get away with a minimal runtime.
<kensan> hannes: and since we use SPARK the checks that would be runtime in Ada must be shown at compile time.
<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 ;)
<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).
abeaumont has joined #mirage
<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 :)
<hannes> imho it is worth a look.
<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.
<kensan> hannes: well it was nice and interesting talking to you.
<hannes> kensan: same here.. ttyl@
<hannes> s/@/!/
<kensan> hannes: Will let you know, when I make some more progress.