4 ms·

> Their is no such things as unsafe and safe Zig. All Zig is unsafe, but you can add additional runtime checks Zig is meant to ultimately give you full memory

by pron 6y ago

> Their is no such things as unsafe and safe Zig. All Zig is unsafe, but you can add additional runtime checks Zig is meant to ultimately give you full memory safety, that you can selectively turn off. In addition, there are specific unsafe operations -- clearly marked -- such as casting an integer to a pointer or other non-typesafe casts. A code unit with safety checks on and without unsafe operations is what I call "safe Zig." > And without it your code isn't memory-safe. This is simply not true. Perhaps you mean that you don't have a guarantee that your code is memory-safe, but that's not the same thing. Our goal is not to write in a language with certain guarantees but to write programs with certain properties, say, without buffer overflows. One way of achieving such a program is to write it in a language that guarantees no such error can happen. Another is to write it in a language that guarantees no such error can happen in development, do some testing, and then remove the guarantees. In the second case it is true that our confidence in the lack of such errors is lower than the first, but in each case it is not 100%, and because the static guarantees are costly, it is possible that the second approach is even more effective at getting to more correct programs overall. They're both common ways for achieving the same goal. As someone who works with formal methods, we do these tradeoffs in formal verification all the time. It is simple false that sound guarantees are always the best way to correctness -- it would be if they were free, but they're not. Once you realise that the goal is achieving some desired level of confidence (which is never 100%, as that cannot exist in a physical system anyway) about overall program correctness -- which includes both "safety" and functional properties, each further divided into degrees of severity -- you see that there is no obvious way with the best effectiveness at achieving that goal. > If you never explicitly test the value “1337” during you debug session, you won't trigger the UB and you won't know it's here But here, again, you are looking at something in isolation. Because Zig is a simple language, the chances of such paths existing without you noticing are lower; also, because the language is simpler it is easier to write concolic testers that would automatically detect this. In fact, if such a "rare path" exists in a complex language that causes some functional bug -- ultimately, we don't care what bug breaks our program or leaves it open to security vulnerabilities -- there's a smaller chance that it will be discovered. Which is exactly what I mean by soundness coming at a cost. It guarantees the lack of certain bugs, but because it complicates the language, it can make other bugs more costly to detect.

