8 ms·

> First, how does the machine get updates? By eliminating updates. Why isn't software that runs on such machines proven correct? Yes, it's expensive, but medic

> First, how does the machine get updates? By eliminating updates. Why isn't software that runs on such machines proven correct? Yes, it's expensive, but medical equipment commands a premium price since it's supposed to meet stringent standards regardless. There's no reason to not up the standards for the software they run.

AnimalMuppet 7y ago
Proven correct? No. It's extensively verified and validated, but that's not the same thing. First, what are you going to prove? That it does what it's supposed to? No, because you have to have some formal definition of "what it's supposed to", and that can actually be wrong (see MCAS for an example - the software worked, the problem is that the spec was insane). Second, as somebody (Donald Knuth?) said, it's amazing how many bugs there can be in proven-correct (or formally verified) software. Does your proof prove against all possible bugs? No. Against all possible security issues? Still no. Third, even with those limitations, proven correct software is much harder (slower, and more expensive) to write, because the proof is really long. You want medical devices to have proven correct software? That would be nice. But we'd have maybe 2% of the medical devices that we have now, just because the proofs are so hard. That would be less nice. In particular, more people would die in that scenario from the absence of medical devices, than die in the existing scenario from bugs in them. That's less than helpful.
- craigsmansion 7y ago
  > That it does what it's supposed to? and that is doesn't do what is not supposed to do. As for your second point, if you could provide some background reading for that, I would appreciate it. I know of Knuth jokingly stating "Beware of bugs in the above code; I have only proved it correct, not tried it", but if he or someone else wrote a more serious paper on the occurrence of software errors in proved software, I would appreciate a link. A proof should prove against all software errors--if it doesn't I'm eager to learn more. As for your third point: software errors are a solved problem, but as you noted, it's a hard (expensive) solution. The solutions also currently may limit functionality, so it's unfortunately not applicable everywhere, but some classes of software should warrant it. In my view medical devices that can directly interact with a patient's physiology is one of them.
  - AnimalMuppet 7y ago
    I don't have any links to offer. The best I can do is an argument. Here's a tool or method that lets you prove that there are no security holes. Now here comes someone who identifies a completely new class of exploits. Does the proof prove that the software is immune to the new class of exploit? Maybe - it depends on the details of the new class of exploit, and on the details of the proof. So the proof that software is secure may be invalidated by new attacks. And this is (part of) why "proof against all software errors" is... let us say overly optimistic. Even when it's not security issues... do you have a list of all possible software errors, so that you can prove that none of them occur? I don't. I'm not sure that anyone does. I suspect that there's always some kind of error that isn't covered.
    - craigsmansion 7y ago
      Is suspect we're referring to different types of proof here. The sort of formal proof I refer to guarantees that the software will never display unspecified behaviour; your procedures are now backed by mathematical definitions with known properties. It's not about security. It's about the software functioning correctly so no functional updates are necessary, diminishing the need for remote updates and all the security problems that bring along. Even if remote access is needed to conveniently store various data in a different location there is no need to run everything on the same level. Smartphones are mass-produced computers that separate concerns with having a baseband and a main cpu. There is no reason a medical device could not have such a separation. One OS to keep the device working correctly under all circumstances, one OS to slap networking and interfacing on. I don't expect the medical technology industry to change quickly, but as things are they are adopting bad practices of software development and moving in the wrong direction. "If problems pop up, we'll update it later remotely" should not be an acceptable mindset for some classes of computer equipment.

AnimalMuppet 7y ago

Proven correct? No. It's extensively verified and validated, but that's not the same thing. First, what are you going to prove? That it does what it's supposed to? No, because you have to have some formal definition of "what it's supposed to", and that can actually be wrong (see MCAS for an example - the software worked, the problem is that the spec was insane). Second, as somebody (Donald Knuth?) said, it's amazing how many bugs there can be in proven-correct (or formally verified) software. Does your proof prove against all possible bugs? No. Against all possible security issues? Still no. Third, even with those limitations, proven correct software is much harder (slower, and more expensive) to write, because the proof is really long. You want medical devices to have proven correct software? That would be nice. But we'd have maybe 2% of the medical devices that we have now, just because the proofs are so hard. That would be less nice. In particular, more people would die in that scenario from the absence of medical devices, than die in the existing scenario from bugs in them. That's less than helpful.

craigsmansion 7y ago
> That it does what it's supposed to? and that is doesn't do what is not supposed to do. As for your second point, if you could provide some background reading for that, I would appreciate it. I know of Knuth jokingly stating "Beware of bugs in the above code; I have only proved it correct, not tried it", but if he or someone else wrote a more serious paper on the occurrence of software errors in proved software, I would appreciate a link. A proof should prove against all software errors--if it doesn't I'm eager to learn more. As for your third point: software errors are a solved problem, but as you noted, it's a hard (expensive) solution. The solutions also currently may limit functionality, so it's unfortunately not applicable everywhere, but some classes of software should warrant it. In my view medical devices that can directly interact with a patient's physiology is one of them.
- AnimalMuppet 7y ago
  I don't have any links to offer. The best I can do is an argument. Here's a tool or method that lets you prove that there are no security holes. Now here comes someone who identifies a completely new class of exploits. Does the proof prove that the software is immune to the new class of exploit? Maybe - it depends on the details of the new class of exploit, and on the details of the proof. So the proof that software is secure may be invalidated by new attacks. And this is (part of) why "proof against all software errors" is... let us say overly optimistic. Even when it's not security issues... do you have a list of all possible software errors, so that you can prove that none of them occur? I don't. I'm not sure that anyone does. I suspect that there's always some kind of error that isn't covered.
  - craigsmansion 7y ago
    Is suspect we're referring to different types of proof here. The sort of formal proof I refer to guarantees that the software will never display unspecified behaviour; your procedures are now backed by mathematical definitions with known properties. It's not about security. It's about the software functioning correctly so no functional updates are necessary, diminishing the need for remote updates and all the security problems that bring along. Even if remote access is needed to conveniently store various data in a different location there is no need to run everything on the same level. Smartphones are mass-produced computers that separate concerns with having a baseband and a main cpu. There is no reason a medical device could not have such a separation. One OS to keep the device working correctly under all circumstances, one OS to slap networking and interfacing on. I don't expect the medical technology industry to change quickly, but as things are they are adopting bad practices of software development and moving in the wrong direction. "If problems pop up, we'll update it later remotely" should not be an acceptable mindset for some classes of computer equipment.