4 ms·

> Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just

> Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just need the statistical bound on a double fault to be similar to that of the hardware case. Type systems can be used to do this by defining an interface for the data, letting you swap between normal datatypes and ECC ones seamlessly. (And in practice, you only need to define the base operators for your new type.) You can do this with ducktyping ECC versions of objects in say... Python. But the type system helps ensure that you've built the full set of components necessary and it properly links. You have to do this with ad hoc IDE tools in Python. Similarly.... > The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail. That actually sounds like exactly the situation that a type system would be used to prevent -- partly because from a type theoretic perspective, that whole situation sounds like an obvious defect. Further, the result was because of an obscure combination of key strokes that went untested. The use of total functions (enforced by the type system) lets you verify (by computer) that no combination of input can transition to a bad state. So... Did you intentionally pick two cases where type systems are the obvious solution to the problem?

ec109685 9y ago
What stops your program data from being modified or tampwered with without ECC ram, bypassing your checks?
- SomeStupidPoint 9y ago
  I'm not sure I understand your question, but the one that most pertains to ECC would be preventing corruption of the routine performing the checks -- It varies greatly by the method you use to ECC in software, since they all feature different mechanisms. In the case of the one I had in mind, the kernel is relatively small (so errors are unlikely), and once loaded, it's stable against bit errors. There are probably better answers, I'm not an expert on software ECC. (Tampering is a different issue -- if they can tamper with the program, ECC won't save you from them writing garbage to memory. So that a hack which can write memory can bypass memory safety isn't really interesting.)
  - ec109685 9y ago
    I meant tampering via a side channel attack (e.g. forcing a bit flip that ecc would protect). It doesn’t matter if your data types have referential integrity if a hacker could disable that protection. What I am arguing against is saying a typesafe language obviates the need for ecc memory.
    - SomeStupidPoint 9y ago
      > What I am arguing against is saying a typesafe language obviates the need for ecc memory. Which isn't what anyone said: I claimed you can do ECC in software and that type systems assist with that by making a clean interface and verifying the full implementation. (Since ECC is really just a lift of normal functions.) There's little difference between using 9 bits in hardware and 9 bits in software, except that you need to cleanly load your ECC code onto CPU cache and you're using CPU instructions per byte loaded. The reason we do ECC in hardware is efficiency on an operation we're doing on literally every byte. Lots of systems, eg harddrives, use ECC in their actual formats too, because you can do more complex ECC at the software level and not merely the extra bit. Sometimes, this software ECC is more efficient than hardware based ECC would be, because we're okay with less than 12.5% redundancy as long as we can still correct the errors we expect to find.
- deleted 9y ago
  [deleted]
blub 9y ago
You need to read Leveson's full report. It details quite clearly what role software played. If you're focusing on software and avoiding bugs you will at best have good quality software, when the goal is to have a safe system. SW is just part of the picture.
- SomeStupidPoint 9y ago
  I'm not arguing against hardware interlocks. I'm saying that's a weird example to pick of a case against type systems (eg, by asking how they'd have helped prevent that issue), since in that particular case, it actually sounds like a type system would have caught the software glitch that caused the issue.

ec109685 9y ago

What stops your program data from being modified or tampwered with without ECC ram, bypassing your checks?

SomeStupidPoint 9y ago
I'm not sure I understand your question, but the one that most pertains to ECC would be preventing corruption of the routine performing the checks -- It varies greatly by the method you use to ECC in software, since they all feature different mechanisms. In the case of the one I had in mind, the kernel is relatively small (so errors are unlikely), and once loaded, it's stable against bit errors. There are probably better answers, I'm not an expert on software ECC. (Tampering is a different issue -- if they can tamper with the program, ECC won't save you from them writing garbage to memory. So that a hack which can write memory can bypass memory safety isn't really interesting.)
- ec109685 9y ago
  I meant tampering via a side channel attack (e.g. forcing a bit flip that ecc would protect). It doesn’t matter if your data types have referential integrity if a hacker could disable that protection. What I am arguing against is saying a typesafe language obviates the need for ecc memory.
  - SomeStupidPoint 9y ago
    > What I am arguing against is saying a typesafe language obviates the need for ecc memory. Which isn't what anyone said: I claimed you can do ECC in software and that type systems assist with that by making a clean interface and verifying the full implementation. (Since ECC is really just a lift of normal functions.) There's little difference between using 9 bits in hardware and 9 bits in software, except that you need to cleanly load your ECC code onto CPU cache and you're using CPU instructions per byte loaded. The reason we do ECC in hardware is efficiency on an operation we're doing on literally every byte. Lots of systems, eg harddrives, use ECC in their actual formats too, because you can do more complex ECC at the software level and not merely the extra bit. Sometimes, this software ECC is more efficient than hardware based ECC would be, because we're okay with less than 12.5% redundancy as long as we can still correct the errors we expect to find.
deleted 9y ago
[deleted]

blub 9y ago

You need to read Leveson's full report. It details quite clearly what role software played. If you're focusing on software and avoiding bugs you will at best have good quality software, when the goal is to have a safe system. SW is just part of the picture.

SomeStupidPoint 9y ago
I'm not arguing against hardware interlocks. I'm saying that's a weird example to pick of a case against type systems (eg, by asking how they'd have helped prevent that issue), since in that particular case, it actually sounds like a type system would have caught the software glitch that caused the issue.