erictapen has quit [Ping timeout: 255 seconds]
erictapen has joined #nixos-security
pie__ has joined #nixos-security
pie___ has quit [Ping timeout: 272 seconds]
<zimbatm> talking about mirage, the docker 4 mac distribution is using parts of mirage
<pie__> zimbatm, oh? neat i guess
<zimbatm> basically these things were possible because of the unikernel exploration, rejoining my earlier argument :)
<pie__> there was some mention of vpnkit on the nixos mirage packaging issue
<pie__> "a tool for embedding ____ capabilities in your application"
<pie__> hm interesting
<pie__> zimbatm, so, unikernels are cool and all, but for security usage are they better than microkernels? one you need to start having multiple unikernels communicate you have to (?) expose a big complicated networking stack, which sounds worse than microkernels
<ekleog> pie__: you may be interested in http://rumpkernel.org/
<pie__> i need a survey lol...
<pie__> sad thing is im pretty sure none of this stuff is particularly relevant to my current work so im kind of wasting my time
* ekleog discovers there's an anykernel for ntfs support
<pie__> :(
<ekleog> well all of this stuff is particularly relevant to things that would be very interesting to do
<pie__> yes
<pie__> the problem being i should fcus on my work x)
<ekleog> if you want to try and write a seL4 userspace in rust with me some day… :D
<ekleog> I wonder if we could get some VC funding, make all the code open-source, and see how long we can live off that funding before they realize we've got nothing to sell
* ekleog should keep his evil plans secret
<pie__> >:D
<pie__> as long as you can make it technically not fraud
<ekleog> well, just do it docker-style
<pie__> whats stopping you from just running redox on it
* ekleog wonders what they actually sell
<pie__> or does that not really fit the model
<ekleog> redox is a full OS
<pie__> right
<ekleog> and it's not a cap-based OS afaik
<pie__> and you want the uhh...split things
<ekleog> yup
<pie__> its not? huh. i think they at least have caps on some level
<pie__> i watched part of a talk on youtube
<pie__> something about the filesystem URLs being capabilities
<ekleog> take libs from anykernel (or a reimplementation thereof in rust), and plug them into stuff
<ekleog> oh? that'd be nice, I haven't followed it in the last ~2 years, so…
<pie__> dumb question, does hardware vrtualizatoin by itself actually give any safety guarantees or does the inner OS need to prevent userspace from running certain privileged operations
<ekleog> now, I must say I'm sad they decided to implement their microkernel in rust while there already was a formally proven one freely available…
<ekleog> and they could have built userspace around it… but well.
<pie__> :V
<pie__> im waiting for the point where i start regretting not going into drawing anime girls instead of whatever it is im currently doing </joke>
<pie__> ekleog, you ever look at HalVM?
<ekleog> @hardware virtualization: if properly configured, it can provide safety guarantees, but it's possible to make a VM that has access to the full hardware (eg. Xen's dom0)
<ekleog> https://github.com/GaloisInc/HaLVM ? that… sounds… a bit weird of an idea
<ekleog> though I'm biased by much preferring processes on microkernels to VMs on hypervisors
<pie__> anyway...theres so many disparate ?kernel projects how does anyone really decide where to go...i guess its relatively easy to write a small kernel, so a question is going to be a compatibility layer + portable userspace
<ekleog> the cake is a portable userspace
<ekleog> only way to get a portable userspace is to emulate one of windows, mac or linux
<pie__> i think this might be sometihng like that https://github.com/Solo5/solo5
<pie__> ekleog, well i didnt necessarily mean *that* userspace
<pie__> (the reason i saw solo5 is its what mirage uses, its some kind of middleware)
<pie__> ofc its written in c :V
<ekleog> in order for the userspace to be portable it needs to abstract over the syscalls across platforms
<ekleog> but platforms have vastly different syscall formats already
<ekleog> linux, mac, BSDs… they're more or less Unixes so it kind of works
<ekleog> even windows has some compatibility by having the same libc interface
<ekleog> it'd be relatively hard to fit a libc-like interface around the seL4 security model, unless you want to just emulate linux and lose part of the security benefits it gives you
<ekleog> (when I say seL4 security model it's more widely any capability-based security model)
<ekleog> there are many things we'd need to change to improve things that it'd end up requiring basically a brand new userspace, with maybe a posix compatibility layer in order to be able to actually use the system
<ekleog> +so
<pie__> righ
<pie__> *right
<pie__> and microkernels seem like they would be a lot more different than alike
<pie__> so its a lost cause :P
<ekleog> well, the L4 series is pretty much alike, the question is what interface the userspace actually deals out
<pie__> why limit yourelf to sel4 :p
<pie__> (if only to make the problem not impossible :P)
<pie__> im wondering if it *would* be possible though to get the fundamentals down to a common api and make it zero cost (or near zero cost)
<ekleog> not only seL4, the L4 series, which is like a dozen microkernels :p
<ekleog> I think more and more that a capability-based API can be converted into a regular API at no cost
<ekleog> basically: if you can handle the most strict, then you can handle anything
<ekleog> now, even between capability-based APIs there are differences that might be difficult to abstract over
<pie__> " basically: if you can handle the most strict, " sounds like that could be a big if
<ekleog> heh, I'm designing my software exclusively as libraries that then get passed the functions to interact with the environment by a wrapper
<ekleog> (some people call that doing effects systems by hand)
<ekleog> it does have an impact on how you design your program
<pie__> hm
<pie__> i like that i think
<pie__> i mena, preferably, not doing it by hand, but yknow
<pie__> any recommendations for how to get started with effect systems if i ever get around to looking at that?
<ekleog> don't have, sorry :/
<pie__> ok
erictapen has quit [Ping timeout: 245 seconds]
erictapen has joined #nixos-security
erictapen has quit [Ping timeout: 272 seconds]
erictapen has joined #nixos-security
<pie__> ekleog, i think this might not be the same exact question i asked earlier xD : whats the differene between having a bunch of unikernels or a microkernel?
<pie__> afaiu youd have a lot more redundant stuff across the domains with a bunch of unikernels
<pie__> i think there may be somethng about the hardware enforcing stuff for the case of unikernels but i dont see why microkernels couldnt do that
<pie__> also i think zour first reading of halvm was kind of wrong
<pie__> seems like a proper unikernel thing to me they just used different words