3 ms·
If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of ap
by nanolith 10y ago
If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would wish to exploit into a formally verified sandbox. That is the real power of systems like seL4, even though seL4 isn't itself really geared toward the sort of chipsets commonly used in consumer grade IoT products. However, a system _like_ seL4 can absolutely improve application level security, as long as the application is constrained by the architecture of the OS.
- tptacek 10y agoCan you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device? (I've done some L4 work so you don't need to spend a lot of time explaining.) General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.
- nanolith 10y agoCase in point: cryptography, authentication, and authorization are each very sensitive operations which are prone to both gadget attacks and sidechannel attacks. Sandboxing these operations by creating well-defined boundaries between application code and these algorithms and protocols can ensure that application level bugs cannot creep into these critical services. Consider, for instance, that it is possible to separate TCP/IP or wireless protocol stacks from authentication code so that, for instance, a packet fragmentation bug can't be exploited to influence authentication level decisions. This is classical defense in depth strategy, but enforced through both runtime and formal methods.
- indolering 10y agoYou wouldn't, SEL4 isn't designed for embedded systems. That's what NICTA's eChronos [1] is for : ) 1: http://ts.data61.csiro.au/projects/TS/echronos/ http://ts.data61.csiro.au/projects/TS/echronos/
- nickpsecurity 10y agoseL4 is designed for embeddee systems. That's why it mainly targeted ARM. Gernot Heiser even said so. I believe eChronos is just targeted for embedded devices with more constrained hardware.
- indolering 10y ago> I believe eChronos is just targeted for embedded devices with more constrained hardware. I guess it all depends on which meaning of IoT and embedded you are using.
- nickpsecurity 10y agoNo MMU is usually the differentiating constraint when there's two RTOS's. I dont use IoT because it's a BS buzzword.