littlestymaar 6y ago
> This is simply not true. Perhaps you mean that you don't have a guarantee that your code is memory-safe, but that's not the same thing. “But people can write correct C code”. Correct Zig != memory safety. It's the opposite: MEMORY SAFETY IS THE GUARANTEE that your code won't have memory error no matter how broken it is! > Another is to write it in a language that guarantees no such error can happen in development, do some testing, and then remove the guarantees. That's what the same kind of design as C is with ASan, TSan, MemSan etc. Yes Zig is less broken than C, leading to fewer sources of memory issues, but for what matters most (Double Free, Use After Free[1], Data Races) Zig and C offers the same level of safety guarantees: none. > As someone who works with formal methods, we do these tradeoffs in formal verification all the time. It is simple false that sound guarantees are always the best way to correctness -- it would be if they were free, but they're not. This is a straw man: comparing compile-time enforced ownership (Rust borrowck) to formal method doesn't make any more sense than comparing static typing to formal methods. It adds a lot of learning friction, but that's it. I just grepped my current 90kLoc rust project. You know how many lifetime annotation ('x) there is in it? Fifty-four! Which is one every 1666 lines. Please tell me again how much it cripples productivity and the ability to write correct code! > Because Zig is a simple language, the chances of such paths existing without you noticing are lower; If you ever try to use shared-memory parallelism, this kind of bugs will be everywhere! That's simple: every call to allocator.free is a minefield. > ultimately, we don't care what bug breaks our program or leaves it open to security vulnerabilities Memory safety issues aren't just security vulnerabilities, more than anything they are horrible bugs to track down, and it costs tons of money. > Which is exactly what I mean by soundness coming at a cost. It guarantees the lack of certain bugs, but because it complicates the language, it can make other bugs more costly to detect. This is BS. It's not because a language has few symbols or a simple syntax that it is easier to debug. Otherwise brainfuck would be the ultimate productivity tool. Semantic is what matters, and because it has UBs, Zig semantic is more complex than most languages out there. That's why C is one of the most complex language ever in practice, even if it's really “simple” and easy to “learn”. Again, don't get me wrong, I have nothing against Zig and I find it refreshing because it has tons of cool ergonomic tricks (and having a built-in sanitizer which “just works” out of the box in debug mode without any other programmer intervention is cool!). It's a nice programming language experiment that will probably inspire a lot of others, and it's probably a really cool language for C programmers who like to manage their memory by themselves and don't want the “nany compiler” Rust has and still have a language with a modern look and feel: that's totally legit. But memory safe, it isn't. [1]: which cause more than 30% of Google and Microsoft security issues by itself! (https://www.zdnet.com/article/microsoft-70-percent-of-all-security-bugs-are-memory-safety-issues/ https://www.zdnet.com/article/microsoft-70-percent-of-all-se... https://www.chromium.org/Home/chromium-security/memory-safety https://www.chromium.org/Home/chromium-security/memory-safet...)

by pron 6y ago

littlestymaar 6y ago

> This is simply not true. Perhaps you mean that you don't have a guarantee that your code is memory-safe, but that's not the same thing. “But people can write correct C code”. Correct Zig != memory safety. It's the opposite: MEMORY SAFETY IS THE GUARANTEE that your code won't have memory error no matter how broken it is! > Another is to write it in a language that guarantees no such error can happen in development, do some testing, and then remove the guarantees. That's what the same kind of design as C is with ASan, TSan, MemSan etc. Yes Zig is less broken than C, leading to fewer sources of memory issues, but for what matters most (Double Free, Use After Free[1], Data Races) Zig and C offers the same level of safety guarantees: none. > As someone who works with formal methods, we do these tradeoffs in formal verification all the time. It is simple false that sound guarantees are always the best way to correctness -- it would be if they were free, but they're not. This is a straw man: comparing compile-time enforced ownership (Rust borrowck) to formal method doesn't make any more sense than comparing static typing to formal methods. It adds a lot of learning friction, but that's it. I just grepped my current 90kLoc rust project. You know how many lifetime annotation ('x) there is in it? Fifty-four! Which is one every 1666 lines. Please tell me again how much it cripples productivity and the ability to write correct code! > Because Zig is a simple language, the chances of such paths existing without you noticing are lower; If you ever try to use shared-memory parallelism, this kind of bugs will be everywhere! That's simple: every call to allocator.free is a minefield. > ultimately, we don't care what bug breaks our program or leaves it open to security vulnerabilities Memory safety issues aren't just security vulnerabilities, more than anything they are horrible bugs to track down, and it costs tons of money. > Which is exactly what I mean by soundness coming at a cost. It guarantees the lack of certain bugs, but because it complicates the language, it can make other bugs more costly to detect. This is BS. It's not because a language has few symbols or a simple syntax that it is easier to debug. Otherwise brainfuck would be the ultimate productivity tool. Semantic is what matters, and because it has UBs, Zig semantic is more complex than most languages out there. That's why C is one of the most complex language ever in practice, even if it's really “simple” and easy to “learn”. Again, don't get me wrong, I have nothing against Zig and I find it refreshing because it has tons of cool ergonomic tricks (and having a built-in sanitizer which “just works” out of the box in debug mode without any other programmer intervention is cool!). It's a nice programming language experiment that will probably inspire a lot of others, and it's probably a really cool language for C programmers who like to manage their memory by themselves and don't want the “nany compiler” Rust has and still have a language with a modern look and feel: that's totally legit. But memory safe, it isn't. [1]: which cause more than 30% of Google and Microsoft security issues by itself! (https://www.zdnet.com/article/microsoft-70-percent-of-all-security-bugs-are-memory-safety-issues/ https://www.zdnet.com/article/microsoft-70-percent-of-all-se... https://www.chromium.org/Home/chromium-security/memory-safety https://www.chromium.org/Home/chromium-security/memory-safet...)