4 ms·

> 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 readin

> 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

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.