avsm changed the topic of #mirage to: Good news everyone! Mirage 3.0 released!
seangrove has joined #mirage
seangrove has quit [Read error: Connection reset by peer]
copy` has quit [Quit: Connection closed for inactivity]
AltGr has joined #mirage
lars_kurth has quit [Read error: Connection reset by peer]
miragebot has joined #mirage
<miragebot> mirage/master 9978641 Thomas Leonard: Merge pull request #829 from talex5/profile-0.8...
miragebot has left #mirage [#mirage]
<miragebot> mirage/master 299773b Thomas Leonard: Update for mirage-profile 0.8...
<miragebot> [mirage] talex5 pushed 2 new commits to master: https://git.io/vH9Z4
copy` has joined #mirage
<dstolfa> kensan: I put you in a security presentation I have to give on Wednesday in the context of separation kernels and formal verification
<dstolfa> :P
<dstolfa> Well, MuenSK to be precise
<dstolfa> MirageOS found it's way in as well in the context of unikernels
<kensan> dstolfa: Oh ok, thanks :)
<kensan> dstolfa: Are the slides available somewhere?
<dstolfa> kensan: Not yet, but I'll happily send them over after I've refined them a bit :)
<kensan> dstolfa: and its "Muen SK" or "Muen Separation Kernel" ;)
<dstolfa> It's for interested students
<dstolfa> kensan: Ah right, sorry. I'll correct that
<kensan> dstolfa: no problem :)
<kensan> dstolfa: What is the topic and context of your presentation?
<dstolfa> kensan: Just an introduction to some security topics for 2nd year students after taking operating systems
<kensan> dstolfa: Ah cool.
<dstolfa> kensan: I put Muen in the conetxt of TCBs and their trustworthiness
<dstolfa> In the sense that formal verification through processor models and L4/Separation kernels can help verify a TCB
<kensan> dstolfa: Right, well thanks for mentioning Muen :)
<dstolfa> kensan: Well, AFAIK, it's been formally verified, hasn't it? :)
<kensan> dstolfa: Yeah, but it is not an "end-to-end" proof. "Just" that it has no runtime errors at the source code level.
<dstolfa> Oh yeah, but it demonstrates the concept well IMO
<dstolfa> I know that some folks in Texas(?) I think? have a model of amd64 and can help verify a TCB as well
<kensan> The current benchmark in formal verification of kernels is seL4. They have a/several proof(s) from the model/specification down to binary.
<kensan> in combination with the ARM ISA HOL4 spec.
AltGr has left #mirage [#mirage]
<kensan> dstolfa: This is a much stronger proof than what we currently have for Muen.
<dstolfa> kensan: Yeah, I've added seL4 too
<kensan> dstolfa: I think what is interesting about Muen is the effort required to achieve the proof of absence of runtime errors.
<kensan> dstolfa: We wrote the initial implementation in 6 months.
<dstolfa> kensan: Nice :)
<dstolfa> I'll make sure to mention that
<kensan> dstolfa: That includes the kernel implementation & proofs, toolchain and documentation.
<kensan> dstolfa: So to some extent it illustrates that projects applying formal methods are not necessarily hopelessly expensive.
<dstolfa> kensan: Yep, makes sense :)
<dstolfa> kensan: Btw, did you see what I posted on Slack yesterday?
<dstolfa> I've dumped a tracing session of VMs on twitter, it's pretty cool to see
<dstolfa> .. I wonder if we could have something like that on a L4-like kernel
<dstolfa> And have it be efficient
<kensan> dstolfa: Sorry, was busy with other stuff over the weekend (Haskell conf/hackathon).
<dstolfa> kensan: Ah yes, saw the tweets, was that fun?
<kensan> dstolfa: Yeah, except I do/did not know Haskell before so quite the learning curve for me *heh* Interesting talks plus great weather so \@/
<dstolfa> Nice! Good to hear it was fun
<kensan> Has further convinced me that I should really learn functional programming.
<kensan> Plus, I learned that HalVM 3.0 is apparently moving to Solo5 as a base platform (to bring the discussion a bit back on topic ;)
<dstolfa> kensan: I've been going about that for a while, but never got around to it properly :<
<kensan> dstolfa: Its why I went to the event to give me a real incentive to start digging in.
<kensan> mato: Do you know the state of thing of HalVM wrt. Solo5?
<dstolfa> kensan: Sounds like a good idea to attend one of those then :)
seliopou has quit [Ping timeout: 240 seconds]
seliopou has joined #mirage