Is anything special planned for the LionsOS CSPRNG entropy server … if there is one?
Looking at QNX, I was surprised by how much it resembles a typical monolithic kernel entropy subsystem WRT the level of access it has. But without that direct access, I’m not sure how one would get entropy!
While one can prove the functional correctness of the internal workings of given CSPRNG algorithm (like optimal recovery time) I think the main system level concern would be to prove the absence of timing side channels. But one must assume the irreversibility of hash WRT confidentiality, correct?
like optimal recovery time
Derp: while that is something one can prove, I don’t think that would be considered part of the “functional correctness”. It’s probably the least important thing to prove overall.
I don’t think there hasn’t been a lot of work in this area. The embedded world is so diverse that each OS basically does its own thing, usually very badly. Fortuna, Linux, and Windows entropy subsystems and the syscalls they expose are products of their time. I think LionsOS has an opportunity to innovate here.
I know a lot about CSPRNG design and the mitigations a robust design should incorporate. I’m taking a sabbatical from work and would love to work on this problem if mentoring or funding would be available. I’m not an OS developer, but I’ll start working through the seL4 and microkit tutorials tomorrow to figure out what sort of shape the API should take.
If anyone has any thoughts on a LionsOS specific design, please reply here or DM me on Mattermost!