4 ms·

Agree, I'd like exactly to look closer inside "hard enough". First, it depends on each specification -- what if the hardware is much-much smaller (IoT) and tas

Agree, I'd like exactly to look closer inside "hard enough". First, it depends on each specification -- what if the hardware is much-much smaller (IoT) and task to perform is well defined? It is hard today primarily because the required skill set becomes less and less current, but it is all demand-driven, it was not so some time ago. Secondly, it could be replicated to some extent only -- for example, verified libraries for each device could come from each HW IP provider, instead of coming from the SoC vendor who integrated them. Say, Synopsis would provide a verified lib for the GbE controller -- to use with all SoCs that integrate it, etc. And the final integrator would take care of verifying the final integration, including his very small, fast, low-power-consuming and maintainable and 100%-dedicated kernel. But my main argument is that the alternative is not so good-looking either. Porting and validation of the Linux kernel is performed mostly by engineers who have not the required skillset (managerial decision to spare on hires since "we have Linux") -- this is also something that I wish wasn't replicated among product makers but is, unfortunately.

pjc50 10y ago
> what if the hardware is much-much smaller (IoT) and task to perform is well defined? Anything IoT needs a full network stack at least, and usually a set of radio drivers for WiFi, 6lowpan, Zigbee, Bluetooth or whatever. That usually amounts to quite a lot of software, which in the case of the radio stuff is often proprietary and patent-encumbered. Asking the hardware vendors is a dead end. You might as well ask for a pony while you're at it, you're not going to get it either. "Verified libraries" would necessarily be written against a particular OS interface and its guarantees. I'm not even sure how this process would work in terms of formal verification; even sel4 is forced to make assumptions about hardware. The reason why you get bad Linux ports with no source and universal default passwords is simply cost. Customers do not incorporate security into their purchasing decisions - or they wouldn't buy these things - so this is what we get.
- minipci1321 10y ago
  In other words, you believe that Kaspersky OS has its place and future market? > Anything IoT needs a full network stack at least ... My point really is, every IoT device would need only its part of the full network stack, not all the protocols currently implemented in, say, Linux, and chances are, some device will require extremely reduced subset of the network stack, especially at the lower layers and with respect to kernel interaction. I am not a verification expert, but verifying a very reduced subset of a well-defined specs seems at least feasible -- how would we verify something open-ended? Those pesky little theorems would become much more general and would come in even greater numbers? Verifying a generic OS, good for all devices and all application, if at all doable from theoretical standpoint, looks too much of work for no particular profit for the verifier (very similar to the validation of the Linux kernel which is relayed on to the distro builders). I wouldn't be as pessimistic either about the hardware vendors. After all, (some of them) already use formal verification in (some of) the silicon design, and verifying closer to the silicon seems simpler -- the closer to the metal the less genericity (assuming the verified silicon underneath).

pjc50 10y ago

> what if the hardware is much-much smaller (IoT) and task to perform is well defined? Anything IoT needs a full network stack at least, and usually a set of radio drivers for WiFi, 6lowpan, Zigbee, Bluetooth or whatever. That usually amounts to quite a lot of software, which in the case of the radio stuff is often proprietary and patent-encumbered. Asking the hardware vendors is a dead end. You might as well ask for a pony while you're at it, you're not going to get it either. "Verified libraries" would necessarily be written against a particular OS interface and its guarantees. I'm not even sure how this process would work in terms of formal verification; even sel4 is forced to make assumptions about hardware. The reason why you get bad Linux ports with no source and universal default passwords is simply cost. Customers do not incorporate security into their purchasing decisions - or they wouldn't buy these things - so this is what we get.

minipci1321 10y ago
In other words, you believe that Kaspersky OS has its place and future market? > Anything IoT needs a full network stack at least ... My point really is, every IoT device would need only its part of the full network stack, not all the protocols currently implemented in, say, Linux, and chances are, some device will require extremely reduced subset of the network stack, especially at the lower layers and with respect to kernel interaction. I am not a verification expert, but verifying a very reduced subset of a well-defined specs seems at least feasible -- how would we verify something open-ended? Those pesky little theorems would become much more general and would come in even greater numbers? Verifying a generic OS, good for all devices and all application, if at all doable from theoretical standpoint, looks too much of work for no particular profit for the verifier (very similar to the validation of the Linux kernel which is relayed on to the distro builders). I wouldn't be as pessimistic either about the hardware vendors. After all, (some of them) already use formal verification in (some of) the silicon design, and verifying closer to the silicon seems simpler -- the closer to the metal the less genericity (assuming the verified silicon underneath).