4 ms·
Besides full source boostrapping which could adopt progressive verification of hardware features and assumption of untrusted hardware, integration of Formal Ver
by neuroelectron 2y ago
Besides full source boostrapping which could adopt progressive verification of hardware features and assumption of untrusted hardware, integration of Formal Verification into the lowest levels of boostrapping is a must. Bootstap security with the compiler.
This won't protect against more complex attacks like RoP or unverified state. For that we need to implement simple artifacts that are verifiable and mapped. Return to more simple return states (pass/error). Do error handling external to the compiled binaries. Automate state mapping and combine with targeted fuzzing. Systemd is a perfect example of this kind of thing, what not to do: internal logs and error states being handled by a web of interdependent systems.
- AstralStorm 2y agoRoP and unverified state would at least be highlighted by such an analysis. Generally it's a lot of work and we cannot quite trust fully automated systems to keyword it to us... Especially when some optimizer changes between versions of the compiler. Even a single compile flag can throw the abstract language upside down, much less the execution graph... Fuzzing is good but probabilistic. It is unlikely to hit on a deliberate backdoor. Solid for finding bugs though.
- lrvick 2y agoI agree here. Use automated tools to find low hanging fruit, or mistakes. There is unfortunately no substitute for a coordinated effort to document review by capable security researchers on our toolchain sources.