4 ms·

Memory safety and type safety are different things. They usually go together, but not necessarily so.

• tialaramex 3y ago
  This seems like it ought to make sense, but do you have a concrete example?
  • remram 3y ago
    Null pointer dereference, out of bound array accesses.
    • tialaramex 3y ago
      I was looking for concrete issues which violate either memory safety or type safety but not both. However, these examples are clearly both. Let's look at the null pointer case first: Is this a memory safety issue? Yes, this is definitely a memory safety issue. The actual hardware has no concept of a "null" pointer, it just uses raw addresses - so if we allow this operation typically we're accessing arbitrary memory which happens to have an address corresponding to our "null" pointer. How about type safety? Well we violate type safety if we perform any operation on an object which isn't sanctioned by its type, and dereferencing isn't a sanctioned operation for the null pointer type. Now how about array bounds? Memory safety is pretty obvious here, this is the classic stack smash beloved of "hackers". And type safety? The bounds miss is not a sanctioned operation for this type.
      • noelwelsh 3y ago
        That's not really how most type systems work. Take array access. The typical typing is: if you have an `Array[A]` and reference an `Int` index you get an element of type `A`. ref: Array[A] Int => A This says nothing about what happens if you access an out of bounds element. In a memory safe language this is enforced by a runtime check. Without memory safety you get YOLO semantics like in C.
      • remram 3y ago
        I don't know what kind of type system you have in mind then. Do you have an example of language where all array types have a way to check, statically, that all indexing operations are in bound? How would that even work? A language without dynamically-sized arrays at all, maybe?
        • trealira 3y ago
          I think you can do this with proof assistants, and with the SPARK version of Ada. You can also do it with a dependent type system. I haven't used it, but from what I've read, in the ATS programming language, which is dependently typed, you can guarantee that array index accesses and pointer arithmetic never goes out of bounds, at the cost of having to pass proof variables explicitly to various functions. This poster goes over how to ensure you don't cause buffer overflows in it: https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-b... https://bluishcoder.co.nz/2018/01/10/capturing-program-invariants-in-ats.html https://bluishcoder.co.nz/2018/01/10/capturing-program-invar... It's a bit obscure; this is the only person who's ever blogged about ATS, as far as I can tell.
        • tialaramex 3y ago
          Two things. Firstly, it is simply not the case that all constraints must be able to be statically enforced for them to constitute part of the type's definition. I'd guess that's a huge part of the confusion here. But, yes, actually all WUFFS indexing is statically checked. It's using inference to conclude the range of the index, so if it won't fit that's a static type mismatch.
• trealira 3y ago
  In this case, a type sade programming language would stop you from trying to write to read-only memory at compile time.