Comment by jgiraldo29 | Hacker News Reader

Comment by jgiraldo29 | Hacker News Reader

Parent Full thread

Thank you so much. I really like the idea of the hypervisor-based verification approach as it would provide stronger isolation for the verification chain than the current in-kernel approach. It also aligns really well with some of VEKOS's core components. For instance, the current verification chain (in verification.rs) already maintains an append-only log of system operations:

pub struct VerificationRegistry { proofs: Vec<OperationProof>, current_state: AtomicU64, }

The current proof system could be extended (operation_proofs.rs) to communicate with a hypervisor-level verification layer.

About the ML, I actually had a previous scrapped component that would have allowed an ML model to run natively in the kernel by dividing the memory zones into 4 different components. Now for issues related to the memory, and for security concerns, I decided to not follow with it. ML are really good at detecting specific components, but I am afraid of the false alarms, as these could cause the system to have for example, spontaneous slow downs in the verifications.

Super interesting insights, thanks! I see you are much further already in this stuff, that's amazing.

you are right the ML might be tricky, i have a very specific design in which it might simplify what it's trying to analyse, but it does raise the question if its really going to be useful to add ML into security domain. one of the first things i learned about ML is that it shouldn't be implemented within systems that are not going to handle probabilistic errors well. (if you think about billions of operations, 0.001% false positives can already kill you etc.).

in the design i am going for, each subsystem of the os has its own little 'task language', which i'd hope simplifies what the ML is operating on (separate learning per subsystem to have only a relatively small domain to operate in - memory, disk, cpu, network, etc.). the tasks would be bytecodes interpreted a bit like java. (want to randomise mapping of bytecodes -> functions each time a module starts etc)

obviously this design is kind of leaning into being slow, and performing badly, to experiment with security ideas. i tested a bunch of it in user-mode code but getting the OS infra far enough to build it on baremetal has been an infinite struggle :D

will watch your progress with keen anticipation - i think i can learn tons of it, thanks!

Reply on news.ycombinator.com