Brendan wrote:- the compiler/language doesn't support compile time checking to prevent it, even though it's 100% possible to do so; or
It is not possible in every case to check array bounds at compile time. What you
can do at compile time is verify that only the necessary run-time checks are used. As HoTT said:
HoTT wrote:Many languages use bound checking by default and remove the checks where it can be statically proven they are not needed. Another approach would be to reject all programs where it cannot be proven, which usually will require to add a manual check.
Comes down to the ~same number of run time checks.
No matter how sophisticated your range type system, there will always be useful programs that, if they are not to be exploitable/crashable, must have runtime checks added by either the compiler (verification of ranged type conversion) or by the programmer (explicit ranged type conversions), even if it's nothing more than "take these 4 input bytes, check that they represent an integer in this range, otherwise error." This is a property of any turing complete language (actually a much bigger class of languages), not just of lazily-designed languages.
I would be very interested to see a useful language design that actually does all the checking at compile time. You'd upturn a lot of results in mathematics and computer science with it. Please describe your language design that does this or we're just going around in circles.
Brendan wrote:"security vulnerabilities" is an very unlikely worse case in a properly designed system and isn't even close to a guaranteed outcome for extremely badly designed systems.
Let's take the Linux kernel as an example of an "extremely badly designed system," because you've strongly disagreed with its design decisions in the past, and it's written in C, a language which does no bounds checking at compile time or runtime. In the year 2014 alone, there were
at least 21 buffer overflows, where
at least 6 of them resulted in remote code execution, and several others led to information leaks or security measure bypasses.
Now let's look at your imaginary well-designed system, but without bounds checks (because, paraphrasing my claim and your response, "when languages don't do bounds checking, security vulnerabilities are still very unlikely"). What would be different from Linux? Probably better APIs for I/O that don't rely on the programmer to manage the sizes of arbitrary-sized buffers, probably better protocols that don't involve as much indexing into buffers based on external data. But those are only guidelines, and programmers are human, and one of your core tenets of language design is that the compiler should do as much checking as possible, so why not combine better APIs and protocols with statically-enforced bounds checking?
Brendan wrote:In your example of a browser engine; a managed OS (that relies on a managed language for security/isolation) can not trust the browser because the browser is not "100% managed". Whether or not the malicious code's author thinks you should trust their virus (because they wrote most of the virus in "safe" code and a small part in "unsafe" code) is not particularly relevant when it comes to the OS and/or end user's trust.
I'm going to quote HoTT again:
HoTT wrote:However none of this requires managed code. Whatever that is.
I'm not talking about managed systems. Hardware checking is great, compile time checking is great, not trusting programmers is great.
I'm not talking about that at all. When I brought up trust, I was talking about tools to help programmers write the better-designed systems you're talking about, not user/OS/program trust.
There will always be times when you need to punch through the usual protections to implement abstractions or improve performance. But those times don't have to be "anywhere in your entire program any programmer felt like it." They can instead be "only in specifically marked locations that are easy to find automatically when something does go wrong," and those specifically marked locations can further be automatically banned by the compiler in most of the program